let R be PartFunc of REAL,REAL; :: 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 Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(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 Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) ) )
thus ( R is RestFunc-like implies for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. 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 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) ) ) implies R is RestFunc-like )

proof

assume A2: R is RestFunc-like ; :: thesis: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) )
given 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 & |.z.| < d & not (|.z.| ") * |.(R /. z).| < r ) ; :: thesis: contradiction
defpred S₁[ Nat, Real] means ( $2 <> 0 & |.$2.| < 1 / ($1 + 1) & not (|.$2.| ") * |.(R /. $2).| < r );
A5: for n being Element of NAT ex z being Element of REAL st S₁[n,z]

proof

let n be Element of NAT ; :: thesis: ex z being Element of REAL st S₁[n,z]
reconsider d = 1 / (n + 1) as Element of REAL by XREAL_0:def 1;
d <> 0 by XCMPLX_1:50;
then consider z being Real such that
A6: ( z <> 0 & |.z.| < d & not (|.z.| ") * |.(R /. z).| < r ) by A4;
reconsider z = z as Element of REAL by XREAL_0:def 1;
take z ; :: thesis: S₁[n,z]
thus S₁[n,z] by A6; :: 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(A5);
A8: for n being Nat holds S₁[n,s . n]

proof

let n be Nat; :: thesis: S₁[n,s . n]
n in NAT by ORDINAL1:def 12;
hence S₁[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).| < 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).| < p )
assume A10: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - 0).| < p
consider n being Nat such that
A11: p " < n by SEQ_4:3;
reconsider q0 = 0 , q1 = 1 as Real ;
(p ") + q0 < n + q1 by A11, XREAL_1:8;
then A12: 1 / (n + 1) < 1 / (p ") by A10, XREAL_1:76;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((s . m) - 0).| < p
let m be Nat; :: thesis: ( n <= m implies |.((s . m) - 0).| < p )
A13: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((s . m) - 0).| < p
then A14: n + 1 <= m + 1 by XREAL_1:6;
1 / (m + 1) <= 1 / (n + 1) by A14, XREAL_1:118;
then A15: |.((s . m) - 0).| < 1 / (n + 1) by A7, XXREAL_0:2, A13;
1 / (p ") = p by XCMPLX_1:216;
hence |.((s . m) - 0).| < p by A12, A15, XXREAL_0:2; :: thesis: verum

end;

A16: s is convergent by A9, SEQ_2:def 6;
then lim s = 0 by A9, SEQ_2:def 7;
then reconsider s = s as non-zero 0 -convergent Real_Sequence by A16, A8, SEQ_1:5, FDIFF_1:def 1;
( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0 ) by A2;
then consider n0 being Nat such that
A17: for m being Nat st n0 <= m holds
|.((((s ") (#) (R /* s)) . m) - 0).| < r by A3, SEQ_2:def 7;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
A18: |.(((s . n0) ") * (R /. (s . n0))).| = |.((s . n0) ").| * |.(R /. (s . n0)).| by COMPLEX1:65
.= (|.(s . n0).| ") * |.(R /. (s . n0)).| by COMPLEX1:66 ;
dom R = REAL by A1, PARTFUN1:def 2;
then A19: rng s c= dom R ;
|.((((s ") (#) (R /* s)) . n0) - 0).| = |.(((s ") . n0) * ((R /* s) . n0)).| by SEQ_1:8
.= |.(((s . n0) ") * ((R /* s) . n0)).| by VALUED_1:10
.= |.(((s . n0) ") * (R /. (s . n0))).| by A19, FUNCT_2:109 ;
hence contradiction by A7, A17, A18; :: thesis: verum

end;

assume A20: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) ) ; :: thesis: R is RestFunc-like
thus R is total by A1; :: according to FDIFF_1:def 2 :: thesis: for b₁ being Element of K16(K17(NAT,REAL)) holds
( (b₁ ") (#) (R /* b₁) is convergent & lim ((b₁ ") (#) (R /* b₁)) = 0 )
let s be non-zero 0 -convergent Real_Sequence; :: thesis: ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0 )
A21: ( s is convergent & lim s = 0 ) ;

A22: now :: thesis: for r being Real st r > 0 holds
ex n0 being Nat st
for m being Nat st n0 <= m holds
|.((((s ") (#) (R /* s)) . m) - 0).| < r

let r be Real; :: thesis: ( r > 0 implies ex n0 being Nat st
for m being Nat st n0 <= m holds
|.((((s ") (#) (R /* s)) . m) - 0).| < r )
assume r > 0 ; :: thesis: ex n0 being Nat st
for m being Nat st n0 <= m holds
|.((((s ") (#) (R /* s)) . m) - 0).| < r
then consider d being Real such that
A23: d > 0 and
A24: for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r by A20;
consider n0 being Nat such that
A25: for m being Nat st n0 <= m holds
|.((s . m) - 0).| < d by A21, A23, SEQ_2:def 7;
take n0 = n0; :: thesis: for m being Nat st n0 <= m holds
|.((((s ") (#) (R /* s)) . m) - 0).| < r
thus for m being Nat st n0 <= m holds
|.((((s ") (#) (R /* s)) . m) - 0).| < r :: thesis: verum

proof

dom R = REAL by A1, PARTFUN1:def 2;
then A26: rng s c= dom R ;
let m be Nat; :: thesis: ( n0 <= m implies |.((((s ") (#) (R /* s)) . m) - 0).| < r )
A27: m in NAT by ORDINAL1:def 12;
assume n0 <= m ; :: thesis: |.((((s ") (#) (R /* s)) . m) - 0).| < r
then A28: |.((s . m) - 0).| < d by A25;
(|.(s . m).| ") * |.(R /. (s . m)).| = |.((s . m) ").| * |.(R /. (s . m)).| by COMPLEX1:66
.= |.(((s . m) ") * (R /. (s . m))).| by COMPLEX1:65
.= |.(((s . m) ") * ((R /* s) . m)).| by A26, FUNCT_2:109, A27
.= |.(((s ") . m) * ((R /* s) . m)).| by VALUED_1:10
.= |.((((s ") (#) (R /* s)) . m) - 0).| by SEQ_1:8 ;
hence |.((((s ") (#) (R /* s)) . m) - 0).| < r by A24, A28, SEQ_1:5; :: 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 A22, SEQ_2:def 7; :: thesis: verum