let X1, X2 be non empty set ; :: thesis:
let A be Subset of [:X1,X2:]; :: thesis:
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis:
let x be Element of X1; :: thesis:
let y be Element of X2; :: thesis:
let F be Functional_Sequence of [:X1,X2:],ExtREAL; :: thesis:
assume that
A1: A c= dom f and
A2: for n being Nat holds dom (F . n) = A and
A3: for x being Element of [:X1,X2:] st x in A holds
( F # x is convergent & lim (F # x) = f . x ) ; :: thesis:
set f1 = f | A;
A4: dom (f | A) = A by A1, RELAT_1:62;
defpred S₁[ Element of NAT , object ] means $2 = ProjPMap2 ((F . $1),y);
A5: for n being Element of NAT ex f being Element of PFuncs (X1,ExtREAL) st S₁[n,f]

proof

let n be Element of NAT ; :: thesis:
reconsider f = ProjPMap2 ((F . n),y) as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
take f ; :: thesis:
thus S₁[n,f] ; :: thesis:

end;

thus ex FX being with_the_same_dom Functional_Sequence of X1,ExtREAL st
( ( for n being Nat holds FX . n = ProjPMap2 ((F . n),y) ) & ( 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) ) ) ) :: thesis:

proof

consider FX being sequence of (PFuncs (X1,ExtREAL)) such that
A6: for n being Element of NAT holds S₁[n,FX . n] from FUNCT_2:sch 3(A5);
A7: for n being Nat holds dom (FX . n) = Y-section (A,y)

proof

let n be Nat; :: thesis:
A8: dom (F . n) = dom (f | A) by A2, A4;
n is Element of NAT by ORDINAL1:def 12;
then FX . n = ProjPMap2 ((F . n),y) by A6;
hence dom (FX . n) = Y-section (A,y) by A4, A8, Def4; :: thesis:

end;

for m, n being Nat holds dom (FX . m) = dom (FX . n)

proof

let m, n be Nat; :: thesis:
dom (FX . m) = Y-section (A,y) by A7;
hence dom (FX . m) = dom (FX . n) by A7; :: thesis:

end;

then reconsider FX = FX as with_the_same_dom Functional_Sequence of X1,ExtREAL by MESFUNC8:def 2;
take FX ; :: thesis:
thus for n being Nat holds FX . n = ProjPMap2 ((F . n),y) :: thesis:

proof

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence FX . n = ProjPMap2 ((F . n),y) by A6; :: thesis:

end;

thus 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) ) :: thesis:

proof

let x be Element of X1; :: thesis:
reconsider z = [x,y] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume x in Y-section (A,y) ; :: thesis:
then A13: [x,y] in A by Th25;
then A14: ( F # z is convergent & lim (F # z) = f . z ) by A3;
A15: for n being Element of NAT holds (FX # x) . n = (F # z) . n

proof

let n be Element of NAT ; :: thesis:
A16: [x,y] in dom (F . n) by A2, A13;
(FX # x) . n = (FX . n) . x by MESFUNC5:def 13;
then (FX # x) . n = (ProjPMap2 ((F . n),y)) . x by A6;
then (FX # x) . n = (F . n) . (x,y) by A16, Def4;
hence (FX # x) . n = (F # z) . n by MESFUNC5:def 13; :: thesis:

end;

hence FX # x is convergent by A14, FUNCT_2:63; :: thesis:
(ProjPMap2 (f,y)) . x = f . (x,y) by A1, A13, Def4;
hence (ProjPMap2 (f,y)) . x = lim (FX # x) by A14, A15, FUNCT_2:63; :: thesis:

end;

defpred S₂[ Element of NAT , object ] means $2 = ProjPMap1 ((F . $1),x);
A9: 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:
reconsider f = ProjPMap1 ((F . n),x) as Element of PFuncs (X2,ExtREAL) by PARTFUN1:45;
take f ; :: thesis:
thus S₂[n,f] ; :: thesis:

end;

consider FY being sequence of (PFuncs (X2,ExtREAL)) such that
A10: for n being Element of NAT holds S₂[n,FY . n] from FUNCT_2:sch 3(A9);
A11: for n being Nat holds dom (FY . n) = X-section (A,x)

proof

let n be Nat; :: thesis:
A12: dom (F . n) = dom (f | A) by A2, A4;
n is Element of NAT by ORDINAL1:def 12;
then FY . n = ProjPMap1 ((F . n),x) by A10;
hence dom (FY . n) = X-section (A,x) by A4, A12, Def3; :: thesis:

end;

for m, n being Nat holds dom (FY . m) = dom (FY . n)

proof

let m, n be Nat; :: thesis:
dom (FY . m) = X-section (A,x) by A11;
hence dom (FY . m) = dom (FY . n) by A11; :: thesis:

end;

then reconsider FY = FY as with_the_same_dom Functional_Sequence of X2,ExtREAL by MESFUNC8:def 2;
take FY ; :: thesis:
thus for n being Nat holds FY . n = ProjPMap1 ((F . n),x) :: thesis:

proof

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence FY . n = ProjPMap1 ((F . n),x) by A10; :: thesis:

end;

thus 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) ) :: thesis:

proof

let y be Element of X2; :: thesis:
reconsider z = [x,y] as Element of [:X1,X2:] by ZFMISC_1:def 2;
assume y in X-section (A,x) ; :: thesis:
then A17: [x,y] in A by Th25;
then A18: ( F # z is convergent & lim (F # z) = f . z ) by A3;
A19: for n being Element of NAT holds (FY # y) . n = (F # z) . n

proof

let n be Element of NAT ; :: thesis:
A20: [x,y] in dom (F . n) by A2, A17;
(FY # y) . n = (FY . n) . y by MESFUNC5:def 13;
then (FY # y) . n = (ProjPMap1 ((F . n),x)) . y by A10;
then (FY # y) . n = (F . n) . (x,y) by A20, Def3;
hence (FY # y) . n = (F # z) . n by MESFUNC5:def 13; :: thesis:

end;

hence FY # y is convergent by A18, FUNCT_2:63; :: thesis:
(ProjPMap1 (f,x)) . y = f . (x,y) by A1, A17, Def3;
hence (ProjPMap1 (f,x)) . y = lim (FY # y) by A18, A19, FUNCT_2:63; :: thesis:

end;