let s, s9 be convergent Complex_Sequence; :: thesis: lim (s - s9) = (lim s) - (lim s9)
lim (s - s9) = (lim s) + (lim (- s9)) by Th12
.= (lim s) + (- (lim s9)) by Th16 ;
hence lim (s - s9) = (lim s) - (lim s9) ; :: thesis: verum