let s, s9 be Complex_Sequence; :: thesis: ( s is convergent & s9 is convergent implies lim ((s - s9) *' ) = ((lim s) *' ) - ((lim s9) *' ) )
assume A1: ( s is convergent & s9 is convergent ) ; :: thesis: lim ((s - s9) *' ) = ((lim s) *' ) - ((lim s9) *' )
then s - s9 is convergent by Th25;
hence lim ((s - s9) *' ) = (lim (s - s9)) *' by Th12
.= ((lim s) - (lim s9)) *' by A1, Th26
.= ((lim s) *' ) - ((lim s9) *' ) by COMPLEX1:120 ;
:: thesis: verum