let Omega, I be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let P be Probability of Sigma; :: thesis: for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let F be ManySortedSigmaField of I,Sigma; :: thesis: for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let J, K be non empty Subset of I; :: thesis: ( F is_independent_wrt P & J misses K implies for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v) )

A1: ( MeetSections (J,F) is non empty Subset of Sigma & MeetSections (K,F) is non empty Subset of Sigma ) by Th13;

assume A2: ( F is_independent_wrt P & J misses K ) ; :: thesis: for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

A3: for p, q being Event of Sigma st p in MeetSections (J,F) & q in MeetSections (K,F) holds

p,q are_independent_respect_to P

assume ( u in sigUn (F,J) & v in sigUn (F,K) ) ; :: thesis: P . (u /\ v) = (P . u) * (P . v)

then ( u in sigma (MeetSections (J,F)) & v in sigma (MeetSections (K,F)) ) by Th11;

then u,v are_independent_respect_to P by A1, A3, Th10;

hence P . (u /\ v) = (P . u) * (P . v) by PROB_2:def 4; :: thesis: verum

for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let P be Probability of Sigma; :: thesis: for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let F be ManySortedSigmaField of I,Sigma; :: thesis: for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

let J, K be non empty Subset of I; :: thesis: ( F is_independent_wrt P & J misses K implies for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v) )

A1: ( MeetSections (J,F) is non empty Subset of Sigma & MeetSections (K,F) is non empty Subset of Sigma ) by Th13;

assume A2: ( F is_independent_wrt P & J misses K ) ; :: thesis: for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

A3: for p, q being Event of Sigma st p in MeetSections (J,F) & q in MeetSections (K,F) holds

p,q are_independent_respect_to P

proof

let u, v be Event of Sigma; :: thesis: ( u in sigUn (F,J) & v in sigUn (F,K) implies P . (u /\ v) = (P . u) * (P . v) )
let p, q be Event of Sigma; :: thesis: ( p in MeetSections (J,F) & q in MeetSections (K,F) implies p,q are_independent_respect_to P )

assume A4: ( p in MeetSections (J,F) & q in MeetSections (K,F) ) ; :: thesis: p,q are_independent_respect_to P

reconsider p = p, q = q as Subset of Omega ;

P . (p /\ q) = (P . p) * (P . q) by A2, A4, Th12;

hence p,q are_independent_respect_to P by PROB_2:def 4; :: thesis: verum

end;assume A4: ( p in MeetSections (J,F) & q in MeetSections (K,F) ) ; :: thesis: p,q are_independent_respect_to P

reconsider p = p, q = q as Subset of Omega ;

P . (p /\ q) = (P . p) * (P . q) by A2, A4, Th12;

hence p,q are_independent_respect_to P by PROB_2:def 4; :: thesis: verum

assume ( u in sigUn (F,J) & v in sigUn (F,K) ) ; :: thesis: P . (u /\ v) = (P . u) * (P . v)

then ( u in sigma (MeetSections (J,F)) & v in sigma (MeetSections (K,F)) ) by Th11;

then u,v are_independent_respect_to P by A1, A3, Th10;

hence P . (u /\ v) = (P . u) * (P . v) by PROB_2:def 4; :: thesis: verum