theorem
Th20
:
:: ASYMPT_0:20
for
f
being
eventually-nonnegative
Real_Sequence
holds
f
in
Big_Omega
f