let Omega be non empty set ; for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st 0 < P . B holds
( (P .|. B) . A = P . A iff A,B are_independent_respect_to P )
let Sigma be SigmaField of Omega; for P being Probability of Sigma
for A, B being Event of Sigma st 0 < P . B holds
( (P .|. B) . A = P . A iff A,B are_independent_respect_to P )
let P be Probability of Sigma; for A, B being Event of Sigma st 0 < P . B holds
( (P .|. B) . A = P . A iff A,B are_independent_respect_to P )
let A, B be Event of Sigma; ( 0 < P . B implies ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P ) )
assume A1:
0 < P . B
; ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P )
thus
( (P .|. B) . A = P . A implies A,B are_independent_respect_to P )
( A,B are_independent_respect_to P implies (P .|. B) . A = P . A )
assume
A,B are_independent_respect_to P
; (P .|. B) . A = P . A
then
(P . (A /\ B)) * ((P . B) ") = ((P . A) * (P . B)) * ((P . B) ")
;
then
(P . (A /\ B)) * ((P . B) ") = (P . A) * ((P . B) * ((P . B) "))
;
then
(P . (A /\ B)) * ((P . B) ") = (P . A) * 1
by A1, XCMPLX_0:def 7;
then
(P . (A /\ B)) / (P . B) = P . A
by XCMPLX_0:def 9;
hence
(P .|. B) . A = P . A
by A1, Def6; verum