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