let I, Omega 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 5; :: 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 5; :: thesis: verum