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