let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let M1 be sigma_Measure of S1; :: thesis:
let M2 be sigma_Measure of S2; :: thesis:
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis:
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis:
assume that
A1: M1 is sigma_finite and
A3: ( f is nonnegative & A = dom f & f is A -measurable ) ; :: thesis:
set S = sigma (measurable_rectangles (S1,S2));
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
reconsider M = product_sigma_Measure (M1,M2) as sigma_Measure of (sigma (measurable_rectangles (S1,S2))) by MEASUR11:8;
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
consider F being Functional_Sequence of [:X1,X2:],ExtREAL such that
A4: for n being Nat holds
( F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) & dom (F . n) = dom f ) and
A5: for n being Nat holds F . n is nonnegative and
A6: 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 and
A7: for z being Element of [:X1,X2:] st z in dom f holds
( F # z is convergent & lim (F # z) = f . z ) by A3, MESFUNC5:64;

now :: thesis:

let m, n be Nat; :: thesis:
dom (F . m) = dom f by A4;
hence dom (F . m) = dom (F . n) by A4; :: thesis:

end;

then A8: F is with_the_same_dom by MESFUNC8:def 2;
defpred S₁[ Nat, object ] means ex Fy being Function of X2,ExtREAL st
( $2 = Fy & dom Fy = X2 & ( for y1 being Element of X2 st y1 in dom Fy holds
Fy . y1 = Integral (M1,(ProjPMap2 ((F . $1),y1))) ) );
A10: for n being Element of NAT ex FI1 being Element of PFuncs (X2,ExtREAL) st S₁[n,FI1]

proof

let n be Element of NAT ; :: thesis:
deffunc H₁( Element of X2) -> Element of ExtREAL = Integral (M1,(ProjPMap2 ((F . n),$1)));
consider FI1 being Function such that
A11: ( dom FI1 = X2 & ( for y1 being Element of X2 holds FI1 . y1 = H₁(y1) ) ) from FUNCT_1:sch 4();
A12: for y2 being object st y2 in X2 holds
FI1 . y2 in ExtREAL

proof

let y2 be object ; :: thesis:
assume y2 in X2 ; :: thesis:
then reconsider y1 = y2 as Element of X2 ;
FI1 . y2 = Integral (M1,(ProjPMap2 ((F . n),y1))) by A11;
hence FI1 . y2 in ExtREAL ; :: thesis:

end;

then FI1 is Function of X2,ExtREAL by A11, FUNCT_2:3;
then reconsider FI1 = FI1 as Element of PFuncs (X2,ExtREAL) by PARTFUN1:45;
take FI1 ; :: thesis:
reconsider Fy = FI1 as Function of X2,ExtREAL by A12, A11, FUNCT_2:3;
for y1 being Element of X2 st y1 in dom Fy holds
Fy . y1 = Integral (M1,(ProjPMap2 ((F . n),y1))) by A11;
hence ex Fy being Function of X2,ExtREAL st
( FI1 = Fy & dom Fy = X2 & ( for y1 being Element of X2 st y1 in dom Fy holds
Fy . y1 = Integral (M1,(ProjPMap2 ((F . n),y1))) ) ) by A11; :: thesis:

end;

consider FI1 being Function of NAT,(PFuncs (X2,ExtREAL)) such that
A13: for n being Element of NAT holds S₁[n,FI1 . n] from FUNCT_2:sch 3(A10);
A14: for n being Nat holds dom (FI1 . n) = X2

proof

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
then ex Fy being Function of X2,ExtREAL st
( FI1 . n = Fy & dom Fy = X2 & ( for y1 being Element of X2 st y1 in dom Fy holds
Fy . y1 = Integral (M1,(ProjPMap2 ((F . n),y1))) ) ) by A13;
hence dom (FI1 . n) = X2 ; :: thesis:

end;

A15: for n being Nat
for y1 being Element of X2 st y1 in dom (FI1 . n) holds
(FI1 . n) . y1 = Integral (M1,(ProjPMap2 ((F . n),y1)))

proof

let n be Nat; :: thesis:
let y1 be Element of X2; :: thesis:
assume y1 in dom (FI1 . n) ; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
then S₁[n,FI1 . n] by A13;
hence (FI1 . n) . y1 = Integral (M1,(ProjPMap2 ((F . n),y1))) ; :: thesis:

end;

A16: for y1 being Element of X2
for x1 being Element of X1 st x1 in dom (ProjPMap2 (f,y1)) holds
( (ProjPMap2 (F,y1)) # x1 is convergent & lim ((ProjPMap2 (F,y1)) # x1) = (ProjPMap2 (f,y1)) . x1 )

proof

let y1 be Element of X2; :: thesis:
let x1 be Element of X1; :: thesis:
reconsider z1 = [x1,y1] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume x1 in dom (ProjPMap2 (f,y1)) ; :: thesis:
then x1 in Y-section (A,y1) by A3, Def4;
then A17: z1 in dom f by A3, Th25;
then A18: F # z1 is convergent by A7;
A19: for n being Element of NAT holds (F # z1) . n = ((ProjPMap2 (F,y1)) # x1) . n

proof

let n be Element of NAT ; :: thesis:
A20: [x1,y1] in dom (F . n) by A4, A17;
(F # z1) . n = (F . n) . (x1,y1) by MESFUNC5:def 13;
then (F # z1) . n = (ProjPMap2 ((F . n),y1)) . x1 by A20, Def4;
then (F # z1) . n = ((ProjPMap2 (F,y1)) . n) . x1 by Def6;
hence (F # z1) . n = ((ProjPMap2 (F,y1)) # x1) . n by MESFUNC5:def 13; :: thesis:

end;

hence (ProjPMap2 (F,y1)) # x1 is convergent by A18, FUNCT_2:def 8; :: thesis:
F # z1 = (ProjPMap2 (F,y1)) # x1 by A19, FUNCT_2:def 8;
then lim ((ProjPMap2 (F,y1)) # x1) = f . (x1,y1) by A7, A17;
hence lim ((ProjPMap2 (F,y1)) # x1) = (ProjPMap2 (f,y1)) . x1 by A17, Def4; :: thesis:

end;

A21: for y being Element of X2 holds
( lim (ProjPMap2 (F,y)) = ProjPMap2 (f,y) & FI1 # y is convergent & lim (FI1 # y) = Integral (M1,(lim (ProjPMap2 (F,y)))) )

proof

let y be Element of X2; :: thesis:
dom (lim (ProjPMap2 (F,y))) = dom ((ProjPMap2 (F,y)) . 0) by MESFUNC8:def 9;
then dom (lim (ProjPMap2 (F,y))) = dom (ProjPMap2 ((F . 0),y)) by Def6;
then dom (lim (ProjPMap2 (F,y))) = Y-section ((dom (F . 0)),y) by Def4;
then dom (lim (ProjPMap2 (F,y))) = Y-section ((dom f),y) by A4;
then A22: dom (lim (ProjPMap2 (F,y))) = dom (ProjPMap2 (f,y)) by Def4;
for x being Element of X1 st x in dom (lim (ProjPMap2 (F,y))) holds
(lim (ProjPMap2 (F,y))) . x = (ProjPMap2 (f,y)) . x

proof

let x be Element of X1; :: thesis:
assume A23: x in dom (lim (ProjPMap2 (F,y))) ; :: thesis:
then (lim (ProjPMap2 (F,y))) . x = lim ((ProjPMap2 (F,y)) # x) by MESFUNC8:def 9;
hence (lim (ProjPMap2 (F,y))) . x = (ProjPMap2 (f,y)) . x by A16, A22, A23; :: thesis:

end;

hence lim (ProjPMap2 (F,y)) = ProjPMap2 (f,y) by A22, PARTFUN1:5; :: thesis:
A24: (ProjPMap2 (F,y)) . 0 = ProjPMap2 ((F . 0),y) by Def6;
then dom ((ProjPMap2 (F,y)) . 0) = Y-section ((dom (F . 0)),y) by Def4;
then dom ((ProjPMap2 (F,y)) . 0) = Y-section (A,y) by A4, A3;
then A25: dom ((ProjPMap2 (F,y)) . 0) = Measurable-Y-section (A,y) by MEASUR11:def 7;
F . 0 is nonnegative by A5;
then A26: (ProjPMap2 (F,y)) . 0 is nonnegative by A24, Th32;
A27: for n being Nat holds (ProjPMap2 (F,y)) . n is Measurable-Y-section (A,y) -measurable

proof

let n be Nat; :: thesis:
A28: dom (F . n) = A by A3, A4;
F . n is A -measurable by A4, MESFUNC2:34;
then ProjPMap2 ((F . n),y) is Measurable-Y-section (A,y) -measurable by A28, Th47;
hence (ProjPMap2 (F,y)) . n is Measurable-Y-section (A,y) -measurable by Def6; :: thesis:

end;

A29: 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,y)) . n) . x <= ((ProjPMap2 (F,y)) . m) . x

proof

let n, m be Nat; :: thesis:
assume A30: n <= m ; :: thesis:
let x be Element of X1; :: thesis:
assume A31: x in Measurable-Y-section (A,y) ; :: thesis:
then x in dom (ProjPMap2 ((F . 0),y)) by A25, Def6;
then x in Y-section ((dom (F . 0)),y) by Def4;
then x in Y-section ((dom f),y) by A4;
then A32: [x,y] in dom f by Th25;
A33: ( dom ((ProjPMap2 (F,y)) . n) = dom ((ProjPMap2 (F,y)) . 0) & dom ((ProjPMap2 (F,y)) . m) = dom ((ProjPMap2 (F,y)) . 0) ) by A8, Th58, MESFUNC8:def 2;
( (ProjPMap2 (F,y)) . n = ProjPMap2 ((F . n),y) & (ProjPMap2 (F,y)) . m = ProjPMap2 ((F . m),y) ) by Def6;
then ( ((ProjPMap2 (F,y)) . n) . x = (F . n) . (x,y) & ((ProjPMap2 (F,y)) . m) . x = (F . m) . (x,y) ) by A25, A31, A33, Th26;
hence ((ProjPMap2 (F,y)) . n) . x <= ((ProjPMap2 (F,y)) . m) . x by A6, A30, A32; :: thesis:

end;

for x being Element of X1 st x in Measurable-Y-section (A,y) holds
(ProjPMap2 (F,y)) # x is convergent

proof

let x be Element of X1; :: thesis:
assume x in Measurable-Y-section (A,y) ; :: thesis:
then x in Y-section ((dom f),y) by A3, MEASUR11:def 7;
then x in dom (ProjPMap2 (f,y)) by Def4;
hence (ProjPMap2 (F,y)) # x is convergent by A16; :: thesis:

end;

then consider J being ExtREAL_sequence such that
A34: for n being Nat holds J . n = Integral (M1,((ProjPMap2 (F,y)) . n)) and
A35: J is convergent and
A36: Integral (M1,(lim (ProjPMap2 (F,y)))) = lim J by A8, A25, A26, A27, A29, Th58, MESFUNC9:52;
for n being Element of NAT holds J . n = (FI1 # y) . n

proof

let n be Element of NAT ; :: thesis:
A37: dom (FI1 . n) = X2 by A14;
(FI1 # y) . n = (FI1 . n) . y by MESFUNC5:def 13;
then (FI1 # y) . n = Integral (M1,(ProjPMap2 ((F . n),y))) by A15, A37;
then (FI1 # y) . n = Integral (M1,((ProjPMap2 (F,y)) . n)) by Def6;
hence J . n = (FI1 # y) . n by A34; :: thesis:

end;

hence ( FI1 # y is convergent & lim (FI1 # y) = Integral (M1,(lim (ProjPMap2 (F,y)))) ) by A35, A36, FUNCT_2:63; :: thesis:

end;

dom (lim FI1) = dom (FI1 . 0) by MESFUNC8:def 9;
then A38: dom (lim FI1) = X2 by A14;
then reconsider I1 = lim FI1 as Function of X2,ExtREAL by FUNCT_2:def 1;
take I1 ; :: thesis:
for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y)))

proof

let y be Element of X2; :: thesis:
I1 . y = lim (FI1 # y) by A38, MESFUNC8:def 9;
then I1 . y = Integral (M1,(lim (ProjPMap2 (F,y)))) by A21;
hence I1 . y = Integral (M1,(ProjPMap2 (f,y))) by A21; :: thesis:

end;

hence for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ; :: thesis:
thus for V being Element of S2 holds I1 is V -measurable :: thesis:

proof

let V be Element of S2; :: thesis:

now :: thesis:

let m, n be Nat; :: thesis:
( dom (FI1 . m) = X2 & dom (FI1 . n) = X2 ) by A14;
hence dom (FI1 . m) = dom (FI1 . n) ; :: thesis:

end;

then A39: FI1 is with_the_same_dom by MESFUNC8:def 2;
A40: dom (FI1 . 0) = XX2 by A14;
A41: for n being Nat holds FI1 . n is XX2 -measurable

proof

let n be Nat; :: thesis:
( dom (F . n) = A & F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) ) by A4, A3;
then consider L being Function of X2,ExtREAL such that
A42: ( ( for y being Element of X2 holds L . y = Integral (M1,(ProjPMap2 ((F . n),y))) ) & ( for W being Element of S2 holds L is W -measurable ) ) by A1, A5, Lm5;
A43: dom (FI1 . n) = X2 by A14;
then A44: FI1 . n is Function of X2,ExtREAL by FUNCT_2:def 1;
for y being Element of X2 holds (FI1 . n) . y = L . y

proof

let y be Element of X2; :: thesis:
(FI1 . n) . y = Integral (M1,(ProjPMap2 ((F . n),y))) by A15, A43;
hence (FI1 . n) . y = L . y by A42; :: thesis:

end;

then FI1 . n = L by A44, FUNCT_2:63;
hence FI1 . n is XX2 -measurable by A42; :: thesis:

end;

for y being Element of X2 st y in XX2 holds
FI1 # y is convergent by A21;
hence I1 is V -measurable by A39, A40, A41, MESFUNC8:25, MESFUNC1:30; :: thesis:

end;