for seq1, seq2 being Complex_Sequence st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c holds
lim seq1 = lim seq2