theorem TLNEG3: :: ASYMPT_2:44

for k being Nat
for d being XFinSequence of REAL st len d = k + 1 & 0 < d . k holds
seq_p d is eventually-nonnegative