let r be real number ; :: thesis: for s being Real_Sequence st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (s . n) >= r & s is convergent holds
lim s <> 0
let s be Real_Sequence; :: thesis: ( r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (s . n) >= r & s is convergent implies lim s <> 0 )
assume A1: r > 0 ; :: thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not abs (s . n) >= r ) or not s is convergent or lim s <> 0 )
given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds
abs (s . n) >= r ; :: thesis: ( not s is convergent or lim s <> 0 )

now

per cases ( not s is convergent or s is convergent ) ;

suppose not s is convergent ; :: thesis: ( not s is convergent or lim s <> 0 )

hence ( not s is convergent or lim s <> 0 ) ; :: thesis: verum

end;

suppose A3: s is convergent ; :: thesis: ( not s is convergent or lim s <> 0 )

now

assume lim s = 0 ; :: thesis: contradiction
then consider k being Element of NAT such that
A4: for n being Element of NAT st n >= k holds
abs ((s . n) - 0 ) < r by A1, A3, SEQ_2:def 7;

now

let n be Element of NAT ; :: thesis: not n >= m + k
assume A5: n >= m + k ; :: thesis: contradiction
m + k >= m by NAT_1:11;
then A6: n >= m by A5, XXREAL_0:2;
m + k >= k by NAT_1:11;
then n >= k by A5, XXREAL_0:2;
then abs ((s . n) - 0 ) < r by A4;
hence contradiction by A2, A6; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

hence ( not s is convergent or lim s <> 0 ) ; :: thesis: verum

end;

end;

end;

hence ( not s is convergent or lim s <> 0 ) ; :: thesis: verum