let seq be Real_Sequence; :: thesis: ( seq is convergent & seq is non-empty & lim seq = 0 implies not seq " is bounded )
assume that
A1: seq is convergent and
A2: seq is non-empty 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:132;

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:15;
((seq " ) . n) " = ((seq . n) " ) " by VALUED_1:10;
then (seq " ) . n <> 0 by A2, SEQ_1:7, XCMPLX_1:203;
then A9: 0 < abs ((seq " ) . n) by COMPLEX1:133;
( s < (seq " ) . n & (seq " ) . n < r ) by A4, A5;
then abs ((seq " ) . n) < (abs r) + (abs s) by Th4;
then 1 / (abs ((seq " ) . n)) > 1 / ((abs r) + (abs s)) by A9, XREAL_1:90;
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 Th3;
hence contradiction by A11, A10, A12, Th3; :: 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