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
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
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
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
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
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Q be Function of [:Omega1,Omega2:],REAL ; :: thesis: for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let P be Function of (bool [:Omega1,Omega2:]),REAL ; :: thesis: for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y1 be non empty finite Subset of Omega1; :: thesis: for Y2 being non empty finite Subset of Omega2 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y2 be non empty finite Subset of Omega2; :: 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2) )
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 ) ) ; :: thesis: P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
deffunc H₁( set ) -> Element of REAL = P1 . {$1};
P01: for x being set st x in Y1 holds
H₁(x) in REAL ;
consider F1 being Function of Y1,REAL such that
P11: for x being set st x in Y1 holds
F1 . x = H₁(x) from FUNCT_2:sch 2(P01);
deffunc H₂( set ) -> Element of REAL = P2 . {$1};
P02: for x being set st x in Y2 holds
H₂(x) in REAL ;
consider F2 being Function of Y2,REAL such that
P21: for x being set st x in Y2 holds
F2 . x = H₂(x) from FUNCT_2:sch 2(P02);
reconsider O1 = Omega1 as Element of Trivial-SigmaField Omega1 by ZFMISC_1:def 1;

now

let x be set ; :: thesis: ( x in {{} ,1} implies x in REAL )
assume x in {{} ,1} ; :: thesis: x in REAL
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence x in REAL ; :: thesis: verum

end;

then HMY: {{} ,1} c= REAL by TARSKI:def 3;
HMY1: ( dom (chi Y1,Omega1) = Omega1 & rng (chi Y1,Omega1) c= {{} ,1} ) by FUNCT_3:def 3, FUNCT_3:48;
then chi Y1,Omega1 is Function of Omega1,{{} ,1} by FUNCT_2:def 1, RELSET_1:11;
then reconsider f1 = chi Y1,Omega1 as Function of Omega1,REAL by FUNCT_2:9, HMY;
Q20: dom (f1 | Y1) = (dom f1) /\ Y1 by RELAT_1:90
.= Y1 by XBOOLE_1:28, HMY1 ;
for x being set st x in dom (f1 | Y1) holds
(f1 | Y1) . x = 1

proof

let x be set ; :: thesis: ( x in dom (f1 | Y1) implies (f1 | Y1) . x = 1 )
assume ASQ201: x in dom (f1 | Y1) ; :: thesis: (f1 | Y1) . x = 1
then (f1 | Y1) . x = f1 . x by FUNCT_1:70
.= 1 by ASQ201, Q20, FUNCT_3:def 3 ;
hence (f1 | Y1) . x = 1 ; :: thesis: verum

end;

then Q30: Integral (P2M P1),(f1 | Y1) = (R_EAL 1) * ((P2M P1) . (dom (f1 | Y1))) by MESFUNC6:97
.= 1 * (P1 . Y1) by EXTREAL1:13, Q20
.= P1 . Y1 ;
consider G1 being FinSequence of REAL , s1 being FinSequence of Y1 such that
R1: ( len G1 = card Y1 & s1 is one-to-one & rng s1 = Y1 & len s1 = card Y1 & ( for n being Nat st n in dom G1 holds
G1 . n = (f1 . (s1 . n)) * (P1 . {(s1 . n)}) ) & Integral (P2M P1),(f1 | Y1) = Sum G1 ) by RANDOM113;
Y1 c= Y1 ;
then reconsider YY1 = Y1 as finite Subset of Y1 ;
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 ; :: thesis: ( x in dom G1 implies G1 . x = (F1 * s1) . x )
assume XV4: x in dom G1 ; :: thesis: G1 . x = (F1 * s1) . x
then reconsider nx = x as Element of NAT ;
XV6: s1 . nx in Y1 by R1, XV3, XV4, FUNCT_1:12;
thus G1 . x = (f1 . (s1 . nx)) * (P1 . {(s1 . nx)}) by R1, XV4
.= 1 * (P1 . {(s1 . nx)}) by XV6, FUNCT_3:def 3
.= F1 . (s1 . nx) by P11, R1, XV3, XV4, FUNCT_1:12
.= (F1 * s1) . x by FUNCT_1:23, XV3, XV4 ; :: thesis: verum

end;

then G1 = Func_Seq F1,s1 by XV2, XV3, FUNCT_1:9;
then R4: setopfunc YY1,Y1,REAL ,F1,addreal = Sum G1 by R1, LMXY092A;
reconsider O2 = Omega2 as Element of Trivial-SigmaField Omega2 by ZFMISC_1:def 1;
HMY2: ( dom (chi Y2,Omega2) = Omega2 & rng (chi Y2,Omega2) c= {{} ,1} ) by FUNCT_3:def 3, FUNCT_3:48;
then chi Y2,Omega2 is Function of Omega2,{{} ,1} by FUNCT_2:def 1, RELSET_1:11;
then reconsider f2 = chi Y2,Omega2 as Function of Omega2,REAL by FUNCT_2:9, HMY;
Q20: dom (f2 | Y2) = (dom f2) /\ Y2 by RELAT_1:90
.= Y2 by XBOOLE_1:28, HMY2 ;
for x being set st x in dom (f2 | Y2) holds
(f2 | Y2) . x = 1

proof

let x be set ; :: thesis: ( x in dom (f2 | Y2) implies (f2 | Y2) . x = 1 )
assume ASQ201: x in dom (f2 | Y2) ; :: thesis: (f2 | Y2) . x = 1
then (f2 | Y2) . x = f2 . x by FUNCT_1:70
.= 1 by ASQ201, Q20, FUNCT_3:def 3 ;
hence (f2 | Y2) . x = 1 ; :: thesis: verum

end;

then Q3: Integral (P2M P2),(f2 | Y2) = (R_EAL 1) * ((P2M P2) . Y2) by MESFUNC6:97, Q20
.= 1 * (P2 . Y2) by EXTREAL1:13
.= P2 . Y2 ;
consider G2 being FinSequence of REAL , s2 being FinSequence of Y2 such that
RR1: ( len G2 = card Y2 & s2 is one-to-one & rng s2 = Y2 & len s2 = card Y2 & ( for n being Nat st n in dom G2 holds
G2 . n = (f2 . (s2 . n)) * (P2 . {(s2 . n)}) ) & Integral (P2M P2),(f2 | Y2) = Sum G2 ) by RANDOM113;
Y2 c= Y2 ;
then reconsider YY2 = Y2 as finite Subset of Y2 ;
dom F2 = Y2 by FUNCT_2:def 1;
then XV2: dom (F2 * s2) = dom s2 by RELAT_1:46, RR1;
XV3: dom G2 = Seg (len s2) by RR1, FINSEQ_1:def 3
.= dom s2 by FINSEQ_1:def 3 ;

now

let x be set ; :: thesis: ( x in dom G2 implies G2 . x = (F2 * s2) . x )
assume XV4: x in dom G2 ; :: thesis: G2 . x = (F2 * s2) . x
then reconsider nx = x as Element of NAT ;
XV6: s2 . nx in Y2 by RR1, XV3, XV4, FUNCT_1:12;
thus G2 . x = (f2 . (s2 . nx)) * (P2 . {(s2 . nx)}) by RR1, XV4
.= 1 * (P2 . {(s2 . nx)}) by XV6, FUNCT_3:def 3
.= F2 . (s2 . nx) by P21, RR1, XV3, XV4, FUNCT_1:12
.= (F2 * s2) . x by FUNCT_1:23, XV3, XV4 ; :: thesis: verum

end;

then G2 = Func_Seq F2,s2 by XV2, XV3, FUNCT_1:9;
then S4: setopfunc YY2,Y2,REAL ,F2,addreal = Sum G2 by RR1, LMXY092A;
reconsider Y3 = [:Y1,Y2:] as finite Subset of [:Y1,Y2:] by ZFMISC_1:119;
reconsider Y33 = [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:] by ZFMISC_1:119;
Y1Y2O1O2: [:Y1,Y2:] c= [:Omega1,Omega2:] by ZFMISC_1:119;
then reconsider Q0 = Q | [:Y1,Y2:] as Function of [:Y1,Y2:],REAL by FUNCT_2:38;

T1: now

let x, y be set ; :: thesis: ( x in Y1 & y in Y2 implies Q0 . x,y = (F1 . x) * (F2 . y) )
assume PXY0: ( x in Y1 & y in Y2 ) ; :: thesis: Q0 . x,y = (F1 . x) * (F2 . y)
then [x,y] in [:Y1,Y2:] by ZFMISC_1:def 2;
then [x,y] in dom Q0 by FUNCT_2:def 1;
hence Q0 . x,y = Q . x,y by FUNCT_1:70
.= (P1 . {x}) * (P2 . {y}) by AS, PXY0
.= (F1 . x) * (P2 . {y}) by PXY0, P11
.= (F1 . x) * (F2 . y) by PXY0, P21 ;
:: thesis: verum

end;

Y3 c= dom Q0 by FUNCT_2:def 1;
then consider pp1 being FinSequence of [:Y1,Y2:] such that
DY1: ( pp1 is one-to-one & rng pp1 = Y3 & setopfunc Y3,[:Y1,Y2:],REAL ,Q0,addreal = addreal "**" (Func_Seq Q0,pp1) ) by BHSP_5:def 5;
CRPP1: rng pp1 c= [:Omega1,Omega2:] by XBOOLE_1:1, Y1Y2O1O2;
then reconsider pp2 = pp1 as FinSequence of [:Omega1,Omega2:] by FINSEQ_1:def 4;
rng pp1 c= dom Q by CRPP1, FUNCT_2:def 1;
then ZZ1: dom (Q * pp1) = dom pp1 by RELAT_1:46;
DQQQQP: dom Q0 = [:Y1,Y2:] by FUNCT_2:def 1;
for x being set st x in dom (Q0 * pp1) holds
(Q0 * pp1) . x = (Q * pp1) . x

proof

let x be set ; :: thesis: ( x in dom (Q0 * pp1) implies (Q0 * pp1) . x = (Q * pp1) . x )
assume x in dom (Q0 * pp1) ; :: thesis: (Q0 * pp1) . x = (Q * pp1) . x
then ASDQ0: ( (Q0 * pp1) . x = Q0 . (pp1 . x) & x in dom pp1 ) by FUNCT_1:21, FUNCT_1:22;
then pp1 . x in rng pp1 by FUNCT_1:12;
then Q0 . (pp1 . x) = Q . (pp1 . x) by FUNCT_1:72;
hence (Q0 * pp1) . x = (Q * pp1) . x by ASDQ0, FUNCT_1:23; :: thesis: verum

end;

then DY2: Func_Seq Q0,pp1 = Func_Seq Q,pp2 by FUNCT_1:9, DQQQQP, ZZ1, CRPP1, RELAT_1:46;
dom Q = [:Omega1,Omega2:] by FUNCT_2:def 1;
then DY4: setopfunc Y3,[:Y1,Y2:],REAL ,Q0,addreal = setopfunc Y33,[:Omega1,Omega2:],REAL ,Q,addreal by BHSP_5:def 5, DY1, DY2;
thus P . [:Y1,Y2:] = setopfunc Y33,[:Omega1,Omega2:],REAL ,Q,addreal by AS
.= (P1 . Y1) * (P2 . Y2) by Q3, RR1, Q30, R1, S4, R4, LMXY090, T1, DY4 ; :: thesis: verum