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

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