let E be non empty finite set ; 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; ( 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
; 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
; verum