let s, s' be Complex_Sequence; :: thesis: ( s is convergent & s' is convergent implies s + s' is convergent )
assume that
A1: s is convergent and
A2: s' is convergent ; :: thesis: s + s' is convergent
consider g being Element of COMPLEX such that
A3: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by A1, Def4;
consider g' being Element of COMPLEX such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s' . m) - g').| < p by A2, Def4;
take g1 = g + g'; :: according to COMSEQ_2:def 4 :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s + s') . m) - g1).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s + s') . m) - g1).| < p )
assume A5: p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s + s') . m) - g1).| < p
then consider n1 being Element of NAT such that
A6: for m being Element of NAT st n1 <= m holds
|.((s . m) - g).| < p / 2 by A3, XREAL_1:141;
consider n2 being Element of NAT such that
A7: for m being Element of NAT st n2 <= m holds
|.((s' . m) - g').| < p / 2 by A4, A5, XREAL_1:141;
reconsider n = max n1,n2 as Element of NAT by FINSEQ_2:1;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.(((s + s') . m) - g1).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s + s') . m) - g1).| < p )
assume A8: n <= m ; :: thesis: |.(((s + s') . m) - g1).| < p
n2 <= n by XXREAL_0:25;
then n + n2 <= n + m by A8, XREAL_1:9;
then n2 <= m by XREAL_1:8;
then A9: |.((s' . m) - g').| < p / 2 by A7;
A10: |.(((s + s') . m) - g1).| = |.(((s . m) + (s' . m)) - (g + g')).| by VALUED_1:1
.= |.(((s . m) - g) + ((s' . m) - g')).| ;
n1 <= n by XXREAL_0:25;
then n + n1 <= n + m by A8, XREAL_1:9;
then n1 <= m by XREAL_1:8;
then |.((s . m) - g).| < p / 2 by A6;
then |.((s . m) - g).| + |.((s' . m) - g').| < (p / 2) + (p / 2) by A9, XREAL_1:10;
then (|.((s . m) - g).| + |.((s' . m) - g').|) + |.(((s + s') . m) - g1).| < p + (|.((s . m) - g).| + |.((s' . m) - g').|) by A10, COMPLEX1:142, XREAL_1:10;
hence |.(((s + s') . m) - g1).| < p by XREAL_1:8; :: thesis: verum