for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent