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