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