let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C, B, A being Event of Sigma st C = B ` holds
P . A = (P . (A /\ B)) + (P . (A /\ C))
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for C, B, A being Event of Sigma st C = B ` holds
P . A = (P . (A /\ B)) + (P . (A /\ C))
let P be Probability of Sigma; :: thesis: for C, B, A being Event of Sigma st C = B ` holds
P . A = (P . (A /\ B)) + (P . (A /\ C))
let C, B, A be Event 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:44;
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:25
.= P . ((A /\ B) \/ (A /\ C)) by XBOOLE_1:23
.= (P . (A /\ B)) + (P . (A /\ C)) by A2, PROB_1:def 13 ;
hence P . A = (P . (A /\ B)) + (P . (A /\ C)) ; :: thesis: verum