theorem
:: ASYMPT_0:28
for
f
being
eventually-nonnegative
Real_Sequence
holds
f
in
Big_Theta
f