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