theorem TLNEG36: :: ASYMPT_2:42

for a being Real st 0 < a holds
for k being Nat
for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)