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