theorem :: ASYMPT_0:28

for f being eventually-nonnegative Real_Sequence holds f in Big_Theta f