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 /\ B)))

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 /\ B)))

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
let P be Probability of Sigma; :: thesis: P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
thus P . (A \/ B) = (P . A) + (P . (B \ A)) by Th36
.= (P . A) + (P . (B \ (A /\ B))) by XBOOLE_1:47 ; :: thesis: verum