let s, s9 be Complex_Sequence; :: thesis: ( s is convergent & s9 is convergent implies lim (s - s9) = (lim s) - (lim s9) )
assume that
A1: s is convergent and
A2: s9 is convergent ; :: thesis: lim (s - s9) = (lim s) - (lim s9)
lim (s - s9) = (lim s) + (lim (- s9)) by A1, A2, Th14
.= (lim s) + (- (lim s9)) by A2, Th22 ;
hence lim (s - s9) = (lim s) - (lim s9) ; :: thesis: verum