let Omega be non empty set ; 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; 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; 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; ( 0 < P . (A /\ B) implies P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) )
assume A1:
0 < P . (A /\ B)
; 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)
; verum