let Omega1, Omega2 be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 A1: ( ( 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) ) ) ; :: thesis: P . [:Omega1,Omega2:] = 1
deffunc H₁( object ) -> Element of ExtREAL = P1 . {$1};
A2: for x being object st x in Omega1 holds
H₁(x) in REAL by XREAL_0:def 1;
consider F1 being Function of Omega1,REAL such that
A3: for x being object st x in Omega1 holds
F1 . x = H₁(x) from FUNCT_2:sch 2(A2);
deffunc H₂( object ) -> Element of ExtREAL = P2 . {$1};
A4: for x being object st x in Omega2 holds
H₂(x) in REAL by XREAL_0:def 1;
consider F2 being Function of Omega2,REAL such that
A5: for x being object st x in Omega2 holds
F2 . x = H₂(x) from FUNCT_2:sch 2(A4);
A6: dom (Omega1 --> 1) = Omega1 by FUNCOP_1:13;
rng (Omega1 --> 1) c= REAL ;
then reconsider f1 = Omega1 --> 1 as Function of Omega1,REAL by A6, FUNCT_2:2;
for x being object st x in dom (Omega1 --> 1) holds
(Omega1 --> 1) . x = 1 by FUNCOP_1:7;
then A7: Integral ((P2M P1),f1) = jj * ((P2M P1) . Omega1) by A6, MESFUNC6:97
.= 1 * (P1 . Omega1) by EXTREAL1:1
.= 1 by PROB_1:def 8 ;
consider G1 being FinSequence of REAL , s1 being FinSequence of Omega1 such that
A8: ( 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 A9: dom (F1 * s1) = dom s1 by A8, RELAT_1:27;
A10: dom G1 = Seg (len s1) by A8, FINSEQ_1:def 3
.= dom s1 by FINSEQ_1:def 3 ;

now :: thesis: for x being object st x in dom G1 holds
G1 . x = (F1 * s1) . x

let x be object ; :: thesis: ( x in dom G1 implies G1 . x = (F1 * s1) . x )
assume A11: x in dom G1 ; :: thesis: G1 . x = (F1 * s1) . x
then reconsider nx = x as Element of NAT ;
thus G1 . x = (f1 . (s1 . nx)) * (P1 . {(s1 . nx)}) by A8, A11
.= 1 * (P1 . {(s1 . nx)}) by A8, A10, A11, FUNCOP_1:7, FUNCT_1:3
.= F1 . (s1 . nx) by A3, A8, A10, A11, FUNCT_1:3
.= (F1 * s1) . x by A10, A11, FUNCT_1:13 ; :: thesis: verum

end;

then G1 = Func_Seq (F1,s1) by A9, A10, FUNCT_1:2;
then A12: setopfunc (Y1,Omega1,REAL,F1,addreal) = 1 by A7, A8, Th10;
A13: dom (Omega2 --> 1) = Omega2 by FUNCOP_1:13;
rng (Omega2 --> 1) c= REAL ;
then reconsider f2 = Omega2 --> 1 as Function of Omega2,REAL by A13, FUNCT_2:2;
for x being object st x in dom (Omega2 --> 1) holds
(Omega2 --> 1) . x = 1 by FUNCOP_1:7;
then A14: Integral ((P2M P2),f2) = jj * ((P2M P2) . Omega2) by A13, MESFUNC6:97
.= 1 * (P2 . Omega2) by EXTREAL1:1
.= 1 by PROB_1:def 8 ;
consider G2 being FinSequence of REAL , s2 being FinSequence of Omega2 such that
A15: ( 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 A16: dom (F2 * s2) = dom s2 by A15, RELAT_1:27;
A17: dom G2 = Seg (len s2) by A15, FINSEQ_1:def 3
.= dom s2 by FINSEQ_1:def 3 ;

now :: thesis: for x being object st x in dom G2 holds
G2 . x = (F2 * s2) . x

let x be object ; :: thesis: ( x in dom G2 implies G2 . x = (F2 * s2) . x )
assume A18: x in dom G2 ; :: thesis: G2 . x = (F2 * s2) . x
then reconsider nx = x as Element of NAT ;
thus G2 . x = (f2 . (s2 . nx)) * (P2 . {(s2 . nx)}) by A15, A18
.= 1 * (P2 . {(s2 . nx)}) by A15, A17, A18, FUNCOP_1:7, FUNCT_1:3
.= F2 . (s2 . nx) by A5, A15, A17, A18, FUNCT_1:3
.= (F2 * s2) . x by A17, A18, FUNCT_1:13 ; :: thesis: verum

end;

then A19: G2 = Func_Seq (F2,s2) by A16, A17, FUNCT_1:2;
reconsider Y3 = [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:] by ZFMISC_1:96;

A20: now :: thesis: for x, y being set st x in Y1 & y in Y2 holds
Q . (x,y) = (F1 . x) * (F2 . y)

let x, y be set ; :: thesis: ( x in Y1 & y in Y2 implies Q . (x,y) = (F1 . x) * (F2 . y) )
assume A21: ( x in Y1 & y in Y2 ) ; :: thesis: Q . (x,y) = (F1 . x) * (F2 . y)
hence Q . (x,y) = (P1 . {x}) * (P2 . {y}) by A1
.= (F1 . x) * (P2 . {y}) by A21, A3
.= (F1 . x) * (F2 . y) by A21, A5 ;
:: thesis: verum

end;

thus P . [:Omega1,Omega2:] = setopfunc (Y3,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.= (setopfunc (Y1,Omega1,REAL,F1,addreal)) * (setopfunc (Y2,Omega2,REAL,F2,addreal)) by Th12, A20
.= 1 by A19, A14, A15, Th10, A12 ; :: thesis: verum