let R be Function of REAL,REAL; ( 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).| / |.z.| < r ) ) )
A1:
now ( 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 & |.z.| < d & not |.(R . z).| / |.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).| / |.z.| < r ) ) )assume A2:
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 & |.z.| < d & not |.(R . z).| / |.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).| / |.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 &
|.z.| < d & not
|.(R . z).| / |.z.| < r ) ) ) )
;
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).| / |.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 &
|.z.| < d & not
|.(R . z).| / |.z.| < r )
;
defpred S1[
Nat,
Element of
REAL ]
means ( $2
<> 0 &
|.$2.| < 1
/ ($1 + 1) & not
|.(R . $2).| / |.$2.| < r );
consider s being
Real_Sequence such that A7:
for
n being
Element of
NAT holds
S1[
n,
s . n]
from FUNCT_2:sch 3(A5);
A8:
for
n being
Nat holds
S1[
n,
s . n]
then
s is
convergent
by 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 A9, A8, SEQ_1:5, SEQ_2:def 6, FDIFF_1:def 1;
(
(s ") (#) (R /* s) is
convergent &
lim ((s ") (#) (R /* s)) = 0 )
by A2, FDIFF_1:def 2;
then consider n being
Nat such that A15:
for
m being
Nat st
n <= m holds
|.((((s ") (#) (R /* s)) . m) - 0).| < r
by A3, SEQ_2:def 7;
A16:
n in NAT
by ORDINAL1:def 12;
A18:
|.(((s . n) ") * (R . (s . n))).| =
|.((s . n) ").| * |.(R . (s . n)).|
by COMPLEX1:65
.=
|.(R . (s . n)).| / |.(s . n).|
by COMPLEX1:66
;
|.((((s ") (#) (R /* s)) . n) - 0).| =
|.(((s ") . n) * ((R /* s) . n)).|
by SEQ_1:8
.=
|.(((s . n) ") * ((R /* s) . n)).|
by VALUED_1:10
.=
|.(((s . n) ") * (R . (s . n))).|
by FUNCT_2:115, A16
;
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).| / |.z.| < r ) )
by A8, A15, A18;
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).| / |.z.| < r ) ) )
by A1; verum