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