for r being Element of NAT
for s being Real_Sequence st s = NAT --> r holds
s is polynomially-abs-bounded