let I, Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let P be Probability of Sigma; :: thesis:
let F be ManySortedSigmaField of I,Sigma; :: thesis:
let J, K be non empty Subset of I; :: thesis:
assume A0: F is_independent_wrt P ; :: thesis:
assume A1: J misses K ; :: thesis:
let a, c be Subset of Omega; :: thesis:
assume A2: ( a in MeetSections J,F & c in MeetSections K,F ) ; :: thesis:
consider E1 being non empty finite Subset of I, f1 being SigmaSection of E1,F such that
A3: ( E1 c= J & a = meet (rng f1) ) by A2, Def9;
consider E2 being non empty finite Subset of I, f2 being SigmaSection of E2,F such that
A4: ( E2 c= K & c = meet (rng f2) ) by A2, Def9;
consider n being Nat such that
A5: E1, Seg n are_equipotent by FINSEQ_1:77;
consider m being Nat such that
A6: E2, Seg m are_equipotent by FINSEQ_1:77;
consider e1 being Function such that
A7: ( e1 is one-to-one & dom e1 = Seg n & rng e1 = E1 ) by A5, WELLORD2:def 4;
A8: e1 <> {} by A7;
consider e2 being Function such that
A9: ( e2 is one-to-one & dom e2 = Seg m & rng e2 = E2 ) by A6, WELLORD2:def 4;
A10: e2 <> {} by A9;
A11: ( f1 is_independent_wrt P & f2 is_independent_wrt P ) by A0, Def5;
reconsider rngf1 = rng f1, rngf2 = rng f2 as set ;
reconsider f1 = f1 as Function of E1,rngf1 by FUNCT_2:8;
reconsider f2 = f2 as Function of E2,rngf2 by FUNCT_2:8;
reconsider e1 = e1 as Function of Seg n,E1 by A7, FUNCT_2:3;
reconsider e2 = e2 as Function of Seg m,E2 by A9, FUNCT_2:3;
A12: ( rng (f1 * e1) = rng f1 & rng (f2 * e2) = rng f2 ) by A7, A9, FUNCT_2:20;
A13: ( e1 is FinSequence & e2 is FinSequence ) by A7, A9, FINSEQ_1:def 2;
then reconsider e1 = e1 as one-to-one FinSequence of E1 by A7, FINSEQ_1:def 4;
reconsider e2 = e2 as one-to-one FinSequence of E2 by A9, A13, FINSEQ_1:def 4;
reconsider Si = Sigma as set ;
reconsider f1 = f1 as Function of E1,Si ;
reconsider fe1 = f1 * e1 as FinSequence of Si ;
reconsider f2 = f2 as Function of E2,Si ;
reconsider fe2 = f2 * e2 as FinSequence of Si ;
reconsider Pfe1 = (P * f1) * e1, Pfe2 = (P * f2) * e2 as FinSequence of REAL by FINSEQ_2:36;
deffunc H₁( set ) -> set = f1 . $1;
deffunc H₂( set ) -> set = f2 . $1;
defpred S₁[ set ] means $1 in E1;
consider h being Function such that
A14: ( dom h = E1 \/ E2 & ( for i being set st i in E1 \/ E2 holds
( ( S₁[i] implies h . i = H₁(i) ) & ( not S₁[i] implies h . i = H₂(i) ) ) ) ) from PARTFUN1:sch 1();
A15: fe1 ^ fe2 = h * (e1 ^ e2)

proof

( rng e1 = dom f1 & rng e2 = dom f2 ) by A7, A9, FUNCT_2:def 1;
then B0: ( len fe1 = len e1 & len fe2 = len e2 ) by FINSEQ_2:33;
for x being set st x in dom (h * (e1 ^ e2)) holds
x in dom (e1 ^ e2) by FUNCT_1:21;
then B1: dom (h * (e1 ^ e2)) c= dom (e1 ^ e2) by TARSKI:def 3;
for x being set st x in dom (e1 ^ e2) holds
x in dom (h * (e1 ^ e2))

proof

let x be set ; :: thesis:
assume C0: x in dom (e1 ^ e2) ; :: thesis:
rng (e1 ^ e2) = dom h by A14, A7, A9, FINSEQ_1:44;
then (e1 ^ e2) . x in dom h by C0, FUNCT_1:12;
hence x in dom (h * (e1 ^ e2)) by C0, FUNCT_1:21; :: thesis:

end;

then B2: dom (e1 ^ e2) c= dom (h * (e1 ^ e2)) by TARSKI:def 3;
B3: dom (fe1 ^ fe2) = Seg ((len fe1) + (len fe2)) by FINSEQ_1:def 7
.= dom (e1 ^ e2) by FINSEQ_1:def 7, B0
.= dom (h * (e1 ^ e2)) by B1, B2, XBOOLE_0:def 10 ;
for x being set st x in dom (fe1 ^ fe2) holds
(fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x

proof

let x be set ; :: thesis:
assume C0: x in dom (fe1 ^ fe2) ; :: thesis:
then reconsider x = x as Element of NAT ;

per cases ;

suppose D0: x in dom fe1 ; :: thesis:

then F0: (fe1 ^ fe2) . x = fe1 . x by FINSEQ_1:def 7;
F1: x in dom e1 by D0, FUNCT_1:21;
then F2: (e1 ^ e2) . x = e1 . x by FINSEQ_1:def 7;
F3: e1 . x in E1 by A7, F1, FUNCT_1:12;
E1 c= E1 \/ E2 by XBOOLE_1:7;
then h . (e1 . x) = f1 . (e1 . x) by F3, A14;
then (fe1 ^ fe2) . x = h . (e1 . x) by D0, F0, FUNCT_1:22;
hence (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by B3, C0, F2, FUNCT_1:22; :: thesis:

end;

suppose not x in dom fe1 ; :: thesis:

then consider n being Nat such that
F0: ( n in dom fe2 & x = (len fe1) + n ) by C0, FINSEQ_1:38;
F1: n in dom e2 by F0, FUNCT_1:21;
then F2: e2 . n in E2 by A9, FUNCT_1:12;
E1 /\ E2 c= J /\ K by A3, A4, XBOOLE_1:27;
then E1 /\ E2 c= {} by A1, XBOOLE_0:def 7;
then E1 /\ E2 = {} ;
then E2 = (E2 \ E1) \/ {} by XBOOLE_1:51;
then F3: not e2 . n in E1 by F2, XBOOLE_0:def 5;
F4: E2 c= E1 \/ E2 by XBOOLE_1:7;
(fe1 ^ fe2) . x = fe2 . n by F0, FINSEQ_1:def 7
.= f2 . (e2 . n) by F0, FUNCT_1:22
.= h . (e2 . n) by F2, F3, F4, A14
.= h . ((e1 ^ e2) . x) by F0, F1, B0, FINSEQ_1:def 7 ;
hence (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by C0, B3, FUNCT_1:22; :: thesis:

end;

hence fe1 ^ fe2 = h * (e1 ^ e2) by B3, FUNCT_1:9; :: thesis:

end;

for i being set st i in E1 \/ E2 holds
h . i in Sigma

proof

let i be set ; :: thesis:
assume B0: i in E1 \/ E2 ; :: thesis:

per cases ;

suppose C0: i in E1 ; :: thesis:

then h . i = f1 . i by B0, A14;
hence h . i in Sigma by C0, FUNCT_2:7; :: thesis:

end;

suppose C1: not i in E1 ; :: thesis:

then D0: h . i = f2 . i by B0, A14;
i in E2 by C1, B0, XBOOLE_0:def 3;
hence h . i in Sigma by D0, FUNCT_2:7; :: thesis:

end;

then reconsider h = h as Function of E1 \/ E2,Sigma by A14, FUNCT_2:5;
for i being set st i in E1 \/ E2 holds
h . i in F . i

proof

let i be set ; :: thesis:
assume B0: i in E1 \/ E2 ; :: thesis:

per cases ;

suppose C0: i in E1 ; :: thesis:

then f1 . i in F . i by Def4;
hence h . i in F . i by C0, B0, A14; :: thesis:

end;

suppose C1: not i in E1 ; :: thesis:

then i in E2 by B0, XBOOLE_0:def 3;
then f2 . i in F . i by Def4;
hence h . i in F . i by C1, B0, A14; :: thesis:

end;

then reconsider h = h as SigmaSection of E1 \/ E2,F by Def4;
A16: h is_independent_wrt P by Def5, A0;
E1 c= E1 \/ E2 by XBOOLE_1:7;
then rng e1 c= E1 \/ E2 by XBOOLE_1:1;
then reconsider e1 = e1 as FinSequence of E1 \/ E2 by FINSEQ_1:def 4;
E2 c= E1 \/ E2 by XBOOLE_1:7;
then rng e2 c= E1 \/ E2 by XBOOLE_1:1;
then reconsider e2 = e2 as FinSequence of E1 \/ E2 by FINSEQ_1:def 4;
E1 /\ E2 c= J /\ K by A3, A4, XBOOLE_1:27;
then E1 /\ E2 c= {} by A1, XBOOLE_0:def 7;
then E1 /\ E2 = {} ;
then rng e1 misses rng e2 by A7, A9, XBOOLE_0:def 7;
then reconsider e12 = e1 ^ e2 as one-to-one FinSequence of E1 \/ E2 by FINSEQ_3:98;
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 P = P as Function of Si, REAL ;
A18: (P * h) * e12 = P * (h * (e1 ^ e2)) by RELAT_1:55
.= (P * fe1) ^ (P * fe2) by FINSEQOP:10, A15 ;
A19: ( P * fe1 = Pfe1 & P * fe2 = Pfe2 ) by RELAT_1:55;
reconsider P = P as Function of Sigma, REAL ;
reconsider f1 = f1 as Function of E1,Sigma ;
A21: Product ((P * f1) * e1) = P . (meet (rng (f1 * e1))) by A8, A11, Def3;
reconsider e2 = e2 as one-to-one FinSequence of E2 ;
reconsider f2 = f2 as Function of E2,Sigma ;
P . (a /\ c) = P . (meet ((rng f1) \/ (rng f2))) by SETFAM_1:10, A3, A4
.= P . (meet (rng (fe1 ^ fe2))) by FINSEQ_1:44, A12
.= Product (Pfe1 ^ Pfe2) by A18, A19, A16, A8, Def3, A15
.= (Product Pfe1) * (Product Pfe2) by RVSUM_1:127
.= (P . a) * (P . c) by A3, A4, A12, A21, A10, A11, Def3 ;
hence P . (a /\ c) = (P . a) * (P . c) ; :: thesis: