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