let E be non empty finite set ; :: thesis: for A, B1, B2 being Event of E st 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 holds
prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)))
let A, B1, B2 be Event of E; :: thesis: ( 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 implies prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) )
assume that
A1: 0 < prob B1 and
A2: ( 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 ) ; :: thesis: prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)))
prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) by A1, A2, Th50;
hence prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) by A1, XCMPLX_1:87; :: thesis: verum