let seq be Real_Sequence; :: thesis: ( seq is convergent & seq is non-zero & lim seq = 0 implies not seq " is bounded )
assume that
A1: seq is convergent and
A2: seq is non-zero and
A3: lim seq = 0 ; :: thesis: not seq " is bounded
given r being real number such that A4: for n being Element of NAT holds (seq " ) . n < r ; :: according to SEQ_2:def 3,SEQ_2:def 8 :: thesis: not seq " is bounded_below
given s being real number such that A5: for n being Element of NAT holds s < (seq " ) . n ; :: according to SEQ_2:def 4 :: thesis: contradiction
set aa = abs r;
set ab = abs s;
set rab = 1 / ((abs r) + (abs s));
A6: ( s < (seq " ) . 1 & (seq " ) . 1 < r ) by A4, A5;
( 0 <= abs r & 0 <= abs s ) by COMPLEX1:132;
then A7: 0 + 0 <= (abs r) + (abs s) ;

now

assume 0 >= (abs r) + (abs s) ; :: thesis: contradiction
then (abs r) + (abs s) = 0 by A7;
then ( r = 0 & s = 0 ) by Th3;
hence contradiction by A6; :: thesis: verum

end;

then 0 < ((abs r) + (abs s)) " ;
then A8: 0 < 1 / ((abs r) + (abs s)) ;

A9: now

let n be Element of NAT ; :: thesis: abs (seq . n) > 1 / ((abs r) + (abs s))
set g = seq . n;
set t = (seq " ) . n;
set At = abs ((seq " ) . n);
( s < (seq " ) . n & (seq " ) . n < r ) by A4, A5;
then A10: abs ((seq " ) . n) < (abs r) + (abs s) by Th4;
A11: ((seq " ) . n) " = ((seq . n) " ) " by VALUED_1:10;
then (seq " ) . n <> 0 by A2, SEQ_1:7, XCMPLX_1:203;
then A12: 0 < abs ((seq " ) . n) by COMPLEX1:133;
(seq " ) . n = 1 / (seq . n) by A11;
then A13: abs ((seq " ) . n) = 1 / (abs (seq . n)) by ABSVALUE:15;
1 / (abs ((seq " ) . n)) > 1 / ((abs r) + (abs s)) by A10, A12, XREAL_1:90;
hence abs (seq . n) > 1 / ((abs r) + (abs s)) by A13; :: thesis: verum

end;

consider n being Element of NAT such that
A14: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0 ) < 1 / ((abs r) + (abs s)) by A1, A3, A8, SEQ_2:def 7;
abs ((seq . n) - 0 ) < 1 / ((abs r) + (abs s)) by A14;
hence contradiction by A9; :: thesis: verum