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 A = (((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 A = (((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 /\ B2 = {} and
A6: B1 /\ B3 = {} and
A7: B2 /\ B3 = {} ; :: according to XBOOLE_0:def 7 :: thesis: prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3))
(B1 /\ B3) \/ (B2 /\ B3) = B2 /\ B3 by A6;
then (B1 \/ B2) /\ B3 = {} by A7, XBOOLE_1:23;
then A8: B1 \/ B2 misses B3 ;
((B1 \/ B2) \/ B3) /\ A = A by A4, XBOOLE_1:28;
then ((B1 \/ B2) /\ A) \/ (B3 /\ A) = A by XBOOLE_1:23;
then prob A = (prob ((B1 \/ B2) /\ A)) + (prob (B3 /\ A)) by A8, Th21, XBOOLE_1:76;
then A9: prob A = (prob ((B1 /\ A) \/ (B2 /\ A))) + (prob (B3 /\ A)) by XBOOLE_1:23;
B1 misses B2 by A5;
then prob A = ((prob (A /\ B1)) + (prob (A /\ B2))) + (prob (A /\ B3)) by A9, Th21, XBOOLE_1:76;
then prob A = (((prob (A,B1)) * (prob B1)) + (prob (A /\ B2))) + (prob (A /\ B3)) by A1, XCMPLX_1:87;
then prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + (prob (A /\ B3)) by A2, XCMPLX_1:87;
hence prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) by A3, XCMPLX_1:87; :: thesis: verum