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
consider D1 being set such that
A3: ( D1 in Sigma & C1 c= D1 & P . D1 = 0 ) by Def4;
consider D2 being set such that
A4: ( D2 in Sigma & C2 c= D2 & P . D2 = 0 ) by Def4;
A5: ( B1 c= B2 \/ C2 & B2 \/ C2 c= B2 \/ D2 ) by A2, A4, XBOOLE_1:7, XBOOLE_1:9;
A6: ( B2 c= B1 \/ C1 & B1 \/ C1 c= B1 \/ D1 ) by A2, A3, XBOOLE_1:7, XBOOLE_1:9;
reconsider B1 = B1, B2 = B2, D1 = D1, D2 = D2 as Event of Sigma by A1, A3, A4;
A7: P . B1 <= P . (B2 \/ D2) by A5, PROB_1:70, XBOOLE_1:1;
P . (B2 \/ D2) <= (P . B2) + (P . D2) by PROB_1:75;
then A8: P . B1 <= P . B2 by A4, A7, XXREAL_0:2;
A9: P . B2 <= P . (B1 \/ D1) by A6, PROB_1:70, XBOOLE_1:1;
P . (B1 \/ D1) <= (P . B1) + (P . D1) by PROB_1:75;
then P . B2 <= P . B1 by A3, A9, XXREAL_0:2;
hence P . B1 = P . B2 by A8, XXREAL_0:1; :: thesis: verum