let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob B holds
( prob A,B = 1 - (prob (A ` ),B) & prob (A ` ),B = 1 - (prob A,B) )
let A, B be Event of E; :: thesis: ( 0 < prob B implies ( prob A,B = 1 - (prob (A ` ),B) & prob (A ` ),B = 1 - (prob A,B) ) )
assume A1: 0 < prob B ; :: thesis: ( prob A,B = 1 - (prob (A ` ),B) & prob (A ` ),B = 1 - (prob A,B) )
( (A \/ (A ` )) /\ B = ([#] E) /\ B & ([#] E) /\ B = B ) by SUBSET_1:25, XBOOLE_1:28;
then (A /\ B) \/ ((A ` ) /\ B) = B by XBOOLE_1:23;
then (prob (A /\ B)) + (prob ((A ` ) /\ B)) = prob B by Th34, Th47;
then ((prob A,B) * (prob B)) + (prob ((A ` ) /\ B)) = prob B by A1, XCMPLX_1:88;
then ((prob A,B) * (prob B)) + ((prob (A ` ),B) * (prob B)) = prob B by A1, XCMPLX_1:88;
then (((prob A,B) + (prob (A ` ),B)) * (prob B)) * ((prob B) " ) = 1 by A1, XCMPLX_0:def 7;
then ((prob A,B) + (prob (A ` ),B)) * ((prob B) * ((prob B) " )) = 1 ;
then ((prob A,B) + (prob (A ` ),B)) * 1 = 1 by A1, XCMPLX_0:def 7;
hence ( prob A,B = 1 - (prob (A ` ),B) & prob (A ` ),B = 1 - (prob A,B) ) ; :: thesis: verum