let E be non empty finite set ; :: thesis: for A, B, C being Event of E st 0 < prob (B /\ C) & 0 < prob C holds
prob ((A /\ B) /\ C) = ((prob A,(B /\ C)) * (prob B,C)) * (prob C)
let A, B, C be Event of E; :: thesis: ( 0 < prob (B /\ C) & 0 < prob C implies prob ((A /\ B) /\ C) = ((prob A,(B /\ C)) * (prob B,C)) * (prob C) )
assume that
A1: 0 < prob (B /\ C) and
A2: 0 < prob C ; :: thesis: prob ((A /\ B) /\ C) = ((prob A,(B /\ C)) * (prob B,C)) * (prob C)
prob ((A /\ B) /\ C) = prob (A /\ (B /\ C)) by XBOOLE_1:16;
then A3: prob ((A /\ B) /\ C) = (prob A,(B /\ C)) * (prob (B /\ C)) by A1, XCMPLX_1:88;
prob (B /\ C) = (prob B,C) * (prob C) by A2, XCMPLX_1:88;
hence prob ((A /\ B) /\ C) = ((prob A,(B /\ C)) * (prob B,C)) * (prob C) by A3; :: thesis: verum