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: ( 0 <= abs r & 0 <= abs s ) by COMPLEX1:46;

A7: 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);
(seq ") . n = 1 / (seq . n) by VALUED_1:10;
then A8: abs ((seq ") . n) = 1 / (abs (seq . n)) by ABSVALUE:7;
((seq ") . n) " = ((seq . n) ") " by VALUED_1:10;
then (seq ") . n <> 0 by A2, SEQ_1:5, XCMPLX_1:202;
then A9: 0 < abs ((seq ") . n) by COMPLEX1:47;
( s < (seq ") . n & (seq ") . n < r ) by A4, A5;
then abs ((seq ") . n) < (abs r) + (abs s) by Th73;
then (abs ((seq ") . n)) " > ((abs r) + (abs s)) " by A9, XREAL_1:88;
hence abs (seq . n) > 1 / ((abs r) + (abs s)) by A8; :: thesis: verum

end;

A10: (seq ") . 1 < r by A4;
A11: s < (seq ") . 1 by A5;

now

assume 0 >= (abs r) + (abs s) ; :: thesis: contradiction
then A12: (abs r) + (abs s) = 0 by A6;
then r = 0 by Th72;
hence contradiction by A11, A10, A12, Th72; :: thesis: verum

end;

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