for k being Nat
for c being XFinSequence of REAL st len c = k + 1 & 0 < c . k holds
seq_p c is polynomially-bounded