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