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