let Omega be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 0 < P . B implies ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P ) )
assume A1: 0 < P . B ; :: thesis: ( (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 ) :: thesis: ( A,B are_independent_respect_to P implies (P .|. B) . A = P . A )

proof

assume (P .|. B) . A = P . A ; :: thesis: A,B are_independent_respect_to P
then ((P . (A /\ B)) / (P . B)) * (P . B) = (P . A) * (P . B) by A1, Def6;
then P . (A /\ B) = (P . A) * (P . B) by A1, XCMPLX_1:87;
hence A,B are_independent_respect_to P ; :: thesis: verum

end;

assume A,B are_independent_respect_to P ; :: thesis: (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; :: thesis: verum