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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable implies ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) ) )
assume that
A1: M2 is sigma_finite and
A3: ( f is nonnegative & A = dom f & f is A -measurable ) ; :: thesis: ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 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 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: 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 Fx being Function of X1,ExtREAL st
( $2 = Fx & dom Fx = X1 & ( for x1 being Element of X1 st x1 in dom Fx holds
Fx . x1 = Integral (M2,(ProjPMap1 ((F . $1),x1))) ) );
A10: for n being Element of NAT ex FI2 being Element of PFuncs (X1,ExtREAL) st S1[n,FI2]
proof
let n be Element of NAT ; :: thesis: ex FI2 being Element of PFuncs (X1,ExtREAL) st S1[n,FI2]
deffunc H1( Element of X1) -> Element of ExtREAL = Integral (M2,(ProjPMap1 ((F . n),$1)));
consider FI2 being Function such that
A11: ( dom FI2 = X1 & ( for x1 being Element of X1 holds FI2 . x1 = H1(x1) ) ) from FUNCT_1:sch 4();
 A12: for x2 being object st x2 in X1 holds
FI2 . x2 in ExtREAL
proof
let x2 be object ; :: thesis: ( x2 in X1 implies FI2 . x2 in ExtREAL )
assume x2 in X1 ; :: thesis: FI2 . x2 in ExtREAL
then reconsider x1 = x2 as Element of X1 ;
FI2 . x2 = Integral (M2,(ProjPMap1 ((F . n),x1))) by A11;
hence FI2 . x2 in ExtREAL ; :: thesis: verum
end;
then FI2 is Function of X1,ExtREAL by A11, FUNCT_2:3;
then reconsider FI2 = FI2 as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
take FI2 ; :: thesis: S1[n,FI2]
reconsider Fx = FI2 as Function of X1,ExtREAL by A12, A11, FUNCT_2:3;
for x1 being Element of X1 st x1 in dom Fx holds
Fx . x1 = Integral (M2,(ProjPMap1 ((F . n),x1))) by A11;
hence ex Fx being Function of X1,ExtREAL st
( FI2 = Fx & dom Fx = X1 & ( for x1 being Element of X1 st x1 in dom Fx holds
Fx . x1 = Integral (M2,(ProjPMap1 ((F . n),x1))) ) ) by A11; :: thesis: verum
end;
consider FI2 being Function of NAT,(PFuncs (X1,ExtREAL)) such that
A13: for n being Element of NAT holds S1[n,FI2 . n] from FUNCT_2:sch 3(A10);
 A14: for n being Nat holds dom (FI2 . n) = X1
proof
let n be Nat; :: thesis: dom (FI2 . n) = X1
n is Element of NAT by ORDINAL1:def 12;
then ex Fx being Function of X1,ExtREAL st
( FI2 . n = Fx & dom Fx = X1 & ( for x1 being Element of X1 st x1 in dom Fx holds
Fx . x1 = Integral (M2,(ProjPMap1 ((F . n),x1))) ) ) by A13;
hence dom (FI2 . n) = X1 ; :: thesis: verum
end;
A15: for n being Nat
for x1 being Element of X1 st x1 in dom (FI2 . n) holds
(FI2 . n) . x1 = Integral (M2,(ProjPMap1 ((F . n),x1)))
proof
let n be Nat; :: thesis: for x1 being Element of X1 st x1 in dom (FI2 . n) holds
(FI2 . n) . x1 = Integral (M2,(ProjPMap1 ((F . n),x1)))
let x1 be Element of X1; :: thesis: ( x1 in dom (FI2 . n) implies (FI2 . n) . x1 = Integral (M2,(ProjPMap1 ((F . n),x1))) )
assume x1 in dom (FI2 . n) ; :: thesis: (FI2 . n) . x1 = Integral (M2,(ProjPMap1 ((F . n),x1)))
n is Element of NAT by ORDINAL1:def 12;
then S1[n,FI2 . n] by A13;
hence (FI2 . n) . x1 = Integral (M2,(ProjPMap1 ((F . n),x1))) ; :: thesis: verum
end;
A16: for x1 being Element of X1
for y1 being Element of X2 st y1 in dom (ProjPMap1 (f,x1)) holds
( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 )
proof
let x1 be Element of X1; :: thesis: for y1 being Element of X2 st y1 in dom (ProjPMap1 (f,x1)) holds
( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 )
let y1 be Element of X2; :: thesis: ( y1 in dom (ProjPMap1 (f,x1)) implies ( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 ) )
reconsider z1 = [x1,y1] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume y1 in dom (ProjPMap1 (f,x1)) ; :: thesis: ( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 )
then y1 in X-section (A,x1) by A3, Def3;
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 = ((ProjPMap1 (F,x1)) # y1) . n
proof
let n be Element of NAT ; :: thesis: (F # z1) . n = ((ProjPMap1 (F,x1)) # y1) . 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 = (ProjPMap1 ((F . n),x1)) . y1 by A20, Def3;
then (F # z1) . n = ((ProjPMap1 (F,x1)) . n) . y1 by Def5;
hence (F # z1) . n = ((ProjPMap1 (F,x1)) # y1) . n by MESFUNC5:def 13; :: thesis: verum
end;
hence (ProjPMap1 (F,x1)) # y1 is convergent by A18, FUNCT_2:def 8; :: thesis: lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1
F # z1 = (ProjPMap1 (F,x1)) # y1 by A19, FUNCT_2:def 8;
then lim ((ProjPMap1 (F,x1)) # y1) = f . (x1,y1) by A7, A17;
hence lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 by A17, Def3; :: thesis: verum
end;
A21: for x being Element of X1 holds
( lim (ProjPMap1 (F,x)) = ProjPMap1 (f,x) & FI2 # x is convergent & lim (FI2 # x) = Integral (M2,(lim (ProjPMap1 (F,x)))) )
proof
let x be Element of X1; :: thesis: ( lim (ProjPMap1 (F,x)) = ProjPMap1 (f,x) & FI2 # x is convergent & lim (FI2 # x) = Integral (M2,(lim (ProjPMap1 (F,x)))) )
dom (lim (ProjPMap1 (F,x))) = dom ((ProjPMap1 (F,x)) . 0) by MESFUNC8:def 9;
then dom (lim (ProjPMap1 (F,x))) = dom (ProjPMap1 ((F . 0),x)) by Def5;
then dom (lim (ProjPMap1 (F,x))) = X-section ((dom (F . 0)),x) by Def3;
then dom (lim (ProjPMap1 (F,x))) = X-section ((dom f),x) by A4;
then A22: dom (lim (ProjPMap1 (F,x))) = dom (ProjPMap1 (f,x)) by Def3;
for y being Element of X2 st y in dom (lim (ProjPMap1 (F,x))) holds
(lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y
proof
let y be Element of X2; :: thesis: ( y in dom (lim (ProjPMap1 (F,x))) implies (lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y )
assume A23: y in dom (lim (ProjPMap1 (F,x))) ; :: thesis: (lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y
then (lim (ProjPMap1 (F,x))) . y = lim ((ProjPMap1 (F,x)) # y) by MESFUNC8:def 9;
hence (lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y by A16, A22, A23; :: thesis: verum
end;
hence lim (ProjPMap1 (F,x)) = ProjPMap1 (f,x) by A22, PARTFUN1:5; :: thesis: ( FI2 # x is convergent & lim (FI2 # x) = Integral (M2,(lim (ProjPMap1 (F,x)))) )
A24: (ProjPMap1 (F,x)) . 0 = ProjPMap1 ((F . 0),x) by Def5;
then dom ((ProjPMap1 (F,x)) . 0) = X-section ((dom (F . 0)),x) by Def3;
then dom ((ProjPMap1 (F,x)) . 0) = X-section (A,x) by A4, A3;
then A25: dom ((ProjPMap1 (F,x)) . 0) = Measurable-X-section (A,x) by MEASUR11:def 6;
F . 0 is nonnegative by A5;
then A26: (ProjPMap1 (F,x)) . 0 is nonnegative by A24, Th32;
A27: for n being Nat holds (ProjPMap1 (F,x)) . n is Measurable-X-section (A,x) -measurable
proof
let n be Nat; :: thesis: (ProjPMap1 (F,x)) . n is Measurable-X-section (A,x) -measurable
A28: dom (F . n) = A by A3, A4;
F . n is A -measurable by A4, MESFUNC2:34;
then ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable by A28, Th47;
hence (ProjPMap1 (F,x)) . n is Measurable-X-section (A,x) -measurable by Def5; :: thesis: verum
end;
A29: 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,x)) . n) . y <= ((ProjPMap1 (F,x)) . 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
((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y )
assume A30: n <= m ; :: thesis: for y being Element of X2 st y in Measurable-X-section (A,x) holds
((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y
let y be Element of X2; :: thesis: ( y in Measurable-X-section (A,x) implies ((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y )
assume A31: y in Measurable-X-section (A,x) ; :: thesis: ((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y
then y in dom (ProjPMap1 ((F . 0),x)) by A25, Def5;
then y in X-section ((dom (F . 0)),x) by Def3;
then y in X-section ((dom f),x) by A4;
then A32: [x,y] in dom f by Th25;
A33: ( dom ((ProjPMap1 (F,x)) . n) = dom ((ProjPMap1 (F,x)) . 0) & dom ((ProjPMap1 (F,x)) . m) = dom ((ProjPMap1 (F,x)) . 0) ) by A8, Th58, MESFUNC8:def 2;
( (ProjPMap1 (F,x)) . n = ProjPMap1 ((F . n),x) & (ProjPMap1 (F,x)) . m = ProjPMap1 ((F . m),x) ) by Def5;
then ( ((ProjPMap1 (F,x)) . n) . y = (F . n) . (x,y) & ((ProjPMap1 (F,x)) . m) . y = (F . m) . (x,y) ) by A25, A31, A33, Th26;
hence ((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y by A6, A30, A32; :: thesis: verum
end;
for y being Element of X2 st y in Measurable-X-section (A,x) holds
(ProjPMap1 (F,x)) # y is convergent
proof
let y be Element of X2; :: thesis: ( y in Measurable-X-section (A,x) implies (ProjPMap1 (F,x)) # y is convergent )
assume y in Measurable-X-section (A,x) ; :: thesis: (ProjPMap1 (F,x)) # y is convergent
then y in X-section ((dom f),x) by A3, MEASUR11:def 6;
then y in dom (ProjPMap1 (f,x)) by Def3;
hence (ProjPMap1 (F,x)) # y is convergent by A16; :: thesis: verum
end;
then consider J being ExtREAL_sequence such that
A34: for n being Nat holds J . n = Integral (M2,((ProjPMap1 (F,x)) . n)) and
A35: J is convergent and
A36: Integral (M2,(lim (ProjPMap1 (F,x)))) = lim J by A8, A25, A26, A27, A29, Th58, MESFUNC9:52;
for n being Element of NAT holds J . n = (FI2 # x) . n
proof
let n be Element of NAT ; :: thesis: J . n = (FI2 # x) . n
A37: dom (FI2 . n) = X1 by A14;
(FI2 # x) . n = (FI2 . n) . x by MESFUNC5:def 13;
then (FI2 # x) . n = Integral (M2,(ProjPMap1 ((F . n),x))) by A15, A37;
then (FI2 # x) . n = Integral (M2,((ProjPMap1 (F,x)) . n)) by Def5;
hence J . n = (FI2 # x) . n by A34; :: thesis: verum
end;
hence ( FI2 # x is convergent & lim (FI2 # x) = Integral (M2,(lim (ProjPMap1 (F,x)))) ) by A35, A36, FUNCT_2:63; :: thesis: verum
end;
dom (lim FI2) = dom (FI2 . 0) by MESFUNC8:def 9;
then A38: dom (lim FI2) = X1 by A14;
then reconsider I2 = lim FI2 as Function of X1,ExtREAL by FUNCT_2:def 1;
take I2 ; :: thesis: ( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x)))
proof
let x be Element of X1; :: thesis: I2 . x = Integral (M2,(ProjPMap1 (f,x)))
I2 . x = lim (FI2 # x) by A38, MESFUNC8:def 9;
then I2 . x = Integral (M2,(lim (ProjPMap1 (F,x)))) by A21;
hence I2 . x = Integral (M2,(ProjPMap1 (f,x))) by A21; :: thesis: verum
end;
hence for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ; :: thesis: for V being Element of S1 holds I2 is V -measurable
thus for V being Element of S1 holds I2 is V -measurable :: thesis: verum
proof
let V be Element of S1; :: thesis: I2 is V -measurable
now :: thesis: for m, n being Nat holds dom (FI2 . m) = dom (FI2 . n)
let m, n be Nat; :: thesis: dom (FI2 . m) = dom (FI2 . n)
( dom (FI2 . m) = X1 & dom (FI2 . n) = X1 ) by A14;
hence dom (FI2 . m) = dom (FI2 . n) ; :: thesis: verum
end;
then A39: FI2 is with_the_same_dom by MESFUNC8:def 2;
A40: dom (FI2 . 0) = XX1 by A14;
A41: for n being Nat holds FI2 . n is XX1 -measurable
proof
let n be Nat; :: thesis: FI2 . n is XX1 -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 X1,ExtREAL such that
A42: ( ( for x being Element of X1 holds L . x = Integral (M2,(ProjPMap1 ((F . n),x))) ) & ( for W being Element of S1 holds L is W -measurable ) ) by A1, A5, Lm6;
A43: dom (FI2 . n) = X1 by A14;
then A44: FI2 . n is Function of X1,ExtREAL by FUNCT_2:def 1;
for x being Element of X1 holds (FI2 . n) . x = L . x
proof
let x be Element of X1; :: thesis: (FI2 . n) . x = L . x
(FI2 . n) . x = Integral (M2,(ProjPMap1 ((F . n),x))) by A15, A43;
hence (FI2 . n) . x = L . x by A42; :: thesis: verum
end;
then FI2 . n = L by A44, FUNCT_2:63;
hence FI2 . n is XX1 -measurable by A42; :: thesis: verum
end;
for x being Element of X1 st x in XX1 holds
FI2 # x is convergent by A21;
hence I2 is V -measurable by A39, A40, A41, MESFUNC8:25, MESFUNC1:30; :: thesis: verum
end;