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 )

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

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
A,B are_independent_respect_to P
; :: thesis: (P .|. B) . A = P . A
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;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

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