theorem TLNEG35: :: ASYMPT_2:43

for k being Nat
for d being XFinSequence of REAL
for a being Real
for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds
ex N being Nat st
for x being Nat st N <= x holds
|.((seq_p d) . x).| <= y . x