let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
let Sigma be SigmaField of Omega; :: thesis: for A being Event of Sigma
for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
let A be Event of Sigma; :: thesis: for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
let P be Probability of Sigma; :: thesis: (P . (([#] Sigma) \ A)) + (P . A) = 1
A1: (([#] Sigma) \ A) \/ A = (A `) \/ A
.= [#] Omega by SUBSET_1:10
.= Omega ;
([#] Sigma) \ A misses A by XBOOLE_1:79;
then (P . (([#] Sigma) \ A)) + (P . A) = P . Omega by A1, Def8
.= 1 by Def8 ;
hence (P . (([#] Sigma) \ A)) + (P . A) = 1 ; :: thesis: verum