theorem :: ASYMPT_0:7

for f being positive Real_Sequence

for t being eventually-nonnegative Real_Sequence holds

( t in Big_Oh f iff ex c being Real st

( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) )

for t being eventually-nonnegative Real_Sequence holds

( t in Big_Oh f iff ex c being Real st

( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) )