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
reconsider C = A \ B as thin of P by A1, Def7;
A2: B in Sigma by A1, Def7;
B c= A by A1, Def7;
then A3: A = B \/ C by XBOOLE_1:45;
Sigma c= COM (Sigma,P) by Th28;
then reconsider B = B as Event of COM (Sigma,P) by A2;
reconsider A = A as Event of COM (Sigma,P) ;
B misses C by XBOOLE_1:79;
then A4: (COM P) . A = ((COM P) . B) + ((COM P) . C) by A3, PROB_1:def 8
.= ((COM P) . B) + 0 by Th40
.= (COM P) . B ;
reconsider B = B as Event of Sigma by A1, Def7;
(COM P) . A = P . B by A4, Th39;
hence P . B = (COM P) . A ; :: thesis: verum