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

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

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

for P being Probability of Sigma

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

let A be Event of Sigma; :: thesis: for P being Probability of Sigma

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

let P be Probability of Sigma; :: thesis: for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

let E be Event of Sigma; :: thesis: ( E = {} implies A,E are_independent_respect_to P )

A1: P . (A /\ ({} Sigma)) = (P . A) * 0 by VALUED_0:def 19

.= (P . A) * (P . ({} Sigma)) by VALUED_0:def 19 ;

assume E = {} ; :: thesis: A,E are_independent_respect_to P

hence A,E are_independent_respect_to P by A1; :: thesis: verum

for A being Event of Sigma

for P being Probability of Sigma

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

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

for P being Probability of Sigma

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

let A be Event of Sigma; :: thesis: for P being Probability of Sigma

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

let P be Probability of Sigma; :: thesis: for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

let E be Event of Sigma; :: thesis: ( E = {} implies A,E are_independent_respect_to P )

A1: P . (A /\ ({} Sigma)) = (P . A) * 0 by VALUED_0:def 19

.= (P . A) * (P . ({} Sigma)) by VALUED_0:def 19 ;

assume E = {} ; :: thesis: A,E are_independent_respect_to P

hence A,E are_independent_respect_to P by A1; :: thesis: verum