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