theorem Th12: :: COMSEQ_2:14

for s, s9 being convergent Complex_Sequence holds lim (s + s9) = (lim s) + (lim s9)