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))
A4: prob (B ` ) = 1 - (prob B) by Th48;
(prob B) - 1 < 1 - 1 by A2, XREAL_1:11;
then 0 < - (- (1 - (prob B))) ;
then A5: 0 < prob (B ` ) by Th48;
then (prob A) * (prob (B ` ),A) = (prob (B ` )) * (prob A,(B ` )) by A1, Th69;
then (prob A) * 1 = (prob (B ` )) * (prob A,(B ` )) by A1, A3, Th75;
then (prob A) * ((prob (B ` )) " ) = (prob A,(B ` )) * ((prob (B ` )) * ((prob (B ` )) " )) ;
then (prob A) * ((prob (B ` )) " ) = (prob A,(B ` )) * 1 by A5, XCMPLX_0:def 7;
hence prob A,(B ` ) = (prob A) / (1 - (prob B)) by A4, XCMPLX_0:def 9; :: thesis: verum