let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for B1, B2 being set st B1 in S & B2 in S holds
for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for B1, B2 being set st B1 in S & B2 in S holds
for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2

let M be sigma_Measure of S; :: thesis: for B1, B2 being set st B1 in S & B2 in S holds
for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2

let B1, B2 be set ; :: thesis: ( B1 in S & B2 in S implies for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2 )

assume A1: ( B1 in S & B2 in S ) ; :: thesis: for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2

let C1, C2 be thin of M; :: thesis: ( B1 \/ C1 = B2 \/ C2 implies M . B1 = M . B2 )
assume A2: B1 \/ C1 = B2 \/ C2 ; :: thesis: M . B1 = M . B2
then A3: B1 c= B2 \/ C2 by XBOOLE_1:7;
A4: B2 c= B1 \/ C1 by ;
consider D1 being set such that
A5: D1 in S and
A6: C1 c= D1 and
A7: M . D1 = 0. by Def2;
A8: B1 \/ C1 c= B1 \/ D1 by ;
consider D2 being set such that
A9: D2 in S and
A10: C2 c= D2 and
A11: M . D2 = 0. by Def2;
A12: B2 \/ C2 c= B2 \/ D2 by ;
reconsider B1 = B1, B2 = B2, D1 = D1, D2 = D2 as Element of S by A1, A5, A9;
A13: ( M . (B1 \/ D1) <= (M . B1) + (M . D1) & (M . B1) + (M . D1) = M . B1 ) by ;
M . B2 <= M . (B1 \/ D1) by ;
then A14: M . B2 <= M . B1 by ;
A15: ( M . (B2 \/ D2) <= (M . B2) + (M . D2) & (M . B2) + (M . D2) = M . B2 ) by ;
M . B1 <= M . (B2 \/ D2) by ;
then M . B1 <= M . B2 by ;
hence M . B1 = M . B2 by ; :: thesis: verum