let R be Function of REAL,REAL; :: thesis: ( R is RestFunc-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
(abs (R . z)) / (abs z) < r ) ) )

A1: 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 Real st
( z <> 0 & abs z < d & not (abs (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
(abs (R . z)) / (abs z) < r ) ) )

assume A2: R is RestFunc-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 (abs (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
(abs (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 (abs (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
(abs (R . z)) / (abs z) < r ) )
then consider r being Real such that
A3: r > 0 and
A4: for d being Real st d > 0 holds
ex z being Real st
( z <> 0 & abs z < d & not (abs (R . z)) / (abs z) < r ) ;
defpred S₁[ Element of NAT , Element of REAL ] means ( $2 <> 0 & abs $2 < 1 / ($1 + 1) & not (abs (R . $2)) / (abs $2) < r );

A5: now :: thesis: for n being Element of NAT ex z being Element of REAL st S₁[n,z]

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 A4; :: thesis: verum

end;

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

A7: now :: thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - 0) < p

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 A8: 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
A9: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by A9, XREAL_1:8;
then A10: 1 / (n + 1) < 1 / (p ") by A8, 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 A6, XXREAL_0:2;
hence abs ((s . m) - 0) < p by A10, XXREAL_0:2; :: thesis: verum

end;

then A11: s is convergent by SEQ_2:def 6;
then A12: lim s = 0 by A7, SEQ_2:def 7;
s is non-zero by A6, SEQ_1:5;
then reconsider s = s as non-zero 0 -convergent Real_Sequence by A11, A12, FDIFF_1:def 1;
( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0 ) by A2, FDIFF_1:def 2;
then consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
abs ((((s ") (#) (R /* s)) . m) - 0) < r by A3, SEQ_2:def 7;
A14: abs ((((s ") (#) (R /* s)) . n) - 0) < r by A13;
A15: abs (((s . n) ") * (R . (s . n))) = (abs ((s . n) ")) * (abs (R . (s . n))) by COMPLEX1:65
.= (abs (R . (s . n))) / (abs (s . n)) by COMPLEX1:66 ;
abs ((((s ") (#) (R /* s)) . n) - 0) = abs (((s ") . n) * ((R /* s) . n)) by SEQ_1:8
.= abs (((s . n) ") * ((R /* s) . n)) by VALUED_1:10
.= abs (((s . n) ") * (R . (s . n))) by FUNCT_2:115 ;
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
(abs (R . z)) / (abs z) < r ) ) by A6, A14, A15; :: thesis: verum

end;

now :: 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
(abs (R . z)) / (abs z) < r ) ) ) implies R is RestFunc-like )

assume A16: 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
(abs (R . z)) / (abs z) < r ) ) ; :: thesis: R is RestFunc-like

now :: thesis: for s being non-zero 0 -convergent Real_Sequence holds
( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0 )

let s be non-zero 0 -convergent Real_Sequence; :: thesis: ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0 )
A17: ( s is convergent & lim s = 0 ) ;

A18: now :: thesis: for r being real number st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((s ") (#) (R /* s)) . m) - 0) < r

let r be real number ; :: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((s ") (#) (R /* s)) . m) - 0) < r )
assume A19: r > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((s ") (#) (R /* s)) . m) - 0) < r
r is Real by XREAL_0:def 1;
then consider d being Real such that
A20: d > 0 and
A21: for z being Real st z <> 0 & abs z < d holds
(abs (R . z)) / (abs z) < r by A19, A16;
consider n being Element of NAT such that
A22: for m being Element of NAT st n <= m holds
abs ((s . m) - 0) < d by A17, A20, SEQ_2:def 7;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((((s ") (#) (R /* s)) . m) - 0) < r

hereby :: thesis: verum

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((s ") (#) (R /* s)) . m) - 0) < r )
assume n <= m ; :: thesis: abs ((((s ") (#) (R /* s)) . m) - 0) < r
then A23: abs ((s . m) - 0) < d by A22;
A24: s . m <> 0 by SEQ_1:5;
(abs (R . (s . m))) / (abs (s . m)) = (abs ((s . m) ")) * (abs (R . (s . m))) by COMPLEX1:66
.= abs (((s . m) ") * (R . (s . m))) by COMPLEX1:65
.= abs (((s . m) ") * ((R /* s) . m)) by FUNCT_2:115
.= abs (((s ") . m) * ((R /* s) . m)) by VALUED_1:10
.= abs ((((s ") (#) (R /* s)) . m) - 0) by SEQ_1:8 ;
hence abs ((((s ") (#) (R /* s)) . m) - 0) < r by A21, A23, A24; :: thesis: verum

end;

end;

hence (s ") (#) (R /* s) is convergent by SEQ_2:def 6; :: thesis: lim ((s ") (#) (R /* s)) = 0
hence lim ((s ") (#) (R /* s)) = 0 by A18, SEQ_2:def 7; :: thesis: verum

end;

hence R is RestFunc-like by FDIFF_1:def 2; :: 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 Real st z <> 0 & abs z < d holds
(abs (R . z)) / (abs z) < r ) ) ) by A1; :: thesis: verum