let N be Element of NAT ; :: thesis: for seq, seq' being Real_Sequence of N st seq is convergent & seq' is convergent holds
lim (seq - seq') = (lim seq) - (lim seq')
let seq, seq' be Real_Sequence of N; :: thesis: ( seq is convergent & seq' is convergent implies lim (seq - seq') = (lim seq) - (lim seq') )
assume that
A1: seq is convergent and
A2: seq' is convergent ; :: thesis: lim (seq - seq') = (lim seq) - (lim seq')
- seq' is convergent by A2, Th45;
hence lim (seq - seq') = (lim seq) + (lim (- seq')) by A1, Th42
.= (lim seq) + (- (lim seq')) by A2, Th46
.= (lim seq) - (lim seq') by EUCLID:45 ;
:: thesis: verum