let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for B, A1, A2, A3 being Event of Sigma
for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds
( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )
let Sigma be SigmaField of Omega; :: thesis: for B, A1, A2, A3 being Event of Sigma
for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds
( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )
let B, A1, A2, A3 be Event of Sigma; :: thesis: for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds
( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )
let P be Probability of Sigma; :: thesis: ( 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` implies ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) )
assume that
A1: 0 < P . B and
A2: 0 < P . A1 and
A3: 0 < P . A2 and
A4: 0 < P . A3 and
A5: ( A1 misses A2 & A3 = (A1 \/ A2) ` ) ; :: thesis: ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )
thus (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) = (((P .|. A1) . B) * (P . A1)) / (P . B) by A2, A3, A4, A5, Th32
.= (P .|. B) . A1 by A1, A2, Th36 ; :: thesis: ( (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )
thus (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) = (((P .|. A2) . B) * (P . A2)) / (P . B) by A2, A3, A4, A5, Th32
.= (P .|. B) . A2 by A1, A3, Th36 ; :: thesis: (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3)))
thus (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) = (((P .|. A3) . B) * (P . A3)) / (P . B) by A2, A3, A4, A5, Th32
.= (P .|. B) . A3 by A1, A4, Th36 ; :: thesis: verum