let Omega1, Omega2 be non empty finite set ; for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let P1 be Probability of Trivial-SigmaField Omega1; for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let P2 be Probability of Trivial-SigmaField Omega2; for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let Q be Function of [:Omega1,Omega2:],REAL; for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let P be Function of (bool [:Omega1,Omega2:]),REAL; ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) implies P . [:Omega1,Omega2:] = 1 )
assume AS:
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) )
; P . [:Omega1,Omega2:] = 1
deffunc H1( set ) -> Element of REAL = P1 . {$1};
P01:
for x being set st x in Omega1 holds
H1(x) in REAL
;
consider F1 being Function of Omega1,REAL such that
P11:
for x being set st x in Omega1 holds
F1 . x = H1(x)
from FUNCT_2:sch 2(P01);
deffunc H2( set ) -> Element of REAL = P2 . {$1};
P02:
for x being set st x in Omega2 holds
H2(x) in REAL
;
consider F2 being Function of Omega2,REAL such that
P21:
for x being set st x in Omega2 holds
F2 . x = H2(x)
from FUNCT_2:sch 2(P02);
Q20f1:
dom (Omega1 --> 1) = Omega1
by FUNCOP_1:19;
rng (Omega1 --> 1) c= REAL
;
then reconsider f1 = Omega1 --> 1 as Function of Omega1,REAL by Q20f1, FUNCT_2:4;
for x being set st x in dom (Omega1 --> 1) holds
(Omega1 --> 1) . x = 1
by FUNCOP_1:13;
then Q3: Integral ((P2M P1),f1) =
(R_EAL 1) * ((P2M P1) . Omega1)
by Q20f1, MESFUNC6:97
.=
1 * (P1 . Omega1)
by EXTREAL1:13
.=
1
by PROB_1:def 13
;
consider G1 being FinSequence of REAL , s1 being FinSequence of Omega1 such that
R1:
( len G1 = card Omega1 & s1 is one-to-one & rng s1 = Omega1 & len s1 = card Omega1 & ( for n being Nat st n in dom G1 holds
G1 . n = (f1 . (s1 . n)) * (P1 . {(s1 . n)}) ) & Integral ((P2M P1),f1) = Sum G1 )
by RANDOM_1:13;
Omega1 c= Omega1
;
then reconsider Y1 = Omega1 as finite Subset of Omega1 ;
dom F1 = Y1
by FUNCT_2:def 1;
then XV2:
dom (F1 * s1) = dom s1
by RELAT_1:46, R1;
XV3: dom G1 =
Seg (len s1)
by R1, FINSEQ_1:def 3
.=
dom s1
by FINSEQ_1:def 3
;
now let x be
set ;
( x in dom G1 implies G1 . x = (F1 * s1) . x )assume XV4:
x in dom G1
;
G1 . x = (F1 * s1) . xthen reconsider nx =
x as
Element of
NAT ;
thus G1 . x =
(f1 . (s1 . nx)) * (P1 . {(s1 . nx)})
by R1, XV4
.=
1
* (P1 . {(s1 . nx)})
by R1, XV3, XV4, FUNCT_1:12, FUNCOP_1:13
.=
F1 . (s1 . nx)
by P11, R1, XV3, XV4, FUNCT_1:12
.=
(F1 * s1) . x
by FUNCT_1:23, XV3, XV4
;
verum end;
then
G1 = Func_Seq (F1,s1)
by XV2, XV3, FUNCT_1:9;
then R4:
setopfunc (Y1,Omega1,REAL,F1,addreal) = 1
by Q3, R1, LMXY092A;
Q20:
dom (Omega2 --> 1) = Omega2
by FUNCOP_1:19;
rng (Omega2 --> 1) c= REAL
;
then reconsider f2 = Omega2 --> 1 as Function of Omega2,REAL by Q20, FUNCT_2:4;
for x being set st x in dom (Omega2 --> 1) holds
(Omega2 --> 1) . x = 1
by FUNCOP_1:13;
then Q3: Integral ((P2M P2),f2) =
(R_EAL 1) * ((P2M P2) . Omega2)
by Q20, MESFUNC6:97
.=
1 * (P2 . Omega2)
by EXTREAL1:13
.=
1
by PROB_1:def 13
;
consider G2 being FinSequence of REAL , s2 being FinSequence of Omega2 such that
R1:
( len G2 = card Omega2 & s2 is one-to-one & rng s2 = Omega2 & len s2 = card Omega2 & ( for n being Nat st n in dom G2 holds
G2 . n = (f2 . (s2 . n)) * (P2 . {(s2 . n)}) ) & Integral ((P2M P2),f2) = Sum G2 )
by RANDOM_1:13;
Omega2 c= Omega2
;
then reconsider Y2 = Omega2 as finite Subset of Omega2 ;
dom F2 = Y2
by FUNCT_2:def 1;
then XV2:
dom (F2 * s2) = dom s2
by RELAT_1:46, R1;
XV3: dom G2 =
Seg (len s2)
by R1, FINSEQ_1:def 3
.=
dom s2
by FINSEQ_1:def 3
;
now let x be
set ;
( x in dom G2 implies G2 . x = (F2 * s2) . x )assume XV4:
x in dom G2
;
G2 . x = (F2 * s2) . xthen reconsider nx =
x as
Element of
NAT ;
thus G2 . x =
(f2 . (s2 . nx)) * (P2 . {(s2 . nx)})
by R1, XV4
.=
1
* (P2 . {(s2 . nx)})
by R1, XV3, XV4, FUNCT_1:12, FUNCOP_1:13
.=
F2 . (s2 . nx)
by P21, R1, XV3, XV4, FUNCT_1:12
.=
(F2 * s2) . x
by FUNCT_1:23, XV3, XV4
;
verum end;
then S4P:
G2 = Func_Seq (F2,s2)
by XV2, XV3, FUNCT_1:9;
reconsider Y3 = [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:] by ZFMISC_1:119;
T1:
now let x,
y be
set ;
( x in Y1 & y in Y2 implies Q . (x,y) = (F1 . x) * (F2 . y) )assume PXYP:
(
x in Y1 &
y in Y2 )
;
Q . (x,y) = (F1 . x) * (F2 . y)hence Q . (
x,
y) =
(P1 . {x}) * (P2 . {y})
by AS
.=
(F1 . x) * (P2 . {y})
by PXYP, P11
.=
(F1 . x) * (F2 . y)
by PXYP, P21
;
verum end;
thus P . [:Omega1,Omega2:] =
setopfunc (Y3,[:Omega1,Omega2:],REAL,Q,addreal)
by AS
.=
(setopfunc (Y1,Omega1,REAL,F1,addreal)) * (setopfunc (Y2,Omega2,REAL,F2,addreal))
by LMXY090, T1
.=
1
by S4P, Q3, R1, LMXY092A, R4
; verum