let seq, seq9 be Real_Sequence; :: 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)
thus lim (seq - seq9) = (lim seq) + (lim (- seq9)) by A1, A2, Th20
.= (lim seq) + (- (lim seq9)) by A2, Th24
.= (lim seq) - (lim seq9) ; :: thesis: verum