let Omega, I be non empty set ; 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; 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; 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; 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; ( 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
; ( 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
; 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; ( 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)
; 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 H1( 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 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 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 H2( 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
( ( S1[i] implies h . i = H2(i) ) & ( not S1[i] implies h . i = H1(i) ) ) ) )
from PARTFUN1:sch 1();
for x being object st x in dom (e1 ^ e2) holds
x in dom (h * (e1 ^ e2))
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 ;
( x in dom (fe1 ^ fe2) implies (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x )
assume A33:
x in dom (fe1 ^ fe2)
;
(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
not
x in dom fe1
;
(fe1 ^ fe2) . x = (h * (e1 ^ e2)) . xthen 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;
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
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
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)
; verum