theorem :: CFCONT_1:25

for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds
ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )