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)
A3: seq + seq9 is convergent by A1, A2, Th19;

now

let p be real number ; :: thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p )
assume 0 < p ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p
then A4: 0 < p / 2 by XREAL_1:217;
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p / 2 by A1, Def7;
consider n2 being Element of NAT such that
A6: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - (lim seq9)) < p / 2 by A2, A4, Def7;
take k = n1 + n2; :: thesis: for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p
let m be Element of NAT ; :: thesis: ( k <= m implies abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p )
assume A7: k <= m ; :: thesis: abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A7, XXREAL_0:2;
then A8: abs ((seq . m) - (lim seq)) < p / 2 by A5;
n2 <= k by NAT_1:12;
then n2 <= m by A7, XXREAL_0:2;
then abs ((seq9 . m) - (lim seq9)) < p / 2 by A6;
then A9: (abs ((seq . m) - (lim seq))) + (abs ((seq9 . m) - (lim seq9))) < (p / 2) + (p / 2) by A8, XREAL_1:10;
A10: abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) = abs (((seq . m) + (seq9 . m)) - ((lim seq) + (lim seq9))) by SEQ_1:11
.= abs (((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))) ;
abs (((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))) <= (abs ((seq . m) - (lim seq))) + (abs ((seq9 . m) - (lim seq9))) by COMPLEX1:142;
hence abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p by A9, A10, XXREAL_0:2; :: thesis: verum

end;

hence lim (seq + seq9) = (lim seq) + (lim seq9) by A3, Def7; :: thesis: verum