theorem Th16: :: COMSEQ_2:22

for s being convergent Complex_Sequence holds lim (- s) = - (lim s)