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