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 (M1,(Integral2 (M2,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 (M1,(Integral2 (M2,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 (M1,(Integral2 (M2,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 (M1,(Integral2 (M2,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 (M1,(Integral2 (M2,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 (M1,(Integral2 (M2,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 (M1,(Integral2 (M2,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 (M1,(Integral2 (M2,f)))
set S = sigma (measurable_rectangles (S1,S2));
reconsider XX1 = X1 as Element of S1 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 X1,ExtREAL = Integral2 (M2,(F . $1));
consider G being Functional_Sequence of X1,ExtREAL such that
A11: for n being Nat holds G . n = H₁(n) from SEQFUNC:sch 1();
A12: for n being Nat
for x being Element of X1 holds
( dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (A,x) & ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )

proof

let n be Nat; :: thesis: for x being Element of X1 holds
( dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (A,x) & ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )
let x be Element of X1; :: thesis: ( dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (A,x) & ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )
A13: dom (F . n) = A by A4, A6;
then dom (ProjPMap1 ((F . n),x)) = X-section (A,x) by Def3;
hence dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (A,x) by MEASUR11:def 6; :: thesis: ( ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )
F . n is A -measurable by A6, MESFUNC2:34;
hence ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable by A13, Th47; :: thesis: ProjPMap1 ((F . n),x) is nonnegative
F . n is nonnegative by A6;
hence ProjPMap1 ((F . n),x) is nonnegative by Th32; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( dom (G . n) = XX1 & G . n is XX1 -measurable & G . n is nonnegative )
A15: G . n = Integral2 (M2,(F . n)) by A11;
hence dom (G . n) = XX1 by FUNCT_2:def 1; :: thesis: ( G . n is XX1 -measurable & G . n is nonnegative )
( dom (F . n) = A & F . n is A -measurable ) by A4, A6, MESFUNC2:34;
hence G . n is XX1 -measurable by A2, A15, A6, Th60; :: thesis: G . n is nonnegative

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

let x be object ; :: thesis: ( x in dom (G . n) implies (G . n) . x >= 0 )
assume x in dom (G . n) ; :: thesis: (G . n) . x >= 0
then reconsider x1 = x as Element of X1 ;
( (G . n) . x = Integral (M2,(ProjPMap1 ((F . n),x1))) & ProjPMap1 ((F . n),x1) is Measurable-X-section (A,x1) -measurable & dom (ProjPMap1 ((F . n),x1)) = Measurable-X-section (A,x1) ) by A12, A15, Def8;
hence (G . n) . x >= 0 by A12, MESFUNC5:90; :: thesis: verum

end;

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

end;

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

proof

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

hereby :: thesis: verum

let y be Element of X2; :: thesis: ( y in Measurable-X-section (A,x) implies (ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y )
assume y in Measurable-X-section (A,x) ; :: thesis: (ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y
then y in X-section (A,x) by MEASUR11:def 6;
then y in X-section ((dom (F . n)),x) by A4, A6;
then y in { y where y is Element of X2 : [x,y] in dom (F . n) } by MEASUR11:def 4;
then A18: ex y1 being Element of X2 st
( y1 = y & [x,y1] in dom (F . n) ) ;
then A19: [x,y] in dom f by A6;
then [x,y] in dom (F . m) by A6;
then ( (ProjPMap1 ((F . n),x)) . y = (F . n) . (x,y) & (ProjPMap1 ((F . m),x)) . y = (F . m) . (x,y) ) by A18, Def3;
hence (ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y by A6, A17, A19; :: thesis: verum

end;

end;

A20: for n, m being Nat st n <= m holds
for x being Element of X1 st x in XX1 holds
(G . n) . x <= (G . m) . x

proof

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

hereby :: thesis: verum

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

end;

end;

A25: for x being Element of X1 st x in XX1 holds
( G # x is convergent & lim (G # x) = Integral (M2,(ProjPMap1 (f,x))) )

proof

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

proof

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

end;

consider FX being sequence of (PFuncs (X2,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-X-section (A,x)

proof

let n be Nat; :: thesis: dom (FX . n) = Measurable-X-section (A,x)
n is Element of NAT by ORDINAL1:def 12;
then FX . n = ProjPMap1 ((F . n),x) by A27;
then dom (FX . n) = X-section ((dom (F . n)),x) by Def3;
then dom (FX . n) = X-section (A,x) by A4, A6;
hence dom (FX . n) = Measurable-X-section (A,x) by MEASUR11:def 6; :: 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-X-section (A,x) 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 X2,ExtREAL by MESFUNC8:def 2;
A29: dom (FX . 0) = Measurable-X-section (A,x) by A28;
A30: for n being Nat holds FX . n is Measurable-X-section (A,x) -measurable

proof

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

end;

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

proof

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

end;

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

proof

let y be Element of X2; :: thesis: ( y in Measurable-X-section (A,x) implies ( FX # y is convergent & (ProjPMap1 (f,x)) . y = lim (FX # y) ) )
reconsider z = [x,y] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume y in Measurable-X-section (A,x) ; :: thesis: ( FX # y is convergent & (ProjPMap1 (f,x)) . y = lim (FX # y) )
then y in X-section (A,x) by MEASUR11:def 6;
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 # y) . n = (F # z) . n

proof

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

end;

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

end;

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

proof

let n be Element of NAT ; :: thesis: (G # x) . n = I . n
(G # x) . n = (G . n) . x by MESFUNC5:def 13;
then (G # x) . n = (Integral2 (M2,(F . n))) . x by A11;
then (G # x) . n = Integral (M2,(ProjPMap1 ((F . n),x))) by Def8;
then (G # x) . n = Integral (M2,(FX . n)) by A27;
hence (G # x) . n = I . n by A42; :: thesis: verum

end;

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

proof

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

end;

hence lim (G # x) = Integral (M2,(ProjPMap1 (f,x))) by A44, A45, A36, A42, PARTFUN1:5, MEASUR11:def 6; :: thesis: verum

end;

then A47: for x being Element of X1 st x in XX1 holds
G # x 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) = XX1 & dom (G . m) = XX1 ) 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 = Integral2 (M2,(F . 0)) by A11;
then XX1 = 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 (M1,(G . n)) ) & J is convergent & Integral (M1,(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 (Integral2 (M2,(F . 0))) by A11;
then dom (lim G) = XX1 by FUNCT_2:def 1;
then A50: dom (lim G) = dom (Integral2 (M2,(lim F))) by FUNCT_2:def 1;
for x being Element of X1 st x in dom (lim G) holds
(lim G) . x = (Integral2 (M2,(lim F))) . x

proof

let x be Element of X1; :: thesis: ( x in dom (lim G) implies (lim G) . x = (Integral2 (M2,(lim F))) . x )
assume x in dom (lim G) ; :: thesis: (lim G) . x = (Integral2 (M2,(lim F))) . x
then (lim G) . x = lim (G # x) by MESFUNC8:def 9;
then (lim G) . x = Integral (M2,(ProjPMap1 (f,x))) by A25;
hence (lim G) . x = (Integral2 (M2,(lim F))) . x by A10, Def8; :: thesis: verum

end;

then A51: lim G = Integral2 (M2,(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 (M1,(Integral2 (M2,(F . n)))) by A1, A2, A52, A53, Lm15;
then K . n = Integral (M1,(G . n)) by A11;
hence K . n = J . n by A49; :: thesis: verum

end;

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