0.S by A1,Th7; end; hence thesis by Th7; end; definition let S; let x be Point of S; let IT be sequence of S; attr IT is x-convergent means :Def4: IT is convergent & lim IT = x; end; theorem Th18: for X be RealNormSpace for seq be sequence of X holds seq is constant implies ( seq is convergent & for k be Element of NAT holds lim seq = seq.k ) proof let X be RealNormSpace; let seq be sequence of X; assume A1: seq is constant; then consider r be Point of X such that A2: for n be Nat holds seq.n=r by VALUED_0:def 18; thus A3: seq is convergent by A1,LOPBAN_3:12; now let k be Element of NAT; now let p be Real such that A4: 0

0 & pp*||.x0.|| < p
proof
take pp=p/(||.x0.||+1);
A4: ||.x0.||+0 < ||.x0.||+1 & 0 <= ||.x0.|| by NORMSP_1:4,XREAL_1:8;
A5: ||.x0.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
then 0 < p/( ||.x0.||+1 ) by A3,XREAL_1:139;
then pp* ||.x0.|| < pp*(||.x0.|| + 1) by A4,XREAL_1:97;
hence thesis by A3,A5,XCMPLX_1:87;
end;
then consider pp be Real such that
A6: pp > 0 and
A7: pp*||.x0.|| < p;
consider k1 be Nat such that
A8: pp" 0 & pp*||.z.|| < p
proof
take pp=p/(||.z.||+1);
A5: ||.z.||+0 < ||.z.||+1 & 0 <= ||.z.|| by NORMSP_1:4,XREAL_1:8;
A6: ||.z.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
then 0 < p/(||.z.||+1) by A4,XREAL_1:139;
then pp* ||.z.|| < pp*(||.z.|| + 1) by A5,XREAL_1:97;
hence thesis by A4,A6,XCMPLX_1:87;
end;
then consider pp be Real such that
A7: pp > 0 and
A8: pp*||.z.|| < p;
a is convergent & lim a =0;
then consider n be Nat such that
A9: for m be Nat st n <= m holds |.a.m- 0 .| < pp by A7,SEQ_2:def 7;
reconsider n as Nat;
take n;
let m be Nat;
assume n<=m;
then
A10: |.a.m-0 .| < pp by A9;
A11: ||.(a*z).m-0.S.|| = ||.a.m*z - 0.S.|| by Def3
.= ||.a.m*z.|| by RLVECT_1:13
.= |.a.m.|*||.z.|| by NORMSP_1:def 1;
0 <= ||.z.|| by NORMSP_1:4;
then |.a.m.|*||.z.|| <= pp* ||.z.|| by A10,XREAL_1:64;
hence ||.(a*z).m-0.S.||

0.S as sequence of S; take s1; thus thesis; end; end; :: Normed Linear Spaces versions of FDIFF_1 reserve h for (0.S)-convergent sequence of S; reserve c for constant sequence of S; definition let S,T; let IT be PartFunc of S,T; attr IT is RestFunc-like means :Def5: IT is total & for h st h is non-zero holds (||.h.||")(#)(IT /*h) is convergent & lim ((||.h.||")(#)(IT/*h)) = 0.T; end; registration let S,T; cluster RestFunc-like for PartFunc of S,T; existence proof reconsider f = (the carrier of S) --> 0.T as PartFunc of S,T; take f; thus f is total; A1: dom f = the carrier of S by FUNCOP_1:13; now let h ; assume h is non-zero ; now let n be Nat; A2: f/.(h.n) =f.(h.n) by A1,PARTFUN1:def 6 .=0.T by FUNCOP_1:7; A3: rng h c= dom f by A1; A4: n in NAT by ORDINAL1:def 12; thus ((||.h.||")(#)(f/*h)).n = (||.h.||").n*((f/*h).n) by Def2 .= (||.h.||").n*(f/.(h.n)) by A3,A4,FUNCT_2:109 .= 0.T by A2,RLVECT_1:10; end; then (||.h.||")(#)(f/*h) is constant & ((||.h.||")(#)(f/*h)).0 = 0.T by VALUED_0:def 18; hence (||.h.||")(#)(f/*h) is convergent & lim ((||.h.||")(#)(f/*h)) = 0.T by Th18; end; hence thesis; end; end; definition let S,T; mode RestFunc of S,T is RestFunc-like PartFunc of S,T; end; theorem for R be PartFunc of S,T st R is total holds R is RestFunc-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r proof let R be PartFunc of S,T such that A1: R is total; A2: now assume A3: R is RestFunc-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r ); then consider r be Real such that A4: r > 0 and A5: for d be Real st d > 0 ex z be Point of S st z <> 0.S & ||.z .|| < d & not ( ||.z.||"* ||. R/.z .||) < r; defpred P[Nat,Point of S] means $2 <> 0.S & ||.$2.|| < (1/($1+1 )) & not ( ( ||.$2.||"* ||. R/.$2 .||) < r ); A6: for n be Element of NAT ex z be Point of S st P[n,z] proof let n be Element of NAT; 0 < 1 * (n + 1)"; then 0 < 1/(n + 1) by XCMPLX_0:def 9; hence thesis by A5; end; consider s be sequence of S such that A7: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6); A8: for n being Nat holds P[n,s.n] proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A7; end; A9: now let p be Real; assume A10: 0

0.S by A8;
then ||.s.n.|| <> 0 by NORMSP_0:def 5;
then
A19: ||.s.n.|| > 0 by NORMSP_1:4;
A20: ||.(||.s.n.||)"*(R/.(s.n)).|| = |.(||.s.n.||)".| * ||.(R/.(s.n)).||
by NORMSP_1:def 1
.=(||.s.n.||)" * ||.(R/.(s.n)).|| by A19,ABSVALUE:def 1;
dom R = the carrier of S by A1,PARTFUN1:def 2;
then
A21: rng s c= dom R;
||. ((||.s.||")(#)(R/*s)).n- 0.T.|| = ||. ((||.s.||")(#)(R/*s)).n .||
by RLVECT_1:13
.= ||.(||.s.||".n)*((R/*s).n).|| by Def2
.= ||.(||.s.||.n)"*((R/*s).n).|| by VALUED_1:10
.= ||.(||.s.n.||)"*((R/*s).n).|| by NORMSP_0:def 4
.= ||.(||.s.n.||)"*(R/.(s.n)).|| by A21,FUNCT_2:109,A17;
hence
for r be Real
st r > 0 ex d be Real st d > 0 & for z be Point of S st
z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r
by A8,A18,A20;
end;
now
assume
A22: for r be Real st r > 0
ex d be Real st d > 0 & for z be Point of
S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r;
now
let s be (0.S)-convergent sequence of S
such that A23: s is non-zero;
A24: s is convergent & lim s = 0.S by Def4;
A25: now
let r be Real;
assume r > 0;
then consider d be Real such that
A26: d > 0 and
A27: for z be Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||
"* ||. R/.z .||) < r by A22;
consider n be Nat such that
A28: for m be Nat st n <=m holds ||.s.m-0.S.|| < d by A24,A26,
NORMSP_1:def 7;
take n;
thus for m be Nat st n <=m holds ||. ((||.s.||")(#)(R/*s)).
m- 0.T.|| < r
proof
dom R = the carrier of S by A1,PARTFUN1:def 2;
then
A29: rng s c= dom R;
let m be Nat;
A30: m in NAT by ORDINAL1:def 12;
assume n <=m;
then ||.s.m-0.S .|| < d by A28;
then
A31: ||.s.m.|| < d by RLVECT_1:13;
A32: s.m <> 0.S by Th7,A23;
then ||.s.m.|| <> 0 by NORMSP_0:def 5;
then ||.s.m.|| > 0 by NORMSP_1:4;
then
(||.s.m.||)" * ||.(R/.(s.m)).|| =|.(||.s.m.||)".| * ||.(R/.(s.
m)).|| by ABSVALUE:def 1
.= ||.(||.s.m.||)"*(R/.(s.m)).|| by NORMSP_1:def 1
.= ||.(||.s.m.||)"*((R/*s).m).|| by A29,FUNCT_2:109,A30
.= ||.(||.s.||.m)"*((R/*s).m).|| by NORMSP_0:def 4
.= ||.(||.s.||".m)*((R/*s).m).|| by VALUED_1:10
.= ||. ((||.s.||")(#)(R/*s)).m .|| by Def2
.= ||. ((||.s.||")(#)(R/*s)).m- 0.T.|| by RLVECT_1:13;
hence thesis by A27,A31,A32;
end;
end;
hence (||.s.||")(#)(R/*s) is convergent;
hence lim ((||.s.||")(#)(R/*s)) = 0.T by A25,NORMSP_1:def 7;
end;
hence R is RestFunc-like by A1;
end;
hence thesis by A2;
end;
theorem Th24:
for R be RestFunc of S,T for s be (0.S)-convergent sequence of S
st s is non-zero
holds (R/*s) is convergent & lim (R/*s) = 0.T
proof
let R be RestFunc of S,T;
let s be (0.S)-convergent sequence of S
such that A1: s is non-zero ;
A2: (||.s.||") (#) (R/*s) is convergent by Def5,A1;
now
let n be Element of NAT;
s.n <> 0.S by Th7,A1;
then
A3: ||.s.n.|| <> 0 by NORMSP_0:def 5;
thus (||.s.||(#) ( (||.s.||") (#) (R/*s) )).n =||.s.||.n*((||.s.||")(#)(R
/*s)).n by Def2
.=||.s.||.n*((||.s.||").n*((R/*s).n)) by Def2
.= ||.s.n.||*((||.s.||").n*((R/*s).n)) by NORMSP_0:def 4
.= ||.s.n.||*((||.s.||.n)"*((R/*s).n)) by VALUED_1:10
.= ||.s.n.||*((||.s.n.||)"*((R/*s).n)) by NORMSP_0:def 4
.= ||.s.n.||*(||.s.n.||)"*((R/*s).n) by RLVECT_1:def 7
.= 1*(R/*s).n by A3,XCMPLX_0:def 7
.=(R/*s).n by RLVECT_1:def 8;
end;
then
A4: ||.s.||(#) ( (||.s.||") (#) (R/*s) )= (R/*s) by FUNCT_2:63;
A5: s is convergent by Def4;
then
A6: ||.s.|| is convergent by LOPBAN_1:41;
lim s = 0.S by Def4;
then lim ( ||.s.|| ) = ||.0.S.|| by A5,LOPBAN_1:41;
then
A7: lim ( ||.s.|| ) =0 by NORMSP_1:1;
lim ((||.s.||") (#) (R/*s) ) = 0.T by Def5,A1;
then lim (R/*s) = 0* 0.T by A5,A4,A2,A7,Th14,LOPBAN_1:41;
hence thesis by A4,A2,A6,Th13,RLVECT_1:10;
end;
reserve R,R1,R2 for RestFunc of S,T;
reserve L,L1,L2 for Point of R_NormSpace_of_BoundedLinearOperators(S,T);
theorem Th25:
for h1,h2 be PartFunc of S,T for seq be sequence of S holds h1
is total & h2 is total implies (h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq
= h1/*seq - h2/*seq
proof
let h1,h2 be PartFunc of S,T;
let seq be sequence of S;
assume h1 is total & h2 is total;
then h1+h2 is total by VFUNCT_1:32;
then dom (h1+h2) = the carrier of S by PARTFUN1:def 2;
then dom h1 /\ dom h2 = the carrier of S by VFUNCT_1:def 1;
then
A1: rng seq c= dom h1 /\ dom h2;
hence (h1+h2)/*seq = h1/*seq + h2/*seq by NFCONT_1:12;
thus thesis by A1,NFCONT_1:12;
end;
theorem Th26:
for h be PartFunc of S,T for seq be sequence of S for r be Real
holds h is total implies (r(#)h)/*seq = r*(h/*seq)
proof
let h be PartFunc of S,T;
let seq be sequence of S;
let r be Real;
assume h is total;
then dom h = the carrier of S by PARTFUN1:def 2;
then rng seq c= dom h;
hence thesis by NFCONT_1:13;
end;
theorem Th27:
f is_continuous_in x0 iff x0 in dom f & for s1 be sequence of S
st rng s1 c= dom f & s1 is convergent & lim s1=x0 &
(for n being Nat holds s1.n<>x0)
holds f/*s1 is convergent & f/.x0=lim(f/*s1)
proof
thus f is_continuous_in x0 implies x0 in dom f & for s1 be sequence of S st
rng s1 c= dom f & s1 is convergent & lim s1=x0 &
(for n being Nat holds s1.n<>x0) holds f
/*s1 is convergent & f/.x0=lim(f/*s1);
assume that
A1: x0 in dom f and
A2: for s1 st rng s1 c=dom f & s1 is convergent & lim s1=x0 & (for n being Nat
holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1);
thus x0 in dom f by A1;
let s2 be sequence of S such that
A3: rng s2 c=dom f and
A4: s2 is convergent & lim s2=x0;
now
per cases;
suppose
ex n st for m be Element of NAT st n<=m holds s2.m=x0;
then consider N be Element of NAT such that
A5: for m be Element of NAT st N<=m holds s2.m=x0;
A6: for n holds (s2^\N).n=x0
proof
let n;
s2.(n+N)=x0 by A5,NAT_1:12;
hence thesis by NAT_1:def 3;
end;
A7: rng (s2^\N) c= rng s2 by VALUED_0:21;
A8: now
let p be Real such that
A9: p>0;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
A10: m in NAT by ORDINAL1:def 12;
||.(f/*(s2^\N)).m-f/.x0.|| =||.f/.((s2^\N).m)-f/.x0.|| by A3,A7,
FUNCT_2:109,XBOOLE_1:1,A10
.=||.f/.x0-f/.x0.|| by A6,A10
.=||.0.T.|| by RLVECT_1:15
.=0 by NORMSP_1:1;
hence ||.(f/*(s2^\N)).m-f/.x0.||< p by A9;
end;
then
A11: f/*(s2^\N) is convergent;
A12: f/*(s2^\N)=(f/*s2)^\N by A3,VALUED_0:27;
then
A13: f/*s2 is convergent by A11,LOPBAN_3:10;
f/.x0=lim((f/*s2)^\N) by A8,A11,A12,NORMSP_1:def 7;
hence thesis by A13,LOPBAN_3:9;
end;
suppose
A14: for n ex m be Element of NAT st n<=m & s2.m<>x0;
defpred P[Nat,set,set] means for n,m be Element of NAT st $2=
n & $3=m holds n x0;
then consider l be Element of NAT such that
A52: m=F.l by A29,A50;
n<=l by A49,A52,SEQM_3:1;
then ||.(f/*(s2*F)).l-f/.x0.||

Point of R_NormSpace_of_BoundedLinearOperators(S,T) means
:Def7:
ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be Point of
S st x in N holds f/.x-f/.x0 = it.(x-x0) + R/.(x-x0);
existence
by A1;
uniqueness
proof
let LB,LB1 be Point of R_NormSpace_of_BoundedLinearOperators(S,T);
A2: R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider L = LB as Element of BoundedLinearOperators(S,T);
reconsider L1=LB1 as Element of BoundedLinearOperators(S,T) by A2;
assume that
A3: ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be
Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0)+R/.(x-x0) and
A4: ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be
Point of S st x in N holds f/.x-f/.x0 = LB1.(x-x0) + R/.(x-x0);
consider N being Neighbourhood of x0 such that
N c= dom f and
A5: ex R st for x be Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0)
+R /.(x-x0) by A3;
consider R such that
A6: for x be Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0) + R/.(x
-x0) by A5;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A7: ex R st for x be Point of S st x in N1 holds f/.x-f/.x0=LB1.(x-x0
)+ R/.(x-x0) by A4;
consider R1 such that
A8: for x be Point of S st x in N1 holds f/.x-f/.x0 = LB1.(x-x0) + R1
/.(x-x0) by A7;
A9: for z be Point of S holds modetrans(L,S,T).z = modetrans(L1,S,T).z
proof
let z be Point of S;
now
per cases;
case
A10: z= 0.S;
hence modetrans(L,S,T).z =modetrans(L,S,T).(0*z) by RLVECT_1:10
.=0*modetrans(L,S,T).z by LOPBAN_1:def 5
.=0.T by RLVECT_1:10
.=0*modetrans(L1,S,T).z by RLVECT_1:10
.=modetrans(L1,S,T).(0*z) by LOPBAN_1:def 5
.=modetrans(L1,S,T).z by A10,RLVECT_1:10;
end;
case
A11: z<> 0.S;
consider N0 be Neighbourhood of x0 such that
A12: N0 c= N & N0 c= N1 by Th1;
consider g be Real such that
A13: 0