let T be non trivial RealNormSpace; :: thesis: for R being PartFunc of REAL,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 Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs z) < r ) ) )
let R be PartFunc of REAL,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 Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs 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 Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs 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 Real st
( z <> 0 & abs z < d & not ||.(R /. z).|| / (abs z) < r ) ) ) ) implies for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs z) < r ) ) )
assume ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Real st
( z <> 0 & abs z < d & not ||.(R /. z).|| / (abs z) < r ) ) ) ) ; :: thesis: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs 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 Real st
( z <> 0 & abs z < d & not ||.(R /. z).|| / (abs z) < r ) ;
defpred S₁[ Element of NAT , Element of REAL ] means ( $2 <> 0 & abs $2 < 1 / ($1 + 1) & not ||.(R /. $2).|| / (abs $2) < r );

A6: now

let n be Element of NAT ; :: thesis: ex z being Element of REAL st S₁[n,z]
1 / (n + 1) is Real by XREAL_0:def 1;
hence ex z being Element of REAL st S₁[n,z] by A5; :: thesis: verum

end;

consider s being Real_Sequence 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 number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - 0) < p )
assume A9: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - 0) < 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 A11: 1 / (n + 1) < 1 / (p ") by A9, XREAL_1:76;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((s . m) - 0) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((s . m) - 0) < p )
assume n <= m ; :: thesis: abs ((s . m) - 0) < p
then n + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
then abs ((s . m) - 0) < 1 / (n + 1) by A7, XXREAL_0:2;
hence abs ((s . m) - 0) < p by A11, XXREAL_0:2; :: thesis: verum

end;

then A14: s is convergent by SEQ_2:def 6;
then A15: lim s = 0 by A8, SEQ_2:def 7;
s is non-empty by A7, SEQ_1:5;
then reconsider s = s as convergent_to_0 Real_Sequence by A14, A15, FDIFF_1:def 1;
( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. T ) by A3, NDIFF_3:def 1;
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;
A19: ||.(((s . n) ") * (R /. (s . n))).|| = (abs ((s . n) ")) * ||.(R /. (s . n)).|| by NORMSP_1:def 1
.= ||.(R /. (s . n)).|| / (abs (s . n)) by COMPLEX1:66 ;
dom R = REAL 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 NDIFF_1:def 2
.= ||.(((s . n) ") * ((R /* s) . n)).|| by VALUED_1:10
.= ||.(((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 Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs 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 Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs z) < r ) ) ; :: thesis: R is REST-like

now

let s be convergent_to_0 Real_Sequence; :: thesis: ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. T )
A22: s is non-empty by FDIFF_1:def 1;
A23: ( s is convergent & lim s = 0 ) by FDIFF_1:def 1;

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 Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs z) < r by A21;
consider n being Element of NAT such that
A27: for m being Element of NAT st n <= m holds
abs ((s . m) - 0) < d by A23, A25, SEQ_2: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 = REAL 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 A29: abs ((s . m) - 0) < d by A27;
A30: s . m <> 0 by A22, SEQ_1:5;
||.(R /. (s . m)).|| / (abs (s . m)) = (abs ((s . m) ")) * ||.(R /. (s . m)).|| by COMPLEX1:66
.= ||.(((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 VALUED_1:10
.= ||.(((s ") (#) (R /* s)) . m).|| by NDIFF_1:def 2
.= ||.((((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, NDIFF_3:def 1; :: 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 Real st z <> 0 & abs z < d holds
||.(R /. z).|| / (abs z) < r ) ) ) by A2; :: thesis: verum