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
0 < - (lim f) by A2, XREAL_1:58;
then consider N1 being Element of NAT such that
A3: for m being Element of NAT st N1 <= m holds
abs ((f . m) - (lim f)) < - (lim f) by A1, SEQ_2:def 7;
consider N being Element of NAT such that
A4: for n being Element of NAT st n >= N holds
0 <= f . n by Def4;
set n1 = max (N,N1);

A5: now

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

end;

abs ((f . (max (N,N1))) - (lim f)) <= - (lim f) by A3, XXREAL_0:25;
then (f . (max (N,N1))) - (lim f) <= - (lim f) by ABSVALUE:5;
then ((f . (max (N,N1))) - (lim f)) + (lim f) <= (- (lim f)) + (lim f) by XREAL_1:6;
hence contradiction by A4, A5, XXREAL_0:25; :: thesis: verum