theorem :: ASYMPT_2:20

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