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 A3, Def9;
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 A4, Def9;
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 A11, WELLORD2:def 4;
A15: e2 <> {} by A14;
reconsider e2 = e2 as Function of (Seg m),E2 by A13, A14, FUNCT_2:1;
A16: e2 is FinSequence by A13, FINSEQ_1:def 2;
A17: rng (f2 * e2) = rng f2 by A14, FUNCT_2:14;
reconsider e2 = e2 as one-to-one FinSequence of E2 by A12, A14, A16, FINSEQ_1:def 4;
reconsider f2 = f2 as Function of E2,Si ;
deffunc H₁( object ) -> set = f2 . $1;
reconsider fe2 = f2 * e2 as FinSequence of Si ;
rng e2 = dom f2 by A14, FUNCT_2:def 1;
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 S₁[ 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 A20, WELLORD2:def 4;
A24: e1 <> {} by A23;
reconsider e1 = e1 as Function of (Seg n),E1 by A22, A23, FUNCT_2:1;
A25: e1 is FinSequence by A22, FINSEQ_1:def 2;
A26: rng (f1 * e1) = rng f1 by A23, FUNCT_2:14;
reconsider e1 = e1 as one-to-one FinSequence of E1 by A21, A23, A25, FINSEQ_1:def 4;
reconsider f1 = f1 as Function of E1,Si ;
deffunc H₂( object ) -> set = f1 . $1;
reconsider fe1 = f1 * e1 as FinSequence of Si ;
rng e1 = dom f1 by A23, FUNCT_2:def 1;
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
( ( S₁[i] implies h . i = H₂(i) ) & ( not S₁[i] implies h . i = H₁(i) ) ) ) ) from PARTFUN1:sch 1();
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 A23, A14, A28, FINSEQ_1:31;
then (e1 ^ e2) . x in dom h by A29, FUNCT_1:3;
hence x in dom (h * (e1 ^ e2)) by A29, FUNCT_1:11; :: 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 A27, A18, FINSEQ_1:def 7
.= dom (h * (e1 ^ e2)) by A31, A30 ;
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 A34, FUNCT_1:11;
then e1 . x in E1 by A23, FUNCT_1:3;
then h . (e1 . x) = f1 . (e1 . x) by A28, A36;
then A38: (fe1 ^ fe2) . x = h . (e1 . x) by A34, A35, FUNCT_1:12;
(e1 ^ e2) . x = e1 . x by A37, FINSEQ_1:def 7;
hence (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by A32, A33, A38, FUNCT_1:12; :: 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 A33, FINSEQ_1:25;
A41: n in dom e2 by A39, FUNCT_1:11;
then A42: e2 . n in E2 by A14, FUNCT_1:3;
E1 /\ E2 c= J /\ K by A5, A8, XBOOLE_1:27;
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 A42, XBOOLE_0:def 5;
A44: E2 c= E1 \/ E2 by XBOOLE_1:7;
(fe1 ^ fe2) . x = fe2 . n by A39, A40, FINSEQ_1:def 7
.= f2 . (e2 . n) by A39, FUNCT_1:12
.= h . (e2 . n) by A28, A42, A43, A44
.= h . ((e1 ^ e2) . x) by A27, A40, A41, FINSEQ_1:def 7 ;
hence (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by A32, A33, FUNCT_1:12; :: thesis: verum

end;

end;

end;

then A45: fe1 ^ fe2 = h * (e1 ^ e2) by A32, FUNCT_1:def 11;
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 A28, A46;
hence h . i in Sigma by A47, FUNCT_2:5; :: thesis: verum

end;

suppose not i in E1 ; :: thesis: h . i in Sigma

then ( h . i = f2 . i & i in E2 ) by A28, A46, XBOOLE_0:def 3;
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 A28, FUNCT_2:3;
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 A28, A48, A49; :: thesis: verum

end;

suppose A50: not i in E1 ; :: thesis: h . i in F . i

then i in E2 by A48, XBOOLE_0:def 3;
then f2 . i in F . i by Def4;
hence h . i in F . i by A28, A48, A50; :: 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 A19, FINSEQ_1:def 4;
reconsider e1 = e1 as FinSequence of E1 \/ E2 by A52, FINSEQ_1:def 4;
E1 /\ E2 c= J /\ K by A5, A8, XBOOLE_1:27;
then E1 /\ E2 c= {} by A2;
then E1 /\ E2 = {} ;
then rng e1 misses rng e2 by A23, A14;
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 A45, FINSEQOP:9 ;
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 A24, A7;
P . (a /\ c) = P . (meet ((rng f1) \/ (rng f2))) by A6, A9, SETFAM_1:9
.= P . (meet (rng (fe1 ^ fe2))) by A26, A17, FINSEQ_1:31
.= 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