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 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 . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
deffunc H1( object ) -> Element of ExtREAL = P1 . {$1};
A2: for x being object st x in Y1 holds
H1(x) in REAL by XREAL_0:def 1;
consider F1 being Function of Y1,REAL such that
A3: for x being object st x in Y1 holds
F1 . x = H1(x) from FUNCT_2:sch 2(A2);
 deffunc H2( object ) -> Element of ExtREAL = P2 . {$1};
A4: for x being object st x in Y2 holds
H2(x) in REAL by XREAL_0:def 1;
consider F2 being Function of Y2,REAL such that
A5: for x being object st x in Y2 holds
F2 . x = H2(x) from FUNCT_2:sch 2(A4);
 for x being object st x in {{},1} holds
x in REAL by XREAL_0:def 1;
then A6: {{},1} c= REAL ;
A7: ( dom (chi (Y1,Omega1)) = Omega1 & rng (chi (Y1,Omega1)) c= {{},1} ) by FUNCT_3:39, FUNCT_3:def 3;
then chi (Y1,Omega1) is Function of Omega1,{{},1} by FUNCT_2:def 1, RELSET_1:4;
then reconsider f1 = chi (Y1,Omega1) as Function of Omega1,REAL by A6, FUNCT_2:7;
A8: dom (f1 | Y1) = (dom f1) /\ Y1 by RELAT_1:61
.= Y1 by A7, XBOOLE_1:28 ;
for x being object st x in dom (f1 | Y1) holds
(f1 | Y1) . x = 1
proof
let x be object ; :: thesis: ( x in dom (f1 | Y1) implies (f1 | Y1) . x = 1 )
assume A9: x in dom (f1 | Y1) ; :: thesis: (f1 | Y1) . x = 1
then (f1 | Y1) . x = f1 . x by FUNCT_1:47
.= 1 by A9, A8, FUNCT_3:def 3 ;
hence (f1 | Y1) . x = 1 ; :: thesis: verum
end;
then A10: Integral ((P2M P1),(f1 | Y1)) = jj * ((P2M P1) . (dom (f1 | Y1))) by MESFUNC6:97
.= 1 * (P1 . Y1) by A8, EXTREAL1:1
.= P1 . Y1 ;
consider G1 being FinSequence of REAL , s1 being FinSequence of Y1 such that
A11: ( 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 Th15;
Y1 c= Y1 ;
then reconsider YY1 = Y1 as finite Subset of Y1 ;
dom F1 = Y1 by FUNCT_2:def 1;
then A12: dom (F1 * s1) = dom s1 by A11, RELAT_1:27;
A13: dom G1 = Seg (len s1) by A11, 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 A14: x in dom G1 ; :: thesis: G1 . x = (F1 * s1) . x
then reconsider nx = x as Element of NAT ;
A15: s1 . nx in Y1 by A11, A13, A14, FUNCT_1:3;
thus G1 . x = (f1 . (s1 . nx)) * (P1 . {(s1 . nx)}) by A11, A14
.= 1 * (P1 . {(s1 . nx)}) by A15, FUNCT_3:def 3
.= F1 . (s1 . nx) by A3, A11, A13, A14, FUNCT_1:3
.= (F1 * s1) . x by A13, A14, FUNCT_1:13 ; :: thesis: verum
end;
then G1 = Func_Seq (F1,s1) by A12, A13, FUNCT_1:2;
then A16: setopfunc (YY1,Y1,REAL,F1,addreal) = Sum G1 by A11, Th10;
A17: ( dom (chi (Y2,Omega2)) = Omega2 & rng (chi (Y2,Omega2)) c= {{},1} ) by FUNCT_3:39, FUNCT_3:def 3;
then chi (Y2,Omega2) is Function of Omega2,{{},1} by FUNCT_2:def 1, RELSET_1:4;
then reconsider f2 = chi (Y2,Omega2) as Function of Omega2,REAL by A6, FUNCT_2:7;
A18: dom (f2 | Y2) = (dom f2) /\ Y2 by RELAT_1:61
.= Y2 by A17, XBOOLE_1:28 ;
for x being object st x in dom (f2 | Y2) holds
(f2 | Y2) . x = 1
proof
let x be object ; :: thesis: ( x in dom (f2 | Y2) implies (f2 | Y2) . x = 1 )
assume A19: x in dom (f2 | Y2) ; :: thesis: (f2 | Y2) . x = 1
then (f2 | Y2) . x = f2 . x by FUNCT_1:47
.= 1 by A19, A18, FUNCT_3:def 3 ;
hence (f2 | Y2) . x = 1 ; :: thesis: verum
end;
then A20: Integral ((P2M P2),(f2 | Y2)) = jj * ((P2M P2) . Y2) by A18, MESFUNC6:97
.= 1 * (P2 . Y2) by EXTREAL1:1
.= P2 . Y2 ;
consider G2 being FinSequence of REAL , s2 being FinSequence of Y2 such that
A21: ( 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 Th15;
Y2 c= Y2 ;
then reconsider YY2 = Y2 as finite Subset of Y2 ;
dom F2 = Y2 by FUNCT_2:def 1;
then A22: dom (F2 * s2) = dom s2 by A21, RELAT_1:27;
A23: dom G2 = Seg (len s2) by A21, 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 A24: x in dom G2 ; :: thesis: G2 . x = (F2 * s2) . x
then reconsider nx = x as Element of NAT ;
A25: s2 . nx in Y2 by A21, A23, A24, FUNCT_1:3;
thus G2 . x = (f2 . (s2 . nx)) * (P2 . {(s2 . nx)}) by A21, A24
.= 1 * (P2 . {(s2 . nx)}) by A25, FUNCT_3:def 3
.= F2 . (s2 . nx) by A5, A21, A23, A24, FUNCT_1:3
.= (F2 * s2) . x by A23, A24, FUNCT_1:13 ; :: thesis: verum
end;
then G2 = Func_Seq (F2,s2) by A22, A23, FUNCT_1:2;
then A26: setopfunc (YY2,Y2,REAL,F2,addreal) = Sum G2 by A21, Th10;
reconsider Y3 = [:Y1,Y2:] as finite Subset of [:Y1,Y2:] by ZFMISC_1:96;
reconsider Y33 = [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:] by ZFMISC_1:96;
A27: [:Y1,Y2:] c= [:Omega1,Omega2:] by ZFMISC_1:96;
then reconsider Q0 = Q | [:Y1,Y2:] as Function of [:Y1,Y2:],REAL by FUNCT_2:32;
A28: now :: thesis: for x, y being set st x in Y1 & y in Y2 holds
Q0 . (x,y) = (F1 . x) * (F2 . y)
let x, y be set ; :: thesis: ( x in Y1 & y in Y2 implies Q0 . (x,y) = (F1 . x) * (F2 . y) )
assume A29: ( 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:47
.= (P1 . {x}) * (P2 . {y}) by A1, A29
.= (F1 . x) * (P2 . {y}) by A29, A3
.= (F1 . x) * (F2 . y) by A29, A5 ;
:: thesis: verum
end;
consider pp1 being FinSequence of [:Y1,Y2:] such that
A30: ( 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;
A31: rng pp1 c= [:Omega1,Omega2:] by A27;
then reconsider pp2 = pp1 as FinSequence of [:Omega1,Omega2:] by FINSEQ_1:def 4;
rng pp1 c= dom Q by A31, FUNCT_2:def 1;
then A32: dom (Q * pp1) = dom pp1 by RELAT_1:27;
A33: dom Q0 = [:Y1,Y2:] by FUNCT_2:def 1;
for x being object st x in dom (Q0 * pp1) holds
(Q0 * pp1) . x = (Q * pp1) . x
proof
let x be object ; :: 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 A34: ( (Q0 * pp1) . x = Q0 . (pp1 . x) & x in dom pp1 ) by FUNCT_1:11, FUNCT_1:12;
then pp1 . x in rng pp1 by FUNCT_1:3;
then Q0 . (pp1 . x) = Q . (pp1 . x) by FUNCT_1:49;
hence (Q0 * pp1) . x = (Q * pp1) . x by A34, FUNCT_1:13; :: thesis: verum
end;
then A35: Func_Seq (Q0,pp1) = Func_Seq (Q,pp2) by A33, A32, A31, FUNCT_1:2, RELAT_1:27;
A36: setopfunc (Y3,[:Y1,Y2:],REAL,Q0,addreal) = setopfunc (Y33,[:Omega1,Omega2:],REAL,Q,addreal) by A30, A35, BHSP_5:def 5;
thus P . [:Y1,Y2:] = setopfunc (Y33,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.= (P1 . Y1) * (P2 . Y2) by A20, A21, A10, A11, A26, A16, Th12, A28, A36 ; :: thesis: verum