let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq <> 0 implies ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero ) )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; :: thesis: ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )
consider k being Element of NAT such that
A3: seq ^\ k is non-zero by A1, A2, Th37;
take seq ^\ k ; :: thesis: ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero )
thus ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero ) by A3; :: thesis: verum