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