let X1, X2 be 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) ) ) ) )
let A be 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) ) ) ) )
let f be 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) ) ) ) )
let x be 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) ) ) ) )
let y be 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) ) ) ) )
let F be Functional_Sequence of [:X1,X2:],ExtREAL; ( 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 ) ) implies ( 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) ) ) ) ) )
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 )
; ( 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) ) ) ) )
set f1 = f | A;
A4:
dom (f | A) = A
by A1, RELAT_1:62;
defpred S1[ 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 S1[n,f]
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) ) ) )
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) ) ) )proof
consider FX being
sequence of
(PFuncs (X1,ExtREAL)) such that A6:
for
n being
Element of
NAT holds
S1[
n,
FX . n]
from FUNCT_2:sch 3(A5);
A7:
for
n being
Nat holds
dom (FX . n) = Y-section (
A,
y)
for
m,
n being
Nat holds
dom (FX . m) = dom (FX . n)
then reconsider FX =
FX as
with_the_same_dom Functional_Sequence of
X1,
ExtREAL by MESFUNC8:def 2;
take
FX
;
( ( 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) ) ) )
thus
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) )
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) )
verumproof
let x be
Element of
X1;
( x in Y-section (A,y) implies ( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) ) )
reconsider z =
[x,y] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
assume
x in Y-section (
A,
y)
;
( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) )
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
hence
FX # x is
convergent
by A14, FUNCT_2:63;
(ProjPMap2 (f,y)) . x = lim (FX # x)
(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;
verum
end;
end;
defpred S2[ 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 S2[n,f]
consider FY being sequence of (PFuncs (X2,ExtREAL)) such that
A10:
for n being Element of NAT holds S2[n,FY . n]
from FUNCT_2:sch 3(A9);
A11:
for n being Nat holds dom (FY . n) = X-section (A,x)
for m, n being Nat holds dom (FY . m) = dom (FY . n)
then reconsider FY = FY as with_the_same_dom Functional_Sequence of X2,ExtREAL by MESFUNC8:def 2;
take
FY
; ( ( 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) ) ) )
thus
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) )
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) )
verumproof
let y be
Element of
X2;
( y in X-section (A,x) implies ( FY # y is convergent & (ProjPMap1 (f,x)) . y = lim (FY # y) ) )
reconsider z =
[x,y] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
assume
y in X-section (
A,
x)
;
( FY # y is convergent & (ProjPMap1 (f,x)) . y = lim (FY # y) )
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
hence
FY # y is
convergent
by A18, FUNCT_2:63;
(ProjPMap1 (f,x)) . y = lim (FY # y)
(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;
verum
end;