let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds
P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds
P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))
let P be Probability of Sigma; :: thesis: for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds
P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))
let A, B, C be Event of Sigma; :: thesis: ( C = B ` & 0 < P . B & 0 < P . C implies P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) )
assume that
A1: C = B ` and
A2: 0 < P . B and
A3: 0 < P . C ; :: thesis: P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))
P . A = (P . (A /\ B)) + (P . (A /\ C)) by A1, Th14
.= (((P .|. B) . A) * (P . B)) + (P . (A /\ C)) by A2, Th29
.= (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) by A3, Th29 ;
hence P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) ; :: thesis: verum