let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

let P be Probability of Sigma; :: thesis: ( A,B are_independent_respect_to P implies A,([#] Sigma) \ B are_independent_respect_to P )

assume A,B are_independent_respect_to P ; :: thesis: A,([#] Sigma) \ B are_independent_respect_to P

then A1: P . (A /\ B) = (P . A) * (P . B) ;

P . (A /\ (([#] Sigma) \ B)) = P . (A /\ (B `))

.= P . (A \ B) by SUBSET_1:13

.= P . (A \ (A /\ B)) by XBOOLE_1:47

.= ((P . A) * 1) - ((P . A) * (P . B)) by A1, PROB_1:33, XBOOLE_1:17

.= (P . A) * (1 - (P . B))

.= (P . A) * (P . (([#] Sigma) \ B)) by PROB_1:32 ;

hence A,([#] Sigma) \ B are_independent_respect_to P ; :: thesis: verum

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

let P be Probability of Sigma; :: thesis: ( A,B are_independent_respect_to P implies A,([#] Sigma) \ B are_independent_respect_to P )

assume A,B are_independent_respect_to P ; :: thesis: A,([#] Sigma) \ B are_independent_respect_to P

then A1: P . (A /\ B) = (P . A) * (P . B) ;

P . (A /\ (([#] Sigma) \ B)) = P . (A /\ (B `))

.= P . (A \ B) by SUBSET_1:13

.= P . (A \ (A /\ B)) by XBOOLE_1:47

.= ((P . A) * 1) - ((P . A) * (P . B)) by A1, PROB_1:33, XBOOLE_1:17

.= (P . A) * (1 - (P . B))

.= (P . A) * (P . (([#] Sigma) \ B)) by PROB_1:32 ;

hence A,([#] Sigma) \ B are_independent_respect_to P ; :: thesis: verum