let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob A & prob B < 1 & A misses B holds
prob (A,(B `)) = (prob A) / (1 - (prob B))
let A, B be Event of E; :: thesis: ( 0 < prob A & prob B < 1 & A misses B implies prob (A,(B `)) = (prob A) / (1 - (prob B)) )
assume that
A1: 0 < prob A and
A2: prob B < 1 and
A3: A misses B ; :: thesis: prob (A,(B `)) = (prob A) / (1 - (prob B))
(prob B) - 1 < 1 - 1 by A2, XREAL_1:9;
then 0 < - (- (1 - (prob B))) ;
then A4: 0 < prob (B `) by Th22;
then (prob A) * (prob ((B `),A)) = (prob (B `)) * (prob (A,(B `))) by A1, Th39;
then (prob A) * 1 = (prob (B `)) * (prob (A,(B `))) by A1, A3, Th45;
then (prob A) * ((prob (B `)) ") = (prob (A,(B `))) * ((prob (B `)) * ((prob (B `)) ")) ;
then A5: (prob A) * ((prob (B `)) ") = (prob (A,(B `))) * 1 by A4, XCMPLX_0:def 7;
prob (B `) = 1 - (prob B) by Th22;
hence prob (A,(B `)) = (prob A) / (1 - (prob B)) by A5, XCMPLX_0:def 9; :: thesis: verum