let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds
A,B \/ C are_independent_respect_to P
let Sigma be SigmaField of Omega; :: thesis: for A, B, C being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds
A,B \/ C are_independent_respect_to P
let A, B, C be Event of Sigma; :: thesis: for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds
A,B \/ C are_independent_respect_to P
let P be Probability of Sigma; :: thesis: ( A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C implies A,B \/ C are_independent_respect_to P )
assume that
A1: A,B are_independent_respect_to P and
A2: A,C are_independent_respect_to P and
A3: B misses C ; :: thesis: A,B \/ C are_independent_respect_to P
A4: A /\ B misses A /\ C by A3, XBOOLE_1:76;
P . (A /\ (B \/ C)) = P . ((A /\ B) \/ (A /\ C)) by XBOOLE_1:23
.= (P . (A /\ B)) + (P . (A /\ C)) by A4, PROB_1:def 8
.= ((P . A) * (P . B)) + (P . (A /\ C)) by A1
.= ((P . A) * (P . B)) + ((P . A) * (P . C)) by A2
.= (P . A) * ((P . B) + (P . C))
.= (P . A) * (P . (B \/ C)) by A3, PROB_1:def 8 ;
hence A,B \/ C are_independent_respect_to P ; :: thesis: verum