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 0 < P . (A /\ B) holds
P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds
P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)
let P be Probability of Sigma; :: thesis: for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds
P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)
let A, B, C be Event of Sigma; :: thesis: ( 0 < P . (A /\ B) implies P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) )
assume A1: 0 < P . (A /\ B) ; :: thesis: P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)
then A2: 0 < P . A by PROB_1:34, XBOOLE_1:17;
P . ((A /\ B) /\ C) = (P . (B /\ A)) * ((P .|. (A /\ B)) . C) by A1, Th29
.= ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) by A2, Th29 ;
hence P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) ; :: thesis: verum