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

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