theorem :: ASYMPT_0:8

for f being eventually-positive Real_Sequence

for t being eventually-nonnegative Real_Sequence

for N being Element of NAT st t in Big_Oh f & ( for n being Element of NAT st n >= N holds

f . n > 0 ) holds

ex c being Real st

( c > 0 & ( for n being Element of NAT st n >= N holds

t . n <= c * (f . n) ) )

for t being eventually-nonnegative Real_Sequence

for N being Element of NAT st t in Big_Oh f & ( for n being Element of NAT st n >= N holds

f . n > 0 ) holds

ex c being Real st

( c > 0 & ( for n being Element of NAT st n >= N holds

t . n <= c * (f . n) ) )