let E be non empty finite set ; 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; ( 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
; 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; verum