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