let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob B & prob B < 1 holds
prob A = ((prob A,B) * (prob B)) + ((prob A,(B ` )) * (prob (B ` )))
let A, B be Event of E; :: thesis: ( 0 < prob B & prob B < 1 implies prob A = ((prob A,B) * (prob B)) + ((prob A,(B ` )) * (prob (B ` ))) )
assume that
A1: 0 < prob B and
A2: prob B < 1 ; :: thesis: prob A = ((prob A,B) * (prob B)) + ((prob A,(B ` )) * (prob (B ` )))
(prob B) - 1 < 1 - 1 by A2, XREAL_1:11;
then 0 < - (- (1 - (prob B))) ;
then A3: 0 < prob (B ` ) by Th48;
prob A = (prob (A /\ B)) + (prob (A /\ (B ` ))) by Th53;
then prob A = ((prob A,B) * (prob B)) + (prob (A /\ (B ` ))) by A1, XCMPLX_1:88;
hence prob A = ((prob A,B) * (prob B)) + ((prob A,(B ` )) * (prob (B ` ))) by A3, XCMPLX_1:88; :: thesis: verum