let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent implies seq - seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; :: thesis: seq - seq9 is convergent
- seq9 is convergent by A2;
hence seq - seq9 is convergent by A1; :: thesis: verum