for k being Nat
for c being XFinSequence of REAL st len c = k + 1 & 0 < c . k holds
seq_p c in Big_Oh (seq_n^ k) by LMXFIN20A, TLNEG3;