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:9;
then 0 < - (- (1 - (prob B))) ;
then A3: 0 < prob (B `) by Th22;
prob A = (prob (A /\ B)) + (prob (A /\ (B `))) by Th26;
then prob A = ((prob (A,B)) * (prob B)) + (prob (A /\ (B `))) by A1, XCMPLX_1:87;
hence prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `))) by A3, XCMPLX_1:87; :: thesis: verum