let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P = COM (P2M P)
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma holds COM P = COM (P2M P)
let P be Probability of Sigma; :: thesis: COM P = COM (P2M P)
set Y = COM P;
COM (Sigma,P) = COM (Sigma,(P2M P)) by Th27;
then reconsider Y1 = P2M (COM P) as sigma_Measure of (COM (Sigma,(P2M P))) ;
for B being set st B in Sigma holds
for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B

proof

let B be set ; :: thesis: ( B in Sigma implies for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B )
assume A1: B in Sigma ; :: thesis: for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B
let C be thin of P2M P; :: thesis: Y1 . (B \/ C) = (P2M P) . B
reconsider C1 = C as thin of P by Th23;
(COM P) . (B \/ C1) = P . B by A1, Def8;
hence Y1 . (B \/ C) = (P2M P) . B ; :: thesis: verum

end;

hence COM P = COM (P2M P) by MEASURE3:def 5; :: thesis: verum