theorem LM1: :: ASYMPT_3:10

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