let seq be Complex_Sequence; ( seq is convergent & lim seq <> 0 implies ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is non-empty ) )
assume
( seq is convergent & lim seq <> 0 )
; ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is non-empty )
then consider k being Element of NAT such that
A1:
seq ^\ k is non-empty
by Th46;
take
seq ^\ k
; ( seq ^\ k is subsequence of seq & seq ^\ k is non-empty )
thus
( seq ^\ k is subsequence of seq & seq ^\ k is non-empty )
by A1; verum