let f be eventually-nonnegative Real_Sequence; :: thesis: ( f is convergent implies 0 <= lim f )
assume that
A1: f is convergent and
A2: not 0 <= lim f ; :: thesis: contradiction
consider N being Element of NAT such that
A3: for n being Element of NAT st n >= N holds
0 <= f . n by Def4;
A4: 0 < - (lim f) by A2, XREAL_1:60;
then consider N1 being Element of NAT such that
A5: for m being Element of NAT st N1 <= m holds
abs ((f . m) - (lim f)) < - (lim f) by A1, SEQ_2:def 7;
set n1 = max N,N1;
( abs ((f . (max N,N1)) - (lim f)) <= - (lim f) & abs ((f . (max N,N1)) - (lim f)) <> - (lim f) ) by A5, XXREAL_0:25;
then (f . (max N,N1)) - (lim f) <= - (lim f) by ABSVALUE:12;
then A6: ((f . (max N,N1)) - (lim f)) + (lim f) <= (- (lim f)) + (lim f) by XREAL_1:8;

now

assume f . (max N,N1) = 0 ; :: thesis: contradiction
then abs ((f . (max N,N1)) - (lim f)) = - (lim f) by A4, ABSVALUE:def 1;
hence contradiction by A5, XXREAL_0:25; :: thesis: verum

end;

hence contradiction by A3, A6, XXREAL_0:25; :: thesis: verum