let seq be Real_Sequence; :: thesis: ( seq is convergent & 0 < lim seq implies ex n being Nat st
for m being Nat st n <= m holds
0 < seq . m )
assume that
A1: seq is convergent and
A2: 0 < lim seq and
A3: for n being Nat ex m being Nat st
( n <= m & not 0 < seq . m ) ; :: thesis: contradiction
consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < lim seq by A1, A2, SEQ_2:def 7;
consider m being Nat such that
A5: n <= m and
A6: not 0 < seq . m by A3;
A7: |.((seq . m) - (lim seq)).| < lim seq by A4, A5;

now :: thesis: contradiction

per cases ( seq . m < 0 or seq . m = 0 ) by A6;

suppose A8: seq . m < 0 ; :: thesis: contradiction

then - ((seq . m) - (lim seq)) < lim seq by A2, A7, ABSVALUE:def 1;
then (lim seq) - (seq . m) < lim seq ;
then lim seq < (lim seq) + (seq . m) by XREAL_1:19;
then (lim seq) - (lim seq) < seq . m by XREAL_1:19;
hence contradiction by A8; :: thesis: verum

end;

suppose seq . m = 0 ; :: thesis: contradiction

then |.(- (lim seq)).| < lim seq by A7;
then |.(lim seq).| < lim seq by COMPLEX1:52;
hence contradiction by A2, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum