let s, s9 be convergent Complex_Sequence; :: thesis: lim (s + s9) = (lim s) + (lim s9)
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((s + s9) . m) - ((lim s) + (lim s9))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((s + s9) . m) - ((lim s) + (lim s9))).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((s + s9) . m) - ((lim s) + (lim s9))).| < p
then A1: 0 < p / 2 ;
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((s . m) - (lim s)).| < p / 2 by Def6;
consider n2 being Nat such that
A3: for m being Nat st n2 <= m holds
|.((s9 . m) - (lim s9)).| < p / 2 by A1, Def6;
reconsider n = max (n1,n2) as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((s + s9) . m) - ((lim s) + (lim s9))).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p )
assume A4: n <= m ; :: thesis: |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p
n2 <= n by XXREAL_0:25;
then n + n2 <= n + m by A4, XREAL_1:7;
then n2 <= m by XREAL_1:6;
then A5: |.((s9 . m) - (lim s9)).| < p / 2 by A3;
m in NAT by ORDINAL1:def 12;
then A6: |.(((s + s9) . m) - ((lim s) + (lim s9))).| = |.(((s . m) + (s9 . m)) - ((lim s) + (lim s9))).| by VALUED_1:1
.= |.(((s . m) - (lim s)) + ((s9 . m) - (lim s9))).| ;
n1 <= n by XXREAL_0:25;
then n + n1 <= n + m by A4, XREAL_1:7;
then n1 <= m by XREAL_1:6;
then |.((s . m) - (lim s)).| < p / 2 by A2;
then |.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).| < (p / 2) + (p / 2) by A5, XREAL_1:8;
then (|.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).|) + |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p + (|.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).|) by A6, COMPLEX1:56, XREAL_1:8;
hence |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p by XREAL_1:6; :: thesis: verum

end;

hence lim (s + s9) = (lim s) + (lim s9) by Def6; :: thesis: verum