theorem LMXFIN10: :: ASYMPT_2:33

for k being Nat
for c being nonnegative-yielding XFinSequence of REAL st len c = k + 1 holds
seq_p c in Big_Oh (seq_n^ k)