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 Nat such that
A3: for m being Nat st N1 <= m holds
|.((f . m) - (lim f)).| < - (lim f) by A1, SEQ_2:def 7;
consider N being Nat such that
A4: for n being Nat st n >= N holds
0 <= f . n by Def2;
set n1 = max (N,N1);
A0: max (N,N1) is Nat by TARSKI:1;

A5: now :: thesis: not f . (max (N,N1)) = 0

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

end;

|.((f . (max (N,N1))) - (lim f)).| <= - (lim f) by A0, 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 A0, A4, A5, XXREAL_0:25; :: thesis: verum