let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P
let Sigma be SigmaField of Omega; :: thesis: for A being Event of Sigma
for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P
let A be Event of Sigma; :: thesis: for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P
let P be Probability of Sigma; :: thesis: A, [#] Sigma are_independent_respect_to P
P . (A /\ ([#] Sigma)) = (P . A) * 1 by XBOOLE_1:28
.= (P . A) * (P . ([#] Sigma)) by PROB_1:30 ;
hence A, [#] Sigma are_independent_respect_to P ; :: thesis: verum