for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 holds
seq1 (#) seq2 is divergent_to+infty