theorem :: ASYMPT_2:21

for f being Real_Sequence st ( for k being Nat holds not f in Big_Oh (seq_n^ k) ) holds
not f is polynomially-bounded ;