let n be non zero Element of NAT ; :: thesis: for R being PartFunc of REAL,() 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 Real st z <> 0 & |.z.| < d holds
() * ||.(R /. z).|| < r ) ) )

let R be PartFunc of 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
() * ||.(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
() * ||.(R /. z).|| < r ) ) )

A2: now :: thesis: ( R is RestFunc-like & ex r being Real st
( r > 0 & ( for d being Real st d > 0 holds
ex z being Real st
( z <> 0 & |.z.| < d & not () * ||.(R /. 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 & |.z.| < d holds
() * ||.(R /. z).|| < r ) ) )
assume A3: R is RestFunc-like ; :: thesis: ( ex r being Real st
( r > 0 & ( for d being Real st d > 0 holds
ex z being Real st
( z <> 0 & |.z.| < d & not () * ||.(R /. 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 & |.z.| < d holds
() * ||.(R /. z).|| < r ) ) )

given 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 & |.z.| < d & not () * ||.(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
() * ||.(R /. z).|| < r ) )

defpred S1[ Nat, Real] means ( \$2 <> 0 & |.\$2.| < 1 / (\$1 + 1) & not (|.\$2.| ") * ||.(R /. \$2).|| < r );
A6: for n being Element of NAT ex z being Element of REAL st S1[n,z]
proof
let n be Element of NAT ; :: thesis: ex z being Element of REAL st S1[n,z]
consider z being Real such that
A7: ( z <> 0 & |.z.| < 1 / (n + 1) & not () * ||.(R /. z).|| < r ) by A5;
reconsider z = z as Element of REAL by XREAL_0:def 1;
take z ; :: thesis: S1[n,z]
( z <> 0 & |.z.| < 1 / (n + 1) & not () * ||.(R /. z).|| < r ) by A7;
then S1[n,z] ;
hence
S1[n,z] ; :: thesis: verum
end;
consider s being Real_Sequence such that
A8: for n being Element of NAT holds S1[n,s . n] from A9: 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 A8; :: thesis: verum
end;
A10: 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 A11: 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
A12: p " < n by SEQ_4:3;
reconsider q0 = 0 , q1 = 1 as Real ;
(p ") + q0 < n + q1 by ;
then A13: 1 / (n + 1) < 1 / (p ") by ;
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 )
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 ;
then |.((s . m) - 0).| < 1 / (n + 1) by ;
hence |.((s . m) - 0).| < p by ; :: thesis: verum
end;
A15: s is convergent by ;
then A16: lim s = 0 by ;
s is non-zero by ;
then reconsider s = s as non-zero 0 -convergent Real_Sequence by ;
( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. () ) by ;
then consider n0 being Nat such that
A17: for m being Nat st n0 <= m holds
||.((((s ") (#) (R /* s)) . m) - (0. ())).|| < r by ;
A18: ||.((((s ") (#) (R /* s)) . n0) - (0. ())).|| < r by A17;
A19: ||.(((s . n0) ") * (R /. (s . n0))).|| = |.((s . n0) ").| * ||.(R /. (s . n0)).|| by NORMSP_1:def 1
.= (|.(s . n0).| ") * ||.(R /. (s . n0)).|| by COMPLEX1:66 ;
dom R = REAL by ;
then A20: rng s c= dom R ;
A21: n0 in NAT by ORDINAL1:def 12;
||.((((s ") (#) (R /* s)) . n0) - (0. ())).|| = ||.(((s ") (#) (R /* s)) . n0).|| by RLVECT_1:13
.= ||.(((s ") . n0) * ((R /* s) . n0)).|| by NDIFF_1:def 2
.= ||.(((s . n0) ") * ((R /* s) . n0)).|| by VALUED_1:10
.= ||.(((s . n0) ") * (R /. (s . n0))).|| by ;
hence 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
() * ||.(R /. z).|| < r ) ) by A9, A18, A19; :: 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 & |.z.| < 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 Real st z <> 0 & |.z.| < d holds
() * ||.(R /. z).|| < r ) ) ; :: thesis:
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. () )
A23: ( s is convergent & lim s = 0 ) ;
A24: 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
A25: d > 0 and
A26: for z being Real st z <> 0 & |.z.| < d holds
() * ||.(R /. z).|| < r by A22;
consider n0 being Nat such that
A27: for m being Nat st n0 <= m holds
|.((s . m) - 0).| < d by ;
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 ;
then A28: rng s c= dom R ;
let m be Nat; :: thesis: ( n0 <= m implies ||.((((s ") (#) (R /* s)) . m) - (0. ())).|| < r )
assume n0 <= m ; :: thesis: ||.((((s ") (#) (R /* s)) . m) - (0. ())).|| < r
then A29: |.((s . m) - 0).| < d by A27;
A30: s . m <> 0 by SEQ_1:5;
A31: m in NAT by ORDINAL1:def 12;
(|.(s . m).| ") * ||.(R /. (s . m)).|| = |.((s . m) ").| * ||.(R /. (s . m)).|| by COMPLEX1:66
.= ||.(((s . m) ") * (R /. (s . m))).|| by NORMSP_1:def 1
.= ||.(((s . m) ") * ((R /* s) . m)).|| by
.= ||.(((s ") . m) * ((R /* s) . m)).|| by VALUED_1:10
.= ||.(((s ") (#) (R /* s)) . m).|| by NDIFF_1:def 2
.= ||.((((s ") (#) (R /* s)) . m) - (0. ())).|| by RLVECT_1:13 ;
hence ||.((((s ") (#) (R /* s)) . m) - (0. ())).|| < r by ; :: thesis: verum
end;
end;
hence (s ") (#) (R /* s) is convergent by NORMSP_1:def 6; :: thesis: lim ((s ") (#) (R /* s)) = 0. ()
hence lim ((s ") (#) (R /* s)) = 0. () by ; :: thesis: verum
end;
hence R is RestFunc-like by ; :: 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 & |.z.| < d holds
() * ||.(R /. z).|| < r ) ) ) by A2; :: thesis: verum