let seq be Complex_Sequence; :: thesis: ( seq is bounded implies ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) )
assume seq is bounded ; :: thesis: ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )
then consider r being Real such that
A1: 0 < r and
A2: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:8;

now

let n be Element of NAT ; :: thesis: abs ((Re seq) . n) < r
( abs ((Re seq) . n) = abs (Re (seq . n)) & abs (Re (seq . n)) <= |.(seq . n).| ) by Def5, Th13;
hence abs ((Re seq) . n) < r by A2, XXREAL_0:2; :: thesis: verum

end;

then Re seq is bounded by A1, SEQ_2:3;
then consider rseq1 being Real_Sequence such that
A3: rseq1 is subsequence of Re seq and
A4: rseq1 is convergent by SEQ_4:40;
consider Nseq being increasing sequence of NAT such that
A5: rseq1 = (Re seq) * Nseq by A3, VALUED_0:def 17;

A6: now

let n be Element of NAT ; :: thesis: |.((seq * Nseq) . n).| < r
|.((seq * Nseq) . n).| = |.(seq . (Nseq . n)).| by FUNCT_2:15;
hence |.((seq * Nseq) . n).| < r by A2; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: abs ((Im (seq * Nseq)) . n) < r
( abs ((Im (seq * Nseq)) . n) = abs (Im ((seq * Nseq) . n)) & abs (Im ((seq * Nseq) . n)) <= |.((seq * Nseq) . n).| ) by Def6, Th13;
hence abs ((Im (seq * Nseq)) . n) < r by A6, XXREAL_0:2; :: thesis: verum

end;

then Im (seq * Nseq) is bounded by A1, SEQ_2:3;
then consider rseq2 being Real_Sequence such that
A7: rseq2 is subsequence of Im (seq * Nseq) and
A8: rseq2 is convergent by SEQ_4:40;
consider Nseq1 being increasing sequence of NAT such that
A9: rseq2 = (Im (seq * Nseq)) * Nseq1 by A7, VALUED_0:def 17;
Re ((seq * Nseq) * Nseq1) = (Re (seq * Nseq)) * Nseq1 by Th22
.= rseq1 * Nseq1 by A5, Th22 ;
then A10: Re ((seq * Nseq) * Nseq1) is convergent by A4, SEQ_4:16;
( seq * Nseq is subsequence of seq & (seq * Nseq) * Nseq1 is subsequence of seq * Nseq ) by VALUED_0:def 17;
then A11: (seq * Nseq) * Nseq1 is subsequence of seq by VALUED_0:20;
Im ((seq * Nseq) * Nseq1) is convergent by A8, A9, Th22;
hence ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) by A11, A10, Th42; :: thesis: verum