let S, T be non trivial RealNormSpace; :: thesis: for R being PartFunc of S,T st R is total holds
( R is REST-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 & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
let R be PartFunc of S,T; :: thesis: ( R is total implies ( R is REST-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 & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) ) )
assume A1: R is total ; :: thesis: ( R is REST-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 & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )

A2: now

assume A3: R is REST-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 & ||.z.|| < d & not (||.z.|| ") * ||.(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 & ||.z.|| < d holds
(||.z.|| ") * ||.(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 & ||.z.|| < d & not (||.z.|| ") * ||.(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 & ||.z.|| < d holds
(||.z.|| ") * ||.(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 & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ;
defpred S₁[ Element of 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 S₁[n,z]

proof

let n be Element of NAT ; :: thesis: ex z being Point of S st S₁[n,z]
0 <= n by NAT_1:2;
then 0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
hence ex z being Point of S st S₁[n,z] by A5; :: thesis: verum

end;

consider s being sequence of S such that
A7: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A6);

A8: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < p )
assume A9: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < p
consider n being Element of NAT such that
A10: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by A10, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A9, XREAL_1:76;
then A11: 1 / (n + 1) < p by XCMPLX_1:216;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.((s . m) - (0. S)).|| < p )
assume n <= m ; :: thesis: ||.((s . m) - (0. S)).|| < p
then A12: n + 1 <= m + 1 by XREAL_1:6;
||.(s . m).|| < 1 / (m + 1) by A7;
then A13: ||.((s . m) - (0. S)).|| < 1 / (m + 1) by RLVECT_1:13;
0 <= n by NAT_1:2;
then 1 / (m + 1) <= 1 / (n + 1) by A12, XREAL_1:118;
then ||.((s . m) - (0. S)).|| < 1 / (n + 1) by A13, XXREAL_0:2;
hence ||.((s . m) - (0. S)).|| < p by A11, XXREAL_0:2; :: thesis: verum

end;

then A14: s is convergent by NORMSP_1:def 6;
then A15: lim s = 0. S by A8, NORMSP_1:def 7;
s is non-zero by A7, Th7;
then reconsider s = s as convergent_to_0 sequence of S by A14, A15, Def4;
( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T ) by A3, Def5;
then consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A4, NORMSP_1:def 7;
A17: ||.((((||.s.|| ") (#) (R /* s)) . n) - (0. T)).|| < r by A16;
s . n <> 0. S by A7;
then ||.(s . n).|| <> 0 by NORMSP_0:def 5;
then A18: ||.(s . n).|| > 0 by NORMSP_1:4;
A19: ||.((||.(s . n).|| ") * (R /. (s . n))).|| = (abs (||.(s . n).|| ")) * ||.(R /. (s . n)).|| by NORMSP_1:def 1
.= (||.(s . n).|| ") * ||.(R /. (s . n)).|| by A18, ABSVALUE:def 1 ;
dom R = the carrier of S by A1, PARTFUN1:def 2;
then A20: 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 A20, FUNCT_2:109 ;
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 & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A7, A17, A19; :: thesis: verum

end;

now

assume A21: 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 & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) ; :: thesis: R is REST-like

now

let s be convergent_to_0 sequence of S; :: thesis: ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T )
A22: s is non-zero by Def4;
A23: ( s is convergent & lim s = 0. S ) by Def4;

A24: now

let r be Real; :: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r )
assume r > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r
then consider d being Real such that
A25: d > 0 and
A26: for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r by A21;
consider n being Element of NAT such that
A27: for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < d by A23, A25, NORMSP_1:def 7;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r
thus for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r :: thesis: verum

proof

dom R = the carrier of S by A1, PARTFUN1:def 2;
then A28: rng s c= dom R ;
let m be Element of NAT ; :: thesis: ( n <= m implies ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r )
assume n <= m ; :: thesis: ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r
then ||.((s . m) - (0. S)).|| < d by A27;
then A29: ||.(s . m).|| < d by RLVECT_1:13;
A30: s . m <> 0. S by A22, Th7;
s . m <> 0. S by A22, Th7;
then ||.(s . m).|| <> 0 by NORMSP_0:def 5;
then ||.(s . m).|| > 0 by NORMSP_1:4;
then (||.(s . m).|| ") * ||.(R /. (s . m)).|| = (abs (||.(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 A28, FUNCT_2:109
.= ||.(((||.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 ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A26, A29, A30; :: thesis: verum

end;

end;

hence (||.s.|| ") (#) (R /* s) is convergent by NORMSP_1:def 6; :: thesis: lim ((||.s.|| ") (#) (R /* s)) = 0. T
hence lim ((||.s.|| ") (#) (R /* s)) = 0. T by A24, NORMSP_1:def 7; :: thesis: verum

end;

hence R is REST-like by A1, Def5; :: thesis: verum

end;

hence ( R is REST-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 & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) ) by A2; :: thesis: verum