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 & f is nonpositive & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
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 & f is nonpositive & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
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 & f is nonpositive & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
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 & f is nonpositive & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
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 & f is nonpositive & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & f is nonpositive & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( M1 is sigma_finite & f is nonpositive & A = dom f & f is A -measurable implies ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) ) )
assume that
A1: M1 is sigma_finite and
A3: ( f is nonpositive & A = dom f & f is A -measurable ) ; :: thesis: ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
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 nonpositive 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, MESFUN11:56;
now :: thesis: for m, n being Nat holds dom (F . m) = dom (F . n)
let m, n be Nat; :: thesis: dom (F . m) = dom (F . n)
dom (F . m) = dom f by A4;
hence dom (F . m) = dom (F . n) by A4; :: thesis: verum
end;
then A8: F is with_the_same_dom by MESFUNC8:def 2;
defpred S1[ 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 S1[n,FI1]
proof
let n be Element of NAT ; :: thesis: ex FI1 being Element of PFuncs (X2,ExtREAL) st S1[n,FI1]
deffunc H1( 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 = H1(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: ( y2 in X2 implies FI1 . y2 in ExtREAL )
assume y2 in X2 ; :: thesis: FI1 . y2 in ExtREAL
then reconsider y1 = y2 as Element of X2 ;
FI1 . y2 = Integral (M1,(ProjPMap2 ((F . n),y1))) by A11;
hence FI1 . y2 in ExtREAL ; :: thesis: verum
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: S1[n,FI1]
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: verum
end;
consider FI1 being Function of NAT,(PFuncs (X2,ExtREAL)) such that
A13: for n being Element of NAT holds S1[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: dom (FI1 . n) = X2
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: verum
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: for y1 being Element of X2 st y1 in dom (FI1 . n) holds
(FI1 . n) . y1 = Integral (M1,(ProjPMap2 ((F . n),y1)))
let y1 be Element of X2; :: thesis: ( y1 in dom (FI1 . n) implies (FI1 . n) . y1 = Integral (M1,(ProjPMap2 ((F . n),y1))) )
assume y1 in dom (FI1 . n) ; :: thesis: (FI1 . n) . y1 = Integral (M1,(ProjPMap2 ((F . n),y1)))
n is Element of NAT by ORDINAL1:def 12;
then S1[n,FI1 . n] by A13;
hence (FI1 . n) . y1 = Integral (M1,(ProjPMap2 ((F . n),y1))) ; :: thesis: verum
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: 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 )
let x1 be Element of X1; :: thesis: ( x1 in dom (ProjPMap2 (f,y1)) implies ( (ProjPMap2 (F,y1)) # x1 is convergent & lim ((ProjPMap2 (F,y1)) # x1) = (ProjPMap2 (f,y1)) . x1 ) )
reconsider z1 = [x1,y1] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume x1 in dom (ProjPMap2 (f,y1)) ; :: thesis: ( (ProjPMap2 (F,y1)) # x1 is convergent & lim ((ProjPMap2 (F,y1)) # x1) = (ProjPMap2 (f,y1)) . x1 )
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: (F # z1) . n = ((ProjPMap2 (F,y1)) # x1) . n
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: verum
end;
hence (ProjPMap2 (F,y1)) # x1 is convergent by A18, FUNCT_2:def 8; :: thesis: lim ((ProjPMap2 (F,y1)) # x1) = (ProjPMap2 (f,y1)) . x1
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: verum
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: ( lim (ProjPMap2 (F,y)) = ProjPMap2 (f,y) & FI1 # y is convergent & lim (FI1 # y) = Integral (M1,(lim (ProjPMap2 (F,y)))) )
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: ( x in dom (lim (ProjPMap2 (F,y))) implies (lim (ProjPMap2 (F,y))) . x = (ProjPMap2 (f,y)) . x )
assume A23: x in dom (lim (ProjPMap2 (F,y))) ; :: thesis: (lim (ProjPMap2 (F,y))) . x = (ProjPMap2 (f,y)) . x
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: verum
end;
hence lim (ProjPMap2 (F,y)) = ProjPMap2 (f,y) by A22, PARTFUN1:5; :: thesis: ( FI1 # y is convergent & lim (FI1 # y) = Integral (M1,(lim (ProjPMap2 (F,y)))) )
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 nonpositive by A5;
then A26: (ProjPMap2 (F,y)) . 0 is nonpositive by A24, Th33;
A27: for n being Nat holds (ProjPMap2 (F,y)) . n is Measurable-Y-section (A,y) -measurable
proof
let n be Nat; :: thesis: (ProjPMap2 (F,y)) . n is Measurable-Y-section (A,y) -measurable
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: verum
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: ( n <= m implies 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 )
assume A30: n <= m ; :: thesis: 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
let x be Element of X1; :: thesis: ( x in Measurable-Y-section (A,y) implies ((ProjPMap2 (F,y)) . n) . x >= ((ProjPMap2 (F,y)) . m) . x )
assume A31: x in Measurable-Y-section (A,y) ; :: thesis: ((ProjPMap2 (F,y)) . n) . x >= ((ProjPMap2 (F,y)) . m) . x
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: verum
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: ( x in Measurable-Y-section (A,y) implies (ProjPMap2 (F,y)) # x is convergent )
assume x in Measurable-Y-section (A,y) ; :: thesis: (ProjPMap2 (F,y)) # x is convergent
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: verum
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, MESFUN11:74;
for n being Element of NAT holds J . n = (FI1 # y) . n
proof
let n be Element of NAT ; :: thesis: J . n = (FI1 # y) . n
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: verum
end;
hence ( FI1 # y is convergent & lim (FI1 # y) = Integral (M1,(lim (ProjPMap2 (F,y)))) ) by A35, A36, FUNCT_2:63; :: thesis: verum
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))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )
for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y)))
proof
let y be Element of X2; :: thesis: I1 . y = Integral (M1,(ProjPMap2 (f,y)))
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: verum
end;
hence for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ; :: thesis: for V being Element of S2 holds I1 is V -measurable
thus for V being Element of S2 holds I1 is V -measurable :: thesis: verum
proof
let V be Element of S2; :: thesis: I1 is V -measurable
now :: thesis: for m, n being Nat holds dom (FI1 . m) = dom (FI1 . n)
let m, n be Nat; :: thesis: dom (FI1 . m) = dom (FI1 . n)
( dom (FI1 . m) = X2 & dom (FI1 . n) = X2 ) by A14;
hence dom (FI1 . m) = dom (FI1 . n) ; :: thesis: verum
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: FI1 . n is XX2 -measurable
( 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 = L . y
(FI1 . n) . y = Integral (M1,(ProjPMap2 ((F . n),y))) by A15, A43;
hence (FI1 . n) . y = L . y by A42; :: thesis: verum
end;
then FI1 . n = L by A44, FUNCT_2:63;
hence FI1 . n is XX2 -measurable by A42; :: thesis: verum
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: verum
end;