let N be 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, Th40;
hence lim (seq - seq9) = (lim seq) + (lim (- seq9)) by A1, Th37
.= (lim seq) + (- (lim seq9)) by A2, Th41
.= (lim seq) - (lim seq9) ;
:: thesis: verum