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

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