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)
A3: prob (B /\ C) = (prob (B,C)) * (prob C) by A2, XCMPLX_1:87;
prob ((A /\ B) /\ C) = prob (A /\ (B /\ C)) by XBOOLE_1:16;
then prob ((A /\ B) /\ C) = (prob (A,(B /\ C))) * (prob (B /\ C)) by A1, XCMPLX_1:87;
hence prob ((A /\ B) /\ C) = ((prob (A,(B /\ C))) * (prob (B,C))) * (prob C) by A3; :: thesis: verum