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

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