let seq1, seq2 be Complex_Sequence; :: thesis: ( seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c implies lim seq1 = lim seq2 )
assume A1: ( seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c ) ; :: thesis: lim seq1 = lim seq2
then lim (seq1 - seq2) = (lim seq1) - (lim seq2) by COMSEQ_2:26;
hence lim seq1 = lim seq2 by A1; :: thesis: verum