let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B, A being Event of Sigma st 0 < P . B holds
P . (A /\ B) = ((P .|. B) . A) * (P . B)
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for B, A being Event of Sigma st 0 < P . B holds
P . (A /\ B) = ((P .|. B) . A) * (P . B)
let P be Probability of Sigma; :: thesis: for B, A being Event of Sigma st 0 < P . B holds
P . (A /\ B) = ((P .|. B) . A) * (P . B)
let B, A be Event of Sigma; :: thesis: ( 0 < P . B implies P . (A /\ B) = ((P .|. B) . A) * (P . B) )
assume A1: 0 < P . B ; :: thesis: P . (A /\ B) = ((P .|. B) . A) * (P . B)
then ((P .|. B) . A) * (P . B) = ((P . (A /\ B)) / (P . B)) * (P . B) by Def6
.= ((P . (A /\ B)) * ((P . B) ")) * (P . B) by XCMPLX_0:def 9
.= (P . (A /\ B)) * (((P . B) ") * (P . B))
.= (P . (A /\ B)) * 1 by A1, XCMPLX_0:def 7
.= P . (A /\ B) ;
hence P . (A /\ B) = ((P .|. B) . A) * (P . B) ; :: thesis: verum