let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM Sigma,P
for B being set st B in ProbPart A holds
P . B = (COM P) . A
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A being Element of COM Sigma,P
for B being set st B in ProbPart A holds
P . B = (COM P) . A
let P be Probability of Sigma; :: thesis: for A being Element of COM Sigma,P
for B being set st B in ProbPart A holds
P . B = (COM P) . A
let A be Element of COM Sigma,P; :: thesis: for B being set st B in ProbPart A holds
P . B = (COM P) . A
let B be set ; :: thesis: ( B in ProbPart A implies P . B = (COM P) . A )
assume A1: B in ProbPart A ; :: thesis: P . B = (COM P) . A
A2: ( B in Sigma & B c= A & A \ B is thin of P ) by A1, Def7;
reconsider C = A \ B as thin of P by A1, Def7;
A3: A = B \/ C by A2, XBOOLE_1:45;
reconsider A = A as Event of COM Sigma,P ;
Sigma c= COM Sigma,P by Th29;
then reconsider B = B as Event of COM Sigma,P by A2;
B misses C by XBOOLE_1:79;
then A4: (COM P) . A = ((COM P) . B) + ((COM P) . C) by A3, PROB_1:def 13
.= ((COM P) . B) + 0 by Th41
.= (COM P) . B ;
reconsider B = B as Event of Sigma by A2;
(COM P) . A = P . B by A4, Th40;
hence P . B = (COM P) . A ; :: thesis: verum