let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )
let S2 be SigmaField of X2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for x being Element of X1
for y being Element of X2
for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )
let x be Element of X1; :: thesis: for y being Element of X2
for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )
let y be Element of X2; :: thesis: for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable implies ( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable ) )
assume that
A1: ( f is nonnegative or f is nonpositive ) and
A2: A c= dom f and
A3: f is A -measurable ; :: thesis: ( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )
reconsider X12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider S = sigma (measurable_rectangles (S1,S2)) as SigmaField of [:X1,X2:] ;
set f1 = f | A;
A4: dom (f | A) = A by A2, RELAT_1:62;
A = (dom f) /\ A by A2, XBOOLE_1:28;
then A5: f | A is A -measurable by A3, MESFUNC5:42;
A6: ( Measurable-X-section (A,x) = X-section (A,x) & Measurable-Y-section (A,y) = Y-section (A,y) ) by MEASUR11:def 6, MEASUR11:def 7;
A7: ( dom (ProjPMap1 (f,x)) = X-section ((dom f),x) & dom (ProjPMap1 ((f | A),x)) = X-section (A,x) ) by A4, Def3;
B7: ( dom (ProjPMap2 (f,y)) = Y-section ((dom f),y) & dom (ProjPMap2 ((f | A),y)) = Y-section (A,y) ) by A4, Def4;
P1: ex F being Functional_Sequence of [:X1,X2:],ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) ) & ( for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) ) )

proof

per cases ( f is nonnegative or f is nonpositive ) by A1;

suppose f is nonnegative ; :: thesis: ex F being Functional_Sequence of [:X1,X2:],ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) ) & ( for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) ) )

then ex F being Functional_Sequence of [:X1,X2:],ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of [:X1,X2:] st x in dom (f | A) holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) ) ) by A4, A5, MESFUNC5:15, MESFUNC5:64;
hence ex F being Functional_Sequence of [:X1,X2:],ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) ) & ( for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) ) ) ; :: thesis: verum

end;

suppose f is nonpositive ; :: thesis: ex F being Functional_Sequence of [:X1,X2:],ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) ) & ( for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) ) )

then ex F being Functional_Sequence of [:X1,X2:],ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) ) & ( for n being Nat holds F . n is nonpositive ) & ( for n, m being Nat st n <= m holds
for x being Element of [:X1,X2:] st x in dom (f | A) holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) ) ) by A4, A5, MESFUN11:1, MESFUN11:56;
hence ex F being Functional_Sequence of [:X1,X2:],ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) ) & ( for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) ) ) ; :: thesis: verum

end;

end;

end;

consider F being Functional_Sequence of [:X1,X2:],ExtREAL such that
A8: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | A) ) and
A9: for x being Element of [:X1,X2:] st x in dom (f | A) holds
( F # x is convergent & lim (F # x) = (f | A) . x ) by P1;
A10: for z being Element of [:X1,X2:] st z in A holds
( F # z is convergent & lim (F # z) = f . z )

proof

let z be Element of [:X1,X2:]; :: thesis: ( z in A implies ( F # z is convergent & lim (F # z) = f . z ) )
assume A11: z in A ; :: thesis: ( F # z is convergent & lim (F # z) = f . z )
hence F # z is convergent by A4, A9; :: thesis: lim (F # z) = f . z
thus lim (F # z) = (f | A) . z by A4, A9, A11
.= f . z by A11, FUNCT_1:49 ; :: thesis: verum

end;

consider FY being with_the_same_dom Functional_Sequence of X2,ExtREAL such that
A12: for n being Nat holds FY . n = ProjPMap1 ((F . n),x) and
A13: for y being Element of X2 st y in X-section (A,x) holds
( FY # y is convergent & (ProjPMap1 (f,x)) . y = lim (FY # y) ) by A2, A4, A8, A10, Th37;
for n being Nat holds dom (FY . n) = X-section (A,x)

proof

let n be Nat; :: thesis: dom (FY . n) = X-section (A,x)
( FY . n = ProjPMap1 ((F . n),x) & dom (F . n) = A ) by A4, A8, A12;
hence dom (FY . n) = X-section (A,x) by Def3; :: thesis: verum

end;

then A14: dom (FY . 0) = Measurable-X-section (A,x) by A6;
A15: for n being Nat holds FY . n is Measurable-X-section (A,x) -measurable

proof

let n be Nat; :: thesis: FY . n is Measurable-X-section (A,x) -measurable
( FY . n = ProjPMap1 ((F . n),x) & F . n is_simple_func_in S ) by A8, A12;
hence FY . n is Measurable-X-section (A,x) -measurable by Th31, MESFUNC2:34; :: thesis: verum

end;

A16: X-section (A,x) c= dom (ProjPMap1 (f,x)) by A2, A7, MEASUR11:20;
A17: for y being Element of X2 st y in Measurable-X-section (A,x) holds
( FY # y is convergent & (ProjPMap1 ((f | A),x)) . y = lim (FY # y) )

proof

let y be Element of X2; :: thesis: ( y in Measurable-X-section (A,x) implies ( FY # y is convergent & (ProjPMap1 ((f | A),x)) . y = lim (FY # y) ) )
reconsider z = [x,y] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume A18: y in Measurable-X-section (A,x) ; :: thesis: ( FY # y is convergent & (ProjPMap1 ((f | A),x)) . y = lim (FY # y) )
hence FY # y is convergent by A6, A13; :: thesis: (ProjPMap1 ((f | A),x)) . y = lim (FY # y)
ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) by Th34;
then (ProjPMap1 ((f | A),x)) . y = (ProjPMap1 (f,x)) . y by A6, A18, FUNCT_1:49;
hence (ProjPMap1 ((f | A),x)) . y = lim (FY # y) by A6, A13, A18; :: thesis: verum

end;

ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) by Th34;
then (ProjPMap1 ((f | A),x)) | (Measurable-X-section (A,x)) = (ProjPMap1 (f,x)) | (Measurable-X-section (A,x)) by A6;
hence ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable by A6, A7, A14, A15, A16, A17, Th36, MESFUNC8:26; :: thesis: ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable
consider FX being with_the_same_dom Functional_Sequence of X1,ExtREAL such that
A19: for n being Nat holds FX . n = ProjPMap2 ((F . n),y) and
A20: for x being Element of X1 st x in Y-section (A,y) holds
( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) ) by A2, A4, A8, A10, Th37;
for n being Nat holds dom (FX . n) = Y-section (A,y)

proof

let n be Nat; :: thesis: dom (FX . n) = Y-section (A,y)
( FX . n = ProjPMap2 ((F . n),y) & dom (F . n) = A ) by A4, A8, A19;
hence dom (FX . n) = Y-section (A,y) by Def4; :: thesis: verum

end;

then A21: dom (FX . 0) = Measurable-Y-section (A,y) by A6;
A22: 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
( FX . n = ProjPMap2 ((F . n),y) & F . n is_simple_func_in S ) by A8, A19;
hence FX . n is Measurable-Y-section (A,y) -measurable by Th31, MESFUNC2:34; :: thesis: verum

end;

A23: Y-section (A,y) c= dom (ProjPMap2 (f,y)) by A2, B7, MEASUR11:21;
A24: for x being Element of X1 st x in Measurable-Y-section (A,y) holds
( FX # x is convergent & (ProjPMap2 ((f | A),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 | A),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 | A),y)) . x = lim (FX # x) )
then A25: x in Y-section (A,y) by MEASUR11:def 7;
hence FX # x is convergent by A20; :: thesis: (ProjPMap2 ((f | A),y)) . x = lim (FX # x)
ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) by Th34;
then (ProjPMap2 ((f | A),y)) . x = (ProjPMap2 (f,y)) . x by A25, FUNCT_1:49;
hence (ProjPMap2 ((f | A),y)) . x = lim (FX # x) by A25, A20; :: thesis: verum

end;

ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) by Th34;
then (ProjPMap2 ((f | A),y)) | (Measurable-Y-section (A,y)) = (ProjPMap2 (f,y)) | (Measurable-Y-section (A,y)) by A6;
hence ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable by A6, B7, A21, A22, A23, A24, Th36, MESFUNC8:26; :: thesis: verum