let N be Element of NAT ; :: thesis: for seq, seq' being Real_Sequence of N st seq is convergent & seq' is convergent holds
seq - seq' is convergent
let seq, seq' be Real_Sequence of N; :: thesis: ( seq is convergent & seq' is convergent implies seq - seq' is convergent )
assume that
A1: seq is convergent and
A2: seq' is convergent ; :: thesis: seq - seq' is convergent
- seq' is convergent by A2, Th45;
hence seq - seq' is convergent by A1, Th41; :: thesis: verum