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

proof

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;

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) )
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