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