let S, T be RealNormSpace; :: thesis: for R being PartFunc of S,T st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) )

let R be PartFunc of S,T; :: thesis: ( R is total implies ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) ) )

assume A1: R is total ; :: thesis: ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) )

A2: now :: thesis: ( R is RestFunc-like & ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Point of S st
( z <> 0. S & < d & not () * ||.(R /. z).|| < r ) ) ) ) implies for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) )
assume A3: R is RestFunc-like ; :: thesis: ( ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Point of S st
( z <> 0. S & < d & not () * ||.(R /. z).|| < r ) ) ) ) implies for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) )

assume ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Point of S st
( z <> 0. S & < d & not () * ||.(R /. z).|| < r ) ) ) ) ; :: thesis: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) )

then consider r being Real such that
A4: r > 0 and
A5: for d being Real st d > 0 holds
ex z being Point of S st
( z <> 0. S & < d & not () * ||.(R /. z).|| < r ) ;
defpred S1[ Nat, Point of S] means ( \$2 <> 0. S & ||.\$2.|| < 1 / (\$1 + 1) & not (||.\$2.|| ") * ||.(R /. \$2).|| < r );
A6: for n being Element of NAT ex z being Point of S st S1[n,z]
proof
let n be Element of NAT ; :: thesis: ex z being Point of S st S1[n,z]
0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
hence ex z being Point of S st S1[n,z] by A5; :: thesis: verum
end;
consider s being sequence of S such that
A7: for n being Element of NAT holds S1[n,s . n] from A8: for n being Nat holds S1[n,s . n]
proof
let n be Nat; :: thesis: S1[n,s . n]
n in NAT by ORDINAL1:def 12;
hence S1[n,s . n] by A7; :: thesis: verum
end;
A9: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((s . m) - (0. S)).|| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.((s . m) - (0. S)).|| < p )

assume A10: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((s . m) - (0. S)).|| < p

consider n being Nat such that
A11: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by ;
then 1 / (n + 1) < 1 / (p ") by ;
then A12: 1 / (n + 1) < p by XCMPLX_1:216;
reconsider n = n as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.((s . m) - (0. S)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((s . m) - (0. S)).|| < p )
assume n <= m ; :: thesis: ||.((s . m) - (0. S)).|| < p
then A13: n + 1 <= m + 1 by XREAL_1:6;
||.(s . m).|| < 1 / (m + 1) by A8;
then A14: ||.((s . m) - (0. S)).|| < 1 / (m + 1) by RLVECT_1:13;
1 / (m + 1) <= 1 / (n + 1) by ;
then ||.((s . m) - (0. S)).|| < 1 / (n + 1) by ;
hence ||.((s . m) - (0. S)).|| < p by ; :: thesis: verum
end;
then A15: s is convergent ;
then lim s = 0. S by ;
then reconsider s = s as 0. S -convergent sequence of S by ;
s is non-zero by ;
then ( (||.s.|| ") (#) (R /* s) is convergent & lim (() (#) (R /* s)) = 0. T ) by A3;
then consider n being Nat such that
A16: for m being Nat st n <= m holds
||.(((() (#) (R /* s)) . m) - (0. T)).|| < r by ;
A17: n in NAT by ORDINAL1:def 12;
A18: ||.(((() (#) (R /* s)) . n) - (0. T)).|| < r by A16;
s . n <> 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 ;
dom R = the carrier of S by ;
then A21: rng s c= dom R ;
||.(((() (#) (R /* s)) . n) - (0. T)).|| = ||.((() (#) (R /* s)) . n).|| by RLVECT_1:13
.= ||.((() . n) * ((R /* s) . n)).|| by Def2
.= ||.((( . n) ") * ((R /* s) . n)).|| by VALUED_1:10
.= ||.((||.(s . n).|| ") * ((R /* s) . n)).|| by NORMSP_0:def 4
.= ||.((||.(s . n).|| ") * (R /. (s . n))).|| by ;
hence for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) by A8, A18, A20; :: thesis: verum
end;
now :: thesis: ( ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) ) implies R is RestFunc-like )
assume A22: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) ; :: thesis:
now :: thesis: for s being 0. S -convergent sequence of S st s is non-zero holds
( () (#) (R /* s) is convergent & lim (() (#) (R /* s)) = 0. T )
let s be 0. S -convergent sequence of S; :: thesis: ( s is non-zero implies ( () (#) (R /* s) is convergent & lim (() (#) (R /* s)) = 0. T ) )
assume A23: s is non-zero ; :: thesis: ( () (#) (R /* s) is convergent & lim (() (#) (R /* s)) = 0. T )
A24: ( s is convergent & lim s = 0. S ) by Def4;
A25: now :: thesis: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((() (#) (R /* s)) . m) - (0. T)).|| < r
let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
||.(((() (#) (R /* s)) . m) - (0. T)).|| < r )

assume r > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((() (#) (R /* s)) . m) - (0. T)).|| < r

then consider d being Real such that
A26: d > 0 and
A27: for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r by A22;
consider n being Nat such that
A28: for m being Nat st n <= m holds
||.((s . m) - (0. S)).|| < d by ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.(((() (#) (R /* s)) . m) - (0. T)).|| < r

thus for m being Nat st n <= m holds
||.(((() (#) (R /* s)) . m) - (0. T)).|| < r :: thesis: verum
proof
dom R = the carrier of S by ;
then A29: rng s c= dom R ;
let m be Nat; :: thesis: ( n <= m implies ||.(((() (#) (R /* s)) . m) - (0. T)).|| < r )
A30: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: ||.(((() (#) (R /* s)) . m) - (0. T)).|| < r
then ||.((s . m) - (0. S)).|| < d by A28;
then A31: ||.(s . m).|| < d by RLVECT_1:13;
A32: s . m <> 0. S by ;
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
.= ||.((( . m) ") * ((R /* s) . m)).|| by NORMSP_0:def 4
.= ||.((() . m) * ((R /* s) . m)).|| by VALUED_1:10
.= ||.((() (#) (R /* s)) . m).|| by Def2
.= ||.(((() (#) (R /* s)) . m) - (0. T)).|| by RLVECT_1:13 ;
hence ||.(((() (#) (R /* s)) . m) - (0. T)).|| < r by ; :: thesis: verum
end;
end;
hence (||.s.|| ") (#) (R /* s) is convergent ; :: thesis: lim (() (#) (R /* s)) = 0. T
hence lim (() (#) (R /* s)) = 0. T by ; :: thesis: verum
end;
hence R is RestFunc-like by A1; :: thesis: verum
end;
hence ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & < d holds
() * ||.(R /. z).|| < r ) ) ) by A2; :: thesis: verum