:: deftheorem defines polynomially-bounded ASYMPT_2:def 1 :
for p being Real_Sequence holds
( p is polynomially-bounded iff ex k being Nat st p in Big_Oh (seq_n^ k) );