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 a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)

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 a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)

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 a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)

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 a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)

let J, K be non empty Subset of I; :: thesis: ( F is_independent_wrt P & J misses K implies for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c) )

assume A1: F is_independent_wrt P ; :: thesis: ( not J misses K or for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c) )

reconsider Si = Sigma as set ;
assume A2: J misses K ; :: thesis: for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)

let a, c be Subset of Omega; :: thesis: ( a in MeetSections (J,F) & c in MeetSections (K,F) implies P . (a /\ c) = (P . a) * (P . c) )
assume that
A3: a in MeetSections (J,F) and
A4: c in MeetSections (K,F) ; :: thesis: P . (a /\ c) = (P . a) * (P . c)
consider E1 being non empty finite Subset of I, f1 being SigmaSection of E1,F such that
A5: E1 c= J and
A6: a = meet (rng f1) by ;
A7: f1 is_independent_wrt P by A1;
consider E2 being non empty finite Subset of I, f2 being SigmaSection of E2,F such that
A8: E2 c= K and
A9: c = meet (rng f2) by ;
A10: f2 is_independent_wrt P by A1;
reconsider rngf1 = rng f1, rngf2 = rng f2 as set ;
reconsider f1 = f1 as Function of E1,rngf1 by FUNCT_2:6;
reconsider f2 = f2 as Function of E2,rngf2 by FUNCT_2:6;
consider m being Nat such that
A11: E2, Seg m are_equipotent by FINSEQ_1:56;
consider e2 being Function such that
A12: e2 is one-to-one and
A13: dom e2 = Seg m and
A14: rng e2 = E2 by ;
A15: e2 <> {} by A14;
reconsider e2 = e2 as Function of (Seg m),E2 by ;
A16: e2 is FinSequence by ;
A17: rng (f2 * e2) = rng f2 by ;
reconsider e2 = e2 as one-to-one FinSequence of E2 by ;
reconsider f2 = f2 as Function of E2,Si ;
deffunc H1( object ) -> set = f2 . \$1;
reconsider fe2 = f2 * e2 as FinSequence of Si ;
rng e2 = dom f2 by ;
then A18: len fe2 = len e2 by FINSEQ_2:29;
E2 c= E1 \/ E2 by XBOOLE_1:7;
then A19: rng e2 c= E1 \/ E2 ;
defpred S1[ object ] means \$1 in E1;
consider n being Nat such that
A20: E1, Seg n are_equipotent by FINSEQ_1:56;
consider e1 being Function such that
A21: e1 is one-to-one and
A22: dom e1 = Seg n and
A23: rng e1 = E1 by ;
A24: e1 <> {} by A23;
reconsider e1 = e1 as Function of (Seg n),E1 by ;
A25: e1 is FinSequence by ;
A26: rng (f1 * e1) = rng f1 by ;
reconsider e1 = e1 as one-to-one FinSequence of E1 by ;
reconsider f1 = f1 as Function of E1,Si ;
deffunc H2( object ) -> set = f1 . \$1;
reconsider fe1 = f1 * e1 as FinSequence of Si ;
rng e1 = dom f1 by ;
then A27: len fe1 = len e1 by FINSEQ_2:29;
consider h being Function such that
A28: ( dom h = E1 \/ E2 & ( for i being object st i in E1 \/ E2 holds
( ( S1[i] implies h . i = H2(i) ) & ( not S1[i] implies h . i = H1(i) ) ) ) ) from for x being object st x in dom (e1 ^ e2) holds
x in dom (h * (e1 ^ e2))
proof
let x be object ; :: thesis: ( x in dom (e1 ^ e2) implies x in dom (h * (e1 ^ e2)) )
assume A29: x in dom (e1 ^ e2) ; :: thesis: x in dom (h * (e1 ^ e2))
rng (e1 ^ e2) = dom h by ;
then (e1 ^ e2) . x in dom h by ;
hence x in dom (h * (e1 ^ e2)) by ; :: thesis: verum
end;
then A30: dom (e1 ^ e2) c= dom (h * (e1 ^ e2)) ;
for x being object st x in dom (h * (e1 ^ e2)) holds
x in dom (e1 ^ e2) by FUNCT_1:11;
then A31: dom (h * (e1 ^ e2)) c= dom (e1 ^ e2) ;
A32: dom (fe1 ^ fe2) = Seg ((len fe1) + (len fe2)) by FINSEQ_1:def 7
.= dom (e1 ^ e2) by
.= dom (h * (e1 ^ e2)) by ;
for x being object st x in dom (fe1 ^ fe2) holds
(fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
proof
let x be object ; :: thesis: ( x in dom (fe1 ^ fe2) implies (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x )
assume A33: x in dom (fe1 ^ fe2) ; :: thesis: (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
then reconsider x = x as Element of NAT ;
per cases ( x in dom fe1 or not x in dom fe1 ) ;
suppose A34: x in dom fe1 ; :: thesis: (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
then A35: (fe1 ^ fe2) . x = fe1 . x by FINSEQ_1:def 7;
A36: E1 c= E1 \/ E2 by XBOOLE_1:7;
A37: x in dom e1 by ;
then e1 . x in E1 by ;
then h . (e1 . x) = f1 . (e1 . x) by ;
then A38: (fe1 ^ fe2) . x = h . (e1 . x) by ;
(e1 ^ e2) . x = e1 . x by ;
hence (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by ; :: thesis: verum
end;
suppose not x in dom fe1 ; :: thesis: (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
then consider n being Nat such that
A39: n in dom fe2 and
A40: x = (len fe1) + n by ;
A41: n in dom e2 by ;
then A42: e2 . n in E2 by ;
E1 /\ E2 c= J /\ K by ;
then E1 /\ E2 c= {} by A2;
then E1 /\ E2 = {} ;
then E2 = (E2 \ E1) \/ {} by XBOOLE_1:51;
then A43: not e2 . n in E1 by ;
A44: E2 c= E1 \/ E2 by XBOOLE_1:7;
(fe1 ^ fe2) . x = fe2 . n by
.= f2 . (e2 . n) by
.= h . (e2 . n) by A28, A42, A43, A44
.= h . ((e1 ^ e2) . x) by ;
hence (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by ; :: thesis: verum
end;
end;
end;
then A45: fe1 ^ fe2 = h * (e1 ^ e2) by ;
for i being object st i in E1 \/ E2 holds
h . i in Sigma
proof
let i be object ; :: thesis: ( i in E1 \/ E2 implies h . i in Sigma )
assume A46: i in E1 \/ E2 ; :: thesis: h . i in Sigma
per cases ( i in E1 or not i in E1 ) ;
suppose A47: i in E1 ; :: thesis: h . i in Sigma
then h . i = f1 . i by ;
hence h . i in Sigma by ; :: thesis: verum
end;
suppose not i in E1 ; :: thesis: h . i in Sigma
then ( h . i = f2 . i & i in E2 ) by ;
hence h . i in Sigma by FUNCT_2:5; :: thesis: verum
end;
end;
end;
then reconsider h = h as Function of (E1 \/ E2),Sigma by ;
for i being set st i in E1 \/ E2 holds
h . i in F . i
proof
let i be set ; :: thesis: ( i in E1 \/ E2 implies h . i in F . i )
assume A48: i in E1 \/ E2 ; :: thesis: h . i in F . i
per cases ( i in E1 or not i in E1 ) ;
suppose A49: i in E1 ; :: thesis: h . i in F . i
then f1 . i in F . i by Def4;
hence h . i in F . i by ; :: thesis: verum
end;
suppose A50: not i in E1 ; :: thesis: h . i in F . i
then i in E2 by ;
then f2 . i in F . i by Def4;
hence h . i in F . i by ; :: thesis: verum
end;
end;
end;
then reconsider h = h as SigmaSection of E1 \/ E2,F by Def4;
A51: h is_independent_wrt P by A1;
E1 c= E1 \/ E2 by XBOOLE_1:7;
then A52: rng e1 c= E1 \/ E2 ;
reconsider Pfe1 = (P * f1) * e1, Pfe2 = (P * f2) * e2 as FinSequence of REAL by FINSEQ_2:32;
reconsider e2 = e2 as FinSequence of E1 \/ E2 by ;
reconsider e1 = e1 as FinSequence of E1 \/ E2 by ;
E1 /\ E2 c= J /\ K by ;
then E1 /\ E2 c= {} by A2;
then E1 /\ E2 = {} ;
then rng e1 misses rng e2 by ;
then reconsider e12 = e1 ^ e2 as one-to-one FinSequence of E1 \/ E2 by FINSEQ_3:91;
reconsider e1 = e1 as one-to-one FinSequence of E1 ;
reconsider fe1 = fe1 as FinSequence of Si ;
reconsider e2 = e2 as FinSequence of E2 ;
reconsider fe2 = fe2 as FinSequence of Si ;
reconsider f1 = f1 as Function of E1,Sigma ;
reconsider f2 = f2 as Function of E2,Sigma ;
reconsider P = P as Function of Si,REAL ;
A53: (P * h) * e12 = P * (h * (e1 ^ e2)) by RELAT_1:36
.= (P * fe1) ^ (P * fe2) by ;
A54: ( P * fe1 = Pfe1 & P * fe2 = Pfe2 ) by RELAT_1:36;
reconsider P = P as Function of Sigma,REAL ;
A55: Product ((P * f1) * e1) = P . (meet (rng (f1 * e1))) by ;
P . (a /\ c) = P . (meet ((rng f1) \/ (rng f2))) by
.= P . (meet (rng (fe1 ^ fe2))) by
.= Product (Pfe1 ^ Pfe2) by A24, A45, A51, A53, A54
.= (Product Pfe1) * (Product Pfe2) by RVSUM_1:97
.= (P . a) * (P . c) by A6, A9, A15, A10, A26, A17, A55 ;
hence P . (a /\ c) = (P . a) * (P . c) ; :: thesis: verum