theorem :: ASYMPT_0:31

for f, t being positive Real_Sequence holds
( t in Big_Theta f iff ex c, d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) )