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 A = ((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 A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) )
assume that
A1: 0 < prob B1 and
A2: 0 < prob B2 and
A3: B1 \/ B2 = E and
A4: B1 misses B2 ; :: thesis: prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))
A5: B2 \ B1 = E \ B1 by A3, XBOOLE_1:40;
then 0 < prob (B1 `) by A2, A4, XBOOLE_1:83;
then 0 < 1 - (prob B1) by Th22;
then A6: 1 - (1 - (prob B1)) < 1 by XREAL_1:44;
B2 = B1 ` by A4, A5, XBOOLE_1:83;
hence prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) by A1, A6, Th49; :: thesis: verum