let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds
P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds
P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))
let P be Probability of Sigma; :: thesis: for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds
P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))
let A, A1, A2, A3 be Event of Sigma; :: thesis: ( A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 implies P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) )
assume that
A1: A1 misses A2 and
A2: A3 = (A1 \/ A2) ` and
A3: 0 < P . A1 and
A4: 0 < P . A2 and
A5: 0 < P . A3 ; :: thesis: P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))
A6: A /\ A1 misses A /\ A2 by A1, XBOOLE_1:76;
A1 \/ A2 misses A3 by A2, SUBSET_1:24;
then A7: A /\ (A1 \/ A2) misses A /\ A3 by XBOOLE_1:76;
A8: (A1 \/ A2) \/ A3 = [#] Omega by A2, SUBSET_1:10
.= Omega ;
((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) = ((P . (A /\ A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) by A3, Th29
.= ((P . (A /\ A1)) + (P . (A /\ A2))) + (((P .|. A3) . A) * (P . A3)) by A4, Th29
.= ((P . (A /\ A1)) + (P . (A /\ A2))) + (P . (A /\ A3)) by A5, Th29
.= (P . ((A /\ A1) \/ (A /\ A2))) + (P . (A /\ A3)) by A6, PROB_1:def 8
.= (P . (A /\ (A1 \/ A2))) + (P . (A /\ A3)) by XBOOLE_1:23
.= P . ((A /\ (A1 \/ A2)) \/ (A /\ A3)) by A7, PROB_1:def 8
.= P . (A /\ Omega) by A8, XBOOLE_1:23
.= P . A by XBOOLE_1:28 ;
hence P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) ; :: thesis: verum