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

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