for f being eventually-nonnegative Real_Sequence st f is convergent holds
0 <= lim f