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 st A c= B holds

P . (B \ A) = (P . B) - (P . A)

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

for P being Probability of Sigma st A c= B holds

P . (B \ A) = (P . B) - (P . A)

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st A c= B holds

P . (B \ A) = (P . B) - (P . A)

let P be Probability of Sigma; :: thesis: ( A c= B implies P . (B \ A) = (P . B) - (P . A) )

assume A1: A c= B ; :: thesis: P . (B \ A) = (P . B) - (P . A)

A misses B \ A by XBOOLE_1:79;

then (P . A) + (P . (B \ A)) = P . (A \/ (B \ A)) by Def8

.= P . B by A1, XBOOLE_1:45 ;

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

for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . (B \ A) = (P . B) - (P . A)

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

for P being Probability of Sigma st A c= B holds

P . (B \ A) = (P . B) - (P . A)

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st A c= B holds

P . (B \ A) = (P . B) - (P . A)

let P be Probability of Sigma; :: thesis: ( A c= B implies P . (B \ A) = (P . B) - (P . A) )

assume A1: A c= B ; :: thesis: P . (B \ A) = (P . B) - (P . A)

A misses B \ A by XBOOLE_1:79;

then (P . A) + (P . (B \ A)) = P . (A \/ (B \ A)) by Def8

.= P . B by A1, XBOOLE_1:45 ;

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