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