for seq1, seq2 being Real_Sequence st seq1 is bounded & ( seq2 is divergent_to+infty or seq2 is divergent_to-infty ) holds
( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 )