theorem Th37: :: MESFUN12:37

for X1, X2 being non empty set
for A being Subset of [:X1,X2:]
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for F being Functional_Sequence of [:X1,X2:],ExtREAL st A c= dom f & ( for n being Nat holds dom (F . n) = A ) & ( for z being Element of [:X1,X2:] st z in A holds
( F # z is convergent & lim (F # z) = f . z ) ) holds
( 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) ) ) ) & ex FY being with_the_same_dom Functional_Sequence of X2,ExtREAL st
( ( for n being Nat holds FY . n = ProjPMap1 ((F . n),x) ) & ( 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) ) ) ) )