let seq be Real_Sequence; :: thesis: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing implies for n being Nat holds 0 < seq . n )
assume that
A1: seq is non-zero and
A2: ( seq is convergent & lim seq = 0 ) and
A3: seq is non-increasing and
A4: not for n being Nat holds 0 < seq . n ; :: thesis: contradiction
consider n being Nat such that
A5: not 0 < seq . n by A4;

now :: thesis: contradiction

per cases ( seq . n < 0 or seq . n = 0 ) by A5;

suppose A6: seq . n < 0 ; :: thesis: contradiction

then - 0 < - (seq . n) by XREAL_1:24;
then consider n1 being Nat such that
A7: for m being Nat st n1 <= m holds
|.((seq . m) - 0).| < - (seq . n) by A2, SEQ_2:def 7;
A8: |.((seq . (n1 + n)) - 0).| < - (seq . n) by A7, NAT_1:12;
A9: n <= n1 + n by NAT_1:12;
then seq . (n1 + n) < 0 by A3, A6, SEQM_3:8;
then - (seq . (n1 + n)) < - (seq . n) by A8, ABSVALUE:def 1;
then seq . n < seq . (n1 + n) by XREAL_1:24;
hence contradiction by A3, A9, SEQM_3:8; :: thesis: verum

end;

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

hence contradiction by A1, SEQ_1:5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum