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) ) )