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

for A, B, C being Event of Sigma

for P being Probability of Sigma st C = B ` holds

P . A = (P . (A /\ B)) + (P . (A /\ C))

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

for P being Probability of Sigma st C = B ` holds

P . A = (P . (A /\ B)) + (P . (A /\ C))

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

P . A = (P . (A /\ B)) + (P . (A /\ C))

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

assume A1: C = B ` ; :: thesis: P . A = (P . (A /\ B)) + (P . (A /\ C))

then B misses C by SUBSET_1:24;

then A /\ C misses B by XBOOLE_1:74;

then A2: A /\ B misses A /\ C by XBOOLE_1:74;

P . A = P . (A /\ ([#] Omega)) by XBOOLE_1:28

.= P . (A /\ (B \/ C)) by A1, SUBSET_1:10

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

.= (P . (A /\ B)) + (P . (A /\ C)) by A2, PROB_1:def 8 ;

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

for A, B, C being Event of Sigma

for P being Probability of Sigma st C = B ` holds

P . A = (P . (A /\ B)) + (P . (A /\ C))

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

for P being Probability of Sigma st C = B ` holds

P . A = (P . (A /\ B)) + (P . (A /\ C))

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

P . A = (P . (A /\ B)) + (P . (A /\ C))

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

assume A1: C = B ` ; :: thesis: P . A = (P . (A /\ B)) + (P . (A /\ C))

then B misses C by SUBSET_1:24;

then A /\ C misses B by XBOOLE_1:74;

then A2: A /\ B misses A /\ C by XBOOLE_1:74;

P . A = P . (A /\ ([#] Omega)) by XBOOLE_1:28

.= P . (A /\ (B \/ C)) by A1, SUBSET_1:10

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

.= (P . (A /\ B)) + (P . (A /\ C)) by A2, PROB_1:def 8 ;

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