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 such that A4: for n being 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 such that A5: for n being Nat holds s < (seq ") . n ; :: according to SEQ_2:def 4 :: thesis: contradiction
set aa = |.r.|;
set ab = |.s.|;
set rab = 1 / (|.r.| + |.s.|);
A6: ( 0 <= |.r.| & 0 <= |.s.| ) by COMPLEX1:46;

A7: now :: thesis: for n being Element of NAT holds |.(seq . n).| > 1 / (|.r.| + |.s.|)

let n be Element of NAT ; :: thesis: |.(seq . n).| > 1 / (|.r.| + |.s.|)
set g = seq . n;
set t = (seq ") . n;
set At = |.((seq ") . n).|;
(seq ") . n = 1 / (seq . n) by VALUED_1:10;
then A8: |.((seq ") . n).| = 1 / |.(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 < |.((seq ") . n).| by COMPLEX1:47;
( s < (seq ") . n & (seq ") . n < r ) by A4, A5;
then |.((seq ") . n).| < |.r.| + |.s.| by Th37;
then |.((seq ") . n).| " > (|.r.| + |.s.|) " by A9, XREAL_1:88;
hence |.(seq . n).| > 1 / (|.r.| + |.s.|) by A8; :: thesis: verum

end;

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

now :: thesis: not 0 >= |.r.| + |.s.|

assume 0 >= |.r.| + |.s.| ; :: thesis: contradiction
then A12: |.r.| + |.s.| = 0 by A6;
then r = 0 by Th36;
hence contradiction by A11, A10, A12, Th36; :: thesis: verum

end;

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