let N be Nat; :: thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
seq - seq9 is convergent
let seq, seq9 be Real_Sequence of N; :: 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, Th40;
hence seq - seq9 is convergent by A1, Th36; :: thesis: verum