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 0 < P . A & 0 < P . B holds
(P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)
let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma
for P being Probability of Sigma st 0 < P . A & 0 < P . B holds
(P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)
let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st 0 < P . A & 0 < P . B holds
(P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)
let P be Probability of Sigma; :: thesis: ( 0 < P . A & 0 < P . B implies (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B) )
assume that
A1: 0 < P . A and
A2: 0 < P . B ; :: thesis: (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)
thus (((P .|. A) . B) * (P . A)) / (P . B) = (P . (A /\ B)) / (P . B) by A1, Th29
.= (P .|. B) . A by A2, Def6 ; :: thesis: verum