theorem
Th27
:
:: ASYMPT_0:27
for
f
being
eventually-nonnegative
Real_Sequence
holds
Big_Theta
f
=
{
t
where
t
is
Element
of
Funcs
(
NAT
,
REAL
) : ex
c
,
d
being
Real
ex
N
being
Element
of
NAT
st
(
c
>
0
&
d
>
0
& ( for
n
being
Element
of
NAT
st
n
>=
N
holds
(
d
*
(
f
.
n
)
<=
t
.
n
&
t
.
n
<=
c
*
(
f
.
n
)
) ) )
}