let s, s' be Complex_Sequence; :: thesis: ( s is convergent & s' is convergent implies s - s' is convergent )
assume A1: ( s is convergent & s' is convergent ) ; :: thesis: s - s' is convergent
then - s' is convergent ;
hence s - s' is convergent by A1, Th13; :: thesis: verum