let N be Element of NAT ; :: thesis: for seq, seq' being Real_Sequence of N st seq is convergent & seq' is convergent holds
seq + seq' is convergent
let seq, seq' be Real_Sequence of N; :: thesis: ( seq is convergent & seq' is convergent implies seq + seq' is convergent )
assume that
A1: seq is convergent and
A2: seq' is convergent ; :: thesis: seq + seq' is convergent
consider g1 being Point of (TOP-REAL N) such that
A3: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < r by A1, Def9;
consider g2 being Point of (TOP-REAL N) such that
A4: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq' . m) - g2).| < r by A2, Def9;
take g = g1 + g2; :: according to TOPRNS_1:def 9 :: thesis: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((seq + seq') . m) - g).| < r
let r be Real; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((seq + seq') . m) - g).| < r )
assume 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((seq + seq') . m) - g).| < r
then A5: 0 < r / 2 by XREAL_1:217;
then consider n1 being Element of NAT such that
A6: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g1).| < r / 2 by A3;
consider n2 being Element of NAT such that
A7: for m being Element of NAT st n2 <= m holds
|.((seq' . m) - g2).| < r / 2 by A4, A5;
take k = n1 + n2; :: thesis: for m being Element of NAT st k <= m holds
|.(((seq + seq') . m) - g).| < r
let m be Element of NAT ; :: thesis: ( k <= m implies |.(((seq + seq') . m) - g).| < r )
assume A8: k <= m ; :: thesis: |.(((seq + seq') . m) - g).| < r
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A8, XXREAL_0:2;
then A9: |.((seq . m) - g1).| < r / 2 by A6;
n2 <= k by NAT_1:12;
then n2 <= m by A8, XXREAL_0:2;
then |.((seq' . m) - g2).| < r / 2 by A7;
then A10: |.((seq . m) - g1).| + |.((seq' . m) - g2).| < (r / 2) + (r / 2) by A9, XREAL_1:10;
A11: |.(((seq + seq') . m) - g).| = |.(((seq . m) + (seq' . m)) - (g1 + g2)).| by Def2
.= |.((seq . m) + ((seq' . m) - (g1 + g2))).| by EUCLID:49
.= |.((seq . m) + ((- (g1 + g2)) + (seq' . m))).| by EUCLID:45
.= |.(((seq . m) + (- (g1 + g2))) + (seq' . m)).| by EUCLID:30
.= |.(((seq . m) - (g1 + g2)) + (seq' . m)).| by EUCLID:45
.= |.((((seq . m) - g1) - g2) + (seq' . m)).| by EUCLID:50
.= |.((((seq . m) - g1) + (- g2)) + (seq' . m)).| by EUCLID:45
.= |.(((seq . m) - g1) + ((seq' . m) + (- g2))).| by EUCLID:30
.= |.(((seq . m) - g1) + ((seq' . m) - g2)).| by EUCLID:45 ;
|.(((seq . m) - g1) + ((seq' . m) - g2)).| <= |.((seq . m) - g1).| + |.((seq' . m) - g2).| by Th30;
hence |.(((seq + seq') . m) - g).| < r by A10, A11, XXREAL_0:2; :: thesis: verum