let E be non empty finite set ; :: thesis: 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; :: thesis: ( 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 and
A3: 0 < prob B3 and
A4: (B1 \/ B2) \/ B3 = E and
A5: B1 misses B2 and
A6: B1 misses B3 and
A7: B2 misses B3 ; :: thesis: 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, A3, A4, A5, A6, A7, Th81;
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:88; :: thesis: verum