theorem :: ASYMPT_2:39

for f being eventually-nonnegative Real_Sequence
for k being Nat st f in Big_Oh (seq_n^ k) holds
ex N being Nat st
for n being Nat st N <= n holds
f . n <= (seq_n^ (k + 1)) . n