theorem
:: ASYMPT_0:31
for
f
,
t
being
positive
Real_Sequence
holds
(
t
in
Big_Theta
f
iff ex
c
,
d
being
Real
st
(
c
>
0
&
d
>
0
& ( for
n
being
Element
of
NAT
holds
(
d
*
(
f
.
n
)
<=
t
.
n
&
t
.
n
<=
c
*
(
f
.
n
)
) ) ) )