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

now

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:21;
then (lim seq) - (lim seq) < seq . m by XREAL_1:21;
hence contradiction by A8; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum