let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent implies seq + seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; :: thesis: seq + seq9 is convergent
consider g1 being Real such that
A3: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g1).| < p by A1;
consider g2 being Real such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq9 . m) - g2).| < p by A2;
take g = g1 + g2; :: according to SEQ_2:def 6 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq + seq9) . m) - g).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq + seq9) . m) - g).| < p )
assume A5: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq + seq9) . m) - g).| < p
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < p / 2 by A3;
consider n2 being Nat such that
A7: for m being Nat st n2 <= m holds
|.((seq9 . m) - g2).| < p / 2 by A4, A5;
take k = n1 + n2; :: thesis: for m being Nat st k <= m holds
|.(((seq + seq9) . m) - g).| < p
let m be Nat; :: thesis: ( k <= m implies |.(((seq + seq9) . m) - g).| < p )
assume A8: k <= m ; :: thesis: |.(((seq + seq9) . m) - g).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A8, XXREAL_0:2;
then A9: |.((seq . m) - g1).| < p / 2 by A6;
n2 <= k by NAT_1:12;
then n2 <= m by A8, XXREAL_0:2;
then |.((seq9 . m) - g2).| < p / 2 by A7;
then A10: |.((seq . m) - g1).| + |.((seq9 . m) - g2).| < (p / 2) + (p / 2) by A9, XREAL_1:8;
A11: |.(((seq + seq9) . m) - g).| = |.(((seq . m) + (seq9 . m)) - (g1 + g2)).| by SEQ_1:7
.= |.(((seq . m) - g1) + ((seq9 . m) - g2)).| ;
|.(((seq . m) - g1) + ((seq9 . m) - g2)).| <= |.((seq . m) - g1).| + |.((seq9 . m) - g2).| by COMPLEX1:56;
hence |.(((seq + seq9) . m) - g).| < p by A10, A11, XXREAL_0:2; :: thesis: verum