let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Event of Sigma holds P . A = (COM P) . A
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A being Event of Sigma holds P . A = (COM P) . A
let P be Probability of Sigma; :: thesis: for A being Event of Sigma holds P . A = (COM P) . A
reconsider C = {} as thin of P by Th24;
let A be Event of Sigma; :: thesis: P . A = (COM P) . A
thus P . A = (COM P) . (A \/ C) by Def8
.= (COM P) . A ; :: thesis: verum