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