let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
let M2 be sigma_Measure of S2; :: thesis: for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is nonnegative and
A4: A = dom f and
A5: f is A -measurable ; :: thesis: Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
set S = sigma (measurable_rectangles (S1,S2));
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
reconsider EX1 = {} as Element of S1 by MEASURE1:7;
Integral ((Prod_Measure (M1,M2)),f) = integral+ ((Prod_Measure (M1,M2)),f) by A3, A4, A5, MESFUNC5:88;
then consider F being Functional_Sequence of [:X1,X2:],ExtREAL, K being ExtREAL_sequence such that
A6: ( ( for n being Nat holds
( F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for z being Element of [:X1,X2:] st z in dom f holds
(F . n) . z <= (F . m) . z ) & ( for z being Element of [:X1,X2:] st z in dom f holds
( F # z is convergent & lim (F # z) = f . z ) ) & ( for n being Nat holds K . n = integral' ((Prod_Measure (M1,M2)),(F . n)) ) ) and
K is convergent and
A7: Integral ((Prod_Measure (M1,M2)),f) = lim K by A3, A4, A5, MESFUNC5:def 15;
dom (F . 0) = dom f by A6;
then A8: dom (lim F) = dom f by MESFUNC8:def 9;
for z being Element of [:X1,X2:] st z in dom (lim F) holds
(lim F) . z = f . z

proof

let z be Element of [:X1,X2:]; :: thesis: ( z in dom (lim F) implies (lim F) . z = f . z )
assume A9: z in dom (lim F) ; :: thesis: (lim F) . z = f . z
hence (lim F) . z = lim (F # z) by MESFUNC8:def 9
.= f . z by A9, A8, A6 ;
:: thesis: verum

end;

then A10: lim F = f by A8, PARTFUN1:5;
deffunc H₁( Nat) -> Function of X2,ExtREAL = Integral1 (M1,(F . $1));
consider G being Functional_Sequence of X2,ExtREAL such that
A11: for n being Nat holds G . n = H₁(n) from SEQFUNC:sch 1();
A12: for n being Nat
for y being Element of X2 holds
( dom (ProjPMap2 ((F . n),y)) = Measurable-Y-section (A,y) & ProjPMap2 ((F . n),y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 ((F . n),y) is nonnegative )

proof

let n be Nat; :: thesis: for y being Element of X2 holds
( dom (ProjPMap2 ((F . n),y)) = Measurable-Y-section (A,y) & ProjPMap2 ((F . n),y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 ((F . n),y) is nonnegative )
let y be Element of X2; :: thesis: ( dom (ProjPMap2 ((F . n),y)) = Measurable-Y-section (A,y) & ProjPMap2 ((F . n),y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 ((F . n),y) is nonnegative )
A13: dom (F . n) = A by A4, A6;
then dom (ProjPMap2 ((F . n),y)) = Y-section (A,y) by Def4;
hence dom (ProjPMap2 ((F . n),y)) = Measurable-Y-section (A,y) by MEASUR11:def 7; :: thesis: ( ProjPMap2 ((F . n),y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 ((F . n),y) is nonnegative )
F . n is A -measurable by A6, MESFUNC2:34;
hence ProjPMap2 ((F . n),y) is Measurable-Y-section (A,y) -measurable by A13, Th47; :: thesis: ProjPMap2 ((F . n),y) is nonnegative
F . n is nonnegative by A6;
hence ProjPMap2 ((F . n),y) is nonnegative by Th32; :: thesis: verum

end;

A14: for n being Nat holds
( dom (G . n) = XX2 & G . n is XX2 -measurable & G . n is nonnegative )

proof

let n be Nat; :: thesis: ( dom (G . n) = XX2 & G . n is XX2 -measurable & G . n is nonnegative )
A15: G . n = Integral1 (M1,(F . n)) by A11;
hence dom (G . n) = XX2 by FUNCT_2:def 1; :: thesis: ( G . n is XX2 -measurable & G . n is nonnegative )
( dom (F . n) = A & F . n is A -measurable ) by A4, A6, MESFUNC2:34;
hence G . n is XX2 -measurable by A1, A15, A6, Th59; :: thesis: G . n is nonnegative

now :: thesis: for y being object st y in dom (G . n) holds
(G . n) . y >= 0

let y be object ; :: thesis: ( y in dom (G . n) implies (G . n) . y >= 0 )
assume y in dom (G . n) ; :: thesis: (G . n) . y >= 0
then reconsider y1 = y as Element of X2 ;
( (G . n) . y = Integral (M1,(ProjPMap2 ((F . n),y1))) & ProjPMap2 ((F . n),y1) is Measurable-Y-section (A,y1) -measurable & dom (ProjPMap2 ((F . n),y1)) = Measurable-Y-section (A,y1) ) by A12, A15, Def7;
hence (G . n) . y >= 0 by A12, MESFUNC5:90; :: thesis: verum

end;

hence G . n is nonnegative by SUPINF_2:52; :: thesis: verum

end;

A16: for y being Element of X2
for n, m being Nat st n <= m holds
for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x

proof

let y be Element of X2; :: thesis: for n, m being Nat st n <= m holds
for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x )
assume A17: n <= m ; :: thesis: for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x

hereby :: thesis: verum

let x be Element of X1; :: thesis: ( x in Measurable-Y-section (A,y) implies (ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x )
assume x in Measurable-Y-section (A,y) ; :: thesis: (ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x
then x in Y-section (A,y) by MEASUR11:def 7;
then x in Y-section ((dom (F . n)),y) by A4, A6;
then x in { x where x is Element of X1 : [x,y] in dom (F . n) } by MEASUR11:def 5;
then A18: ex x1 being Element of X1 st
( x1 = x & [x1,y] in dom (F . n) ) ;
then A19: [x,y] in dom f by A6;
then [x,y] in dom (F . m) by A6;
then ( (ProjPMap2 ((F . n),y)) . x = (F . n) . (x,y) & (ProjPMap2 ((F . m),y)) . x = (F . m) . (x,y) ) by A18, Def4;
hence (ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x by A6, A17, A19; :: thesis: verum

end;

end;

A20: for n, m being Nat st n <= m holds
for y being Element of X2 st y in XX2 holds
(G . n) . y <= (G . m) . y

proof

let n, m be Nat; :: thesis: ( n <= m implies for y being Element of X2 st y in XX2 holds
(G . n) . y <= (G . m) . y )
assume A21: n <= m ; :: thesis: for y being Element of X2 st y in XX2 holds
(G . n) . y <= (G . m) . y

hereby :: thesis: verum

let y be Element of X2; :: thesis: ( y in XX2 implies (G . n) . y <= (G . m) . y )
assume y in XX2 ; :: thesis: (G . n) . y <= (G . m) . y
A22: ( dom (ProjPMap2 ((F . n),y)) = Measurable-Y-section (A,y) & dom (ProjPMap2 ((F . m),y)) = Measurable-Y-section (A,y) & ProjPMap2 ((F . n),y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 ((F . m),y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 ((F . n),y) is nonnegative & ProjPMap2 ((F . m),y) is nonnegative ) by A12;
for x being Element of X1 st x in dom (ProjPMap2 ((F . n),y)) holds
(ProjPMap2 ((F . n),y)) . x <= (ProjPMap2 ((F . m),y)) . x by A16, A21, A22;
then integral+ (M1,(ProjPMap2 ((F . n),y))) <= integral+ (M1,(ProjPMap2 ((F . m),y))) by A22, MESFUNC5:85;
then Integral (M1,(ProjPMap2 ((F . n),y))) <= integral+ (M1,(ProjPMap2 ((F . m),y))) by A22, MESFUNC5:88;
then A23: Integral (M1,(ProjPMap2 ((F . n),y))) <= Integral (M1,(ProjPMap2 ((F . m),y))) by A22, MESFUNC5:88;
(G . n) . y = (Integral1 (M1,(F . n))) . y by A11;
then A24: (G . n) . y = Integral (M1,(ProjPMap2 ((F . n),y))) by Def7;
(G . m) . y = (Integral1 (M1,(F . m))) . y by A11;
hence (G . n) . y <= (G . m) . y by A23, A24, Def7; :: thesis: verum

end;

end;

A25: for y being Element of X2 st y in XX2 holds
( G # y is convergent & lim (G # y) = Integral (M1,(ProjPMap2 (f,y))) )

proof

let y be Element of X2; :: thesis: ( y in XX2 implies ( G # y is convergent & lim (G # y) = Integral (M1,(ProjPMap2 (f,y))) ) )
assume y in XX2 ; :: thesis: ( G # y is convergent & lim (G # y) = Integral (M1,(ProjPMap2 (f,y))) )
defpred S₁[ Element of NAT , object ] means $2 = ProjPMap2 ((F . $1),y);
A26: for n being Element of NAT ex f being Element of PFuncs (X1,ExtREAL) st S₁[n,f]

proof

let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X1,ExtREAL) st S₁[n,f]
reconsider f = ProjPMap2 ((F . n),y) as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
take f ; :: thesis: S₁[n,f]
thus S₁[n,f] ; :: thesis: verum

end;

consider FX being sequence of (PFuncs (X1,ExtREAL)) such that
A27: for n being Element of NAT holds S₁[n,FX . n] from FUNCT_2:sch 3(A26);
A28: for n being Nat holds dom (FX . n) = Measurable-Y-section (A,y)

proof

let n be Nat; :: thesis: dom (FX . n) = Measurable-Y-section (A,y)
n is Element of NAT by ORDINAL1:def 12;
then FX . n = ProjPMap2 ((F . n),y) by A27;
then dom (FX . n) = Y-section ((dom (F . n)),y) by Def4;
then dom (FX . n) = Y-section (A,y) by A4, A6;
hence dom (FX . n) = Measurable-Y-section (A,y) by MEASUR11:def 7; :: thesis: verum

end;

for m, n being Nat holds dom (FX . m) = dom (FX . n)

proof

let m, n be Nat; :: thesis: dom (FX . m) = dom (FX . n)
dom (FX . m) = Measurable-Y-section (A,y) by A28;
hence dom (FX . m) = dom (FX . n) by A28; :: thesis: verum

end;

then reconsider FX = FX as with_the_same_dom Functional_Sequence of X1,ExtREAL by MESFUNC8:def 2;
A29: dom (FX . 0) = Measurable-Y-section (A,y) by A28;
A30: for n being Nat holds FX . n is Measurable-Y-section (A,y) -measurable

proof

let n be Nat; :: thesis: FX . n is Measurable-Y-section (A,y) -measurable
n is Element of NAT by ORDINAL1:def 12;
then A31: FX . n = ProjPMap2 ((F . n),y) by A27;
F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) by A6;
hence FX . n is Measurable-Y-section (A,y) -measurable by A31, Th31, MESFUNC2:34; :: thesis: verum

end;

ProjPMap2 ((F . 0),y) is nonnegative by A12;
then A32: FX . 0 is nonnegative by A27;
A33: for n, m being Nat st n <= m holds
for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(FX . n) . x <= (FX . m) . x

proof

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(FX . n) . x <= (FX . m) . x )
assume A34: n <= m ; :: thesis: for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(FX . n) . x <= (FX . m) . x
( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
then ( FX . n = ProjPMap2 ((F . n),y) & FX . m = ProjPMap2 ((F . m),y) ) by A27;
hence for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(FX . n) . x <= (FX . m) . x by A16, A34; :: thesis: verum

end;

A36: dom (ProjPMap2 (f,y)) = Y-section (A,y) by A4, Def4;
A37: for x being Element of X1 st x in Measurable-Y-section (A,y) holds
( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) )

proof

let x be Element of X1; :: thesis: ( x in Measurable-Y-section (A,y) implies ( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) ) )
reconsider z = [x,y] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume x in Measurable-Y-section (A,y) ; :: thesis: ( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) )
then x in Y-section (A,y) by MEASUR11:def 7;
then A38: [x,y] in dom f by A4, Th25;
then A39: ( F # z is convergent & lim (F # z) = f . z ) by A6;
A40: for n being Element of NAT holds (FX # x) . n = (F # z) . n

proof

let n be Element of NAT ; :: thesis: (FX # x) . n = (F # z) . n
A41: [x,y] in dom (F . n) by A38, A6;
(FX # x) . n = (FX . n) . x by MESFUNC5:def 13;
then (FX # x) . n = (ProjPMap2 ((F . n),y)) . x by A27;
then (FX # x) . n = (F . n) . (x,y) by A41, Def4;
hence (FX # x) . n = (F # z) . n by MESFUNC5:def 13; :: thesis: verum

end;

hence FX # x is convergent by A39, FUNCT_2:63; :: thesis: (ProjPMap2 (f,y)) . x = lim (FX # x)
(ProjPMap2 (f,y)) . x = f . (x,y) by A38, Def4;
hence (ProjPMap2 (f,y)) . x = lim (FX # x) by A39, A40, FUNCT_2:63; :: thesis: verum

end;

then for x being Element of X1 st x in Measurable-Y-section (A,y) holds
FX # x is convergent ;
then consider I being ExtREAL_sequence such that
A42: ( ( for n being Nat holds I . n = Integral (M1,(FX . n)) ) & I is convergent & Integral (M1,(lim FX)) = lim I ) by A29, A30, A32, A33, MESFUNC9:52;
A43: for n being Element of NAT holds (G # y) . n = I . n

proof

let n be Element of NAT ; :: thesis: (G # y) . n = I . n
(G # y) . n = (G . n) . y by MESFUNC5:def 13;
then (G # y) . n = (Integral1 (M1,(F . n))) . y by A11;
then (G # y) . n = Integral (M1,(ProjPMap2 ((F . n),y))) by Def7;
then (G # y) . n = Integral (M1,(FX . n)) by A27;
hence (G # y) . n = I . n by A42; :: thesis: verum

end;

hence G # y is convergent by A42, FUNCT_2:def 8; :: thesis: lim (G # y) = Integral (M1,(ProjPMap2 (f,y)))
A44: G # y = I by A43, FUNCT_2:def 8;
A45: dom (lim FX) = Measurable-Y-section (A,y) by A29, MESFUNC8:def 9;
for x being Element of X1 st x in dom (lim FX) holds
(lim FX) . x = (ProjPMap2 (f,y)) . x

proof

let x be Element of X1; :: thesis: ( x in dom (lim FX) implies (lim FX) . x = (ProjPMap2 (f,y)) . x )
assume A46: x in dom (lim FX) ; :: thesis: (lim FX) . x = (ProjPMap2 (f,y)) . x
then (lim FX) . x = lim (FX # x) by MESFUNC8:def 9;
hence (lim FX) . x = (ProjPMap2 (f,y)) . x by A37, A45, A46; :: thesis: verum

end;

hence lim (G # y) = Integral (M1,(ProjPMap2 (f,y))) by A44, A45, A36, A42, PARTFUN1:5, MEASUR11:def 7; :: thesis: verum

end;

then A47: for y being Element of X2 st y in XX2 holds
G # y is convergent ;

now :: thesis: for n, m being Nat holds dom (G . n) = dom (G . m)

let n, m be Nat; :: thesis: dom (G . n) = dom (G . m)
( dom (G . n) = XX2 & dom (G . m) = XX2 ) by A14;
hence dom (G . n) = dom (G . m) ; :: thesis: verum

end;

then A48: G is with_the_same_dom by MESFUNC8:def 2;
G . 0 = Integral1 (M1,(F . 0)) by A11;
then XX2 = dom (G . 0) by FUNCT_2:def 1;
then consider J being ExtREAL_sequence such that
A49: ( ( for n being Nat holds J . n = Integral (M2,(G . n)) ) & J is convergent & Integral (M2,(lim G)) = lim J ) by A14, A20, A47, A48, MESFUNC9:52;
dom (lim G) = dom (G . 0) by MESFUNC8:def 9;
then dom (lim G) = dom (Integral1 (M1,(F . 0))) by A11;
then dom (lim G) = XX2 by FUNCT_2:def 1;
then A50: dom (lim G) = dom (Integral1 (M1,(lim F))) by FUNCT_2:def 1;
for y being Element of X2 st y in dom (lim G) holds
(lim G) . y = (Integral1 (M1,(lim F))) . y

proof

let y be Element of X2; :: thesis: ( y in dom (lim G) implies (lim G) . y = (Integral1 (M1,(lim F))) . y )
assume y in dom (lim G) ; :: thesis: (lim G) . y = (Integral1 (M1,(lim F))) . y
then (lim G) . y = lim (G # y) by MESFUNC8:def 9;
then (lim G) . y = Integral (M1,(ProjPMap2 (f,y))) by A25;
hence (lim G) . y = (Integral1 (M1,(lim F))) . y by A10, Def7; :: thesis: verum

end;

then A51: lim G = Integral1 (M1,(lim F)) by A50, PARTFUN1:5;
for n being Element of NAT holds K . n = J . n

proof

let n be Element of NAT ; :: thesis: K . n = J . n
A52: A = dom (F . n) by A4, A6;
A53: ( F . n is nonnegative & F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) ) by A6;
K . n = integral' ((Prod_Measure (M1,M2)),(F . n)) by A6;
then K . n = Integral ((Prod_Measure (M1,M2)),(F . n)) by A53, MESFUNC5:89;
then K . n = Integral (M2,(Integral1 (M1,(F . n)))) by A1, A2, A52, A53, Lm15;
then K . n = Integral (M2,(G . n)) by A11;
hence K . n = J . n by A49; :: thesis: verum

end;

hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) by A7, A10, A49, A51, FUNCT_2:def 8; :: thesis: verum