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_{1}( 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_{1}[ 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_{2}( 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_{1}[i] implies h . i = H_{2}(i) ) & ( not S_{1}[i] implies h . i = H_{1}(i) ) ) ) )
from PARTFUN1:sch 1();

for x being object st x in dom (e1 ^ e2) holds

x in 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

for i being object st i in E1 \/ E2 holds

h . i in Sigma

for i being set st i in E1 \/ E2 holds

h . i in F . i

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

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

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

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

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

for x being object st x in dom (e1 ^ e2) holds

x in dom (h * (e1 ^ e2))

proof

then A30:
dom (e1 ^ e2) c= dom (h * (e1 ^ e2))
;
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;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

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

then A45:
fe1 ^ fe2 = h * (e1 ^ e2)
by A32, FUNCT_1:def 11;
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 ;

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

end;

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

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

for i being object st i in E1 \/ E2 holds

h . i in Sigma

proof

then reconsider h = h as Function of (E1 \/ E2),Sigma by A28, FUNCT_2:3;
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

end;assume A46: i in E1 \/ E2 ; :: thesis: h . i in Sigma

for i being set st i in E1 \/ E2 holds

h . i in F . i

proof

then reconsider h = h as SigmaSection of E1 \/ E2,F by Def4;
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

end;assume A48: i in E1 \/ E2 ; :: thesis: h . i in F . i

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