let s, s' be Complex_Sequence; :: thesis: ( s is convergent & s' is convergent implies lim (s + s') = (lim s) + (lim s') )
assume A1: ( s is convergent & s' is convergent ) ; :: thesis: lim (s + s') = (lim s) + (lim s')
then A2: s + s' is convergent by Th13;
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) - ((lim s) + (lim s'))).| < p

proof

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) - ((lim s) + (lim s'))).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s + s') . m) - ((lim s) + (lim s'))).| < p
then A3: 0 < p / 2 by XREAL_1:141;
then consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
|.((s . m) - (lim s)).| < p / 2 by A1, Def5;
consider n2 being Element of NAT such that
A5: for m being Element of NAT st n2 <= m holds
|.((s' . m) - (lim s')).| < p / 2 by A1, A3, Def5;
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) - ((lim s) + (lim s'))).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s + s') . m) - ((lim s) + (lim s'))).| < p )
assume A6: n <= m ; :: thesis: |.(((s + s') . m) - ((lim s) + (lim s'))).| < p
n1 <= n by XXREAL_0:25;
then n + n1 <= n + m by A6, XREAL_1:9;
then n1 <= m by XREAL_1:8;
then A7: |.((s . m) - (lim s)).| < p / 2 by A4;
n2 <= n by XXREAL_0:25;
then n + n2 <= n + m by A6, XREAL_1:9;
then n2 <= m by XREAL_1:8;
then |.((s' . m) - (lim s')).| < p / 2 by A5;
then A8: |.((s . m) - (lim s)).| + |.((s' . m) - (lim s')).| < (p / 2) + (p / 2) by A7, XREAL_1:10;
|.(((s + s') . m) - ((lim s) + (lim s'))).| = |.(((s . m) + (s' . m)) - ((lim s) + (lim s'))).| by VALUED_1:1
.= |.(((s . m) - (lim s)) + ((s' . m) - (lim s'))).| ;
then (|.((s . m) - (lim s)).| + |.((s' . m) - (lim s')).|) + |.(((s + s') . m) - ((lim s) + (lim s'))).| < p + (|.((s . m) - (lim s)).| + |.((s' . m) - (lim s')).|) by A8, COMPLEX1:142, XREAL_1:10;
hence |.(((s + s') . m) - ((lim s) + (lim s'))).| < p by XREAL_1:8; :: thesis: verum

end;

hence lim (s + s') = (lim s) + (lim s') by A2, Def5; :: thesis: verum