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