let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

let P be Probability of Sigma; :: thesis: P . (A \/ B) = (P . A) + (P . (B \ A))

A1: A misses B \ A by XBOOLE_1:79;

P . (A \/ B) = P . (A \/ (B \ A)) by XBOOLE_1:39

.= (P . A) + (P . (B \ A)) by A1, Def8 ;

hence P . (A \/ B) = (P . A) + (P . (B \ A)) ; :: thesis: verum

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

let P be Probability of Sigma; :: thesis: P . (A \/ B) = (P . A) + (P . (B \ A))

A1: A misses B \ A by XBOOLE_1:79;

P . (A \/ B) = P . (A \/ (B \ A)) by XBOOLE_1:39

.= (P . A) + (P . (B \ A)) by A1, Def8 ;

hence P . (A \/ B) = (P . A) + (P . (B \ A)) ; :: thesis: verum