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 A2, XBOOLE_1:7;
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 A6, XBOOLE_1:9;
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 A10, XBOOLE_1:9;
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 A7, MEASURE1:33, XXREAL_3:4;
M . B2 <= M . (B1 \/ D1) by A4, A8, MEASURE1:31, XBOOLE_1:1;
then A14: M . B2 <= M . B1 by A13, XXREAL_0:2;
A15: ( M . (B2 \/ D2) <= (M . B2) + (M . D2) & (M . B2) + (M . D2) = M . B2 ) by A11, MEASURE1:33, XXREAL_3:4;
M . B1 <= M . (B2 \/ D2) by A3, A12, MEASURE1:31, XBOOLE_1:1;
then M . B1 <= M . B2 by A15, XXREAL_0:2;
hence M . B1 = M . B2 by A14, XXREAL_0:1; :: thesis: verum