let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let P be Probability of Sigma; :: thesis: for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let B1, B2 be set ; :: thesis: ( B1 in Sigma & B2 in Sigma implies for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2 )
assume A1: ( B1 in Sigma & B2 in Sigma ) ; :: thesis: for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let C1, C2 be thin of P; :: thesis: ( B1 \/ C1 = B2 \/ C2 implies P . B1 = P . B2 )
assume A2: B1 \/ C1 = B2 \/ C2 ; :: thesis: P . B1 = P . 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 Sigma and
A6: C1 c= D1 and
A7: P . D1 = 0 by Def4;
A8: B1 \/ C1 c= B1 \/ D1 by A6, XBOOLE_1:9;
consider D2 being set such that
A9: D2 in Sigma and
A10: C2 c= D2 and
A11: P . D2 = 0 by Def4;
A12: B2 \/ C2 c= B2 \/ D2 by A10, XBOOLE_1:9;
reconsider B1 = B1, B2 = B2, D1 = D1, D2 = D2 as Event of Sigma by A1, A5, A9;
A13: P . (B1 \/ D1) <= (P . B1) + (P . D1) by PROB_1:39;
P . B2 <= P . (B1 \/ D1) by A4, A8, PROB_1:34, XBOOLE_1:1;
then A14: P . B2 <= P . B1 by A7, A13, XXREAL_0:2;
A15: P . (B2 \/ D2) <= (P . B2) + (P . D2) by PROB_1:39;
P . B1 <= P . (B2 \/ D2) by A3, A12, PROB_1:34, XBOOLE_1:1;
then P . B1 <= P . B2 by A11, A15, XXREAL_0:2;
hence P . B1 = P . B2 by A14, XXREAL_0:1; :: thesis: verum