let s be Complex_Sequence; :: thesis: ( s = s1 + s2 implies s is convergent )

assume A1: s = s1 + s2 ; :: thesis: s is convergent

consider g being Complex such that

A2: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s1 . m) - g).| < p by Def5;

consider g9 being Complex such that

A3: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s2 . m) - g9).| < p by Def5;

take g1 = g + g9; :: according to COMSEQ_2:def 5 :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g1).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g1).| < p )

assume A4: p > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g1).| < p

then consider n1 being Nat such that

A5: for m being Nat st n1 <= m holds

|.((s1 . m) - g).| < p / 2 by A2;

consider n2 being Nat such that

A6: for m being Nat st n2 <= m holds

|.((s2 . m) - g9).| < p / 2 by A3, A4;

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 . m) - g1).| < p

let m be Nat; :: thesis: ( n <= m implies |.((s . m) - g1).| < p )

assume A7: n <= m ; :: thesis: |.((s . m) - g1).| < p

n2 <= n by XXREAL_0:25;

then n + n2 <= n + m by A7, XREAL_1:7;

then n2 <= m by XREAL_1:6;

then A8: |.((s2 . m) - g9).| < p / 2 by A6;

m in NAT by ORDINAL1:def 12;

then A9: |.(((s1 + s2) . m) - g1).| = |.(((s1 . m) + (s2 . m)) - (g + g9)).| by VALUED_1:1

.= |.(((s1 . m) - g) + ((s2 . m) - g9)).| ;

n1 <= n by XXREAL_0:25;

then n + n1 <= n + m by A7, XREAL_1:7;

then n1 <= m by XREAL_1:6;

then |.((s1 . m) - g).| < p / 2 by A5;

then |.((s1 . m) - g).| + |.((s2 . m) - g9).| < (p / 2) + (p / 2) by A8, XREAL_1:8;

then (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) + |.(((s1 + s2) . m) - g1).| < p + (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) by A9, COMPLEX1:56, XREAL_1:8;

hence |.((s . m) - g1).| < p by A1, XREAL_1:6; :: thesis: verum

assume A1: s = s1 + s2 ; :: thesis: s is convergent

consider g being Complex such that

A2: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s1 . m) - g).| < p by Def5;

consider g9 being Complex such that

A3: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s2 . m) - g9).| < p by Def5;

take g1 = g + g9; :: according to COMSEQ_2:def 5 :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g1).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g1).| < p )

assume A4: p > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g1).| < p

then consider n1 being Nat such that

A5: for m being Nat st n1 <= m holds

|.((s1 . m) - g).| < p / 2 by A2;

consider n2 being Nat such that

A6: for m being Nat st n2 <= m holds

|.((s2 . m) - g9).| < p / 2 by A3, A4;

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 . m) - g1).| < p

let m be Nat; :: thesis: ( n <= m implies |.((s . m) - g1).| < p )

assume A7: n <= m ; :: thesis: |.((s . m) - g1).| < p

n2 <= n by XXREAL_0:25;

then n + n2 <= n + m by A7, XREAL_1:7;

then n2 <= m by XREAL_1:6;

then A8: |.((s2 . m) - g9).| < p / 2 by A6;

m in NAT by ORDINAL1:def 12;

then A9: |.(((s1 + s2) . m) - g1).| = |.(((s1 . m) + (s2 . m)) - (g + g9)).| by VALUED_1:1

.= |.(((s1 . m) - g) + ((s2 . m) - g9)).| ;

n1 <= n by XXREAL_0:25;

then n + n1 <= n + m by A7, XREAL_1:7;

then n1 <= m by XREAL_1:6;

then |.((s1 . m) - g).| < p / 2 by A5;

then |.((s1 . m) - g).| + |.((s2 . m) - g9).| < (p / 2) + (p / 2) by A8, XREAL_1:8;

then (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) + |.(((s1 + s2) . m) - g1).| < p + (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) by A9, COMPLEX1:56, XREAL_1:8;

hence |.((s . m) - g1).| < p by A1, XREAL_1:6; :: thesis: verum