let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq <> 0 implies for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) " )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; :: thesis: for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) "
let seq1 be Real_Sequence; :: thesis: ( seq1 is subsequence of seq & seq1 is non-zero implies lim (seq1 ") = (lim seq) " )
assume that
A3: seq1 is subsequence of seq and
A4: seq1 is non-zero ; :: thesis: lim (seq1 ") = (lim seq) "
lim seq1 = lim seq by A1, A3, Th17;
hence lim (seq1 ") = (lim seq) " by A1, A2, A3, A4, Th16, SEQ_2:22; :: thesis: verum