for seq, seq1 being Real_Sequence st seq is convergent & seq1 is bounded & lim seq = 0 holds
lim (seq (#) seq1) = 0