let s be Complex_Sequence; :: thesis: ( s = s1 (#) s2 implies s is convergent )
assume A1: s = s1 (#) s2 ; :: thesis: s is convergent
consider g1 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) - g1).| < p by Def5;
consider g2 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) - g2).| < p by Def5;
take g = g1 * g2; :: 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) - g).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p )
consider R being Real such that
A4: 0 < R and
A5: for n being Nat holds |.(s1 . n).| < R by Th8;
A6: 0 + 0 < |.g2.| + R by A4, COMPLEX1:46, XREAL_1:8;
assume A7: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p
then consider n1 being Nat such that
A8: for m being Nat st n1 <= m holds
|.((s1 . m) - g1).| < p / (|.g2.| + R) by A2, A6;
consider n2 being Nat such that
A9: for m being Nat st n2 <= m holds
|.((s2 . m) - g2).| < p / (|.g2.| + R) by A3, A6, A7;
take n = n1 + n2; :: thesis: for m being Nat st n <= m holds
|.((s . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.((s . m) - g).| < p )
assume A10: n <= m ; :: thesis: |.((s . m) - g).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A10, XXREAL_0:2;
then A11: |.((s1 . m) - g1).| <= p / (|.g2.| + R) by A8;
( 0 <= |.g2.| & |.(((s1 . m) - g1) * g2).| = |.g2.| * |.((s1 . m) - g1).| ) by COMPLEX1:46, COMPLEX1:65;
then A12: |.(((s1 . m) - g1) * g2).| <= |.g2.| * (p / (|.g2.| + R)) by A11, XREAL_1:64;
|.(((s1 (#) s2) . m) - g).| = |.(((((s1 . m) * (s2 . m)) - ((s1 . m) * g2)) + ((s1 . m) * g2)) - (g1 * g2)).| by VALUED_1:5
.= |.(((s1 . m) * ((s2 . m) - g2)) + (((s1 . m) - g1) * g2)).| ;
then A13: |.(((s1 (#) s2) . m) - g).| <= |.((s1 . m) * ((s2 . m) - g2)).| + |.(((s1 . m) - g1) * g2).| by COMPLEX1:56;
n2 <= n by NAT_1:12;
then n2 <= m by A10, XXREAL_0:2;
then A14: |.((s2 . m) - g2).| < p / (|.g2.| + R) by A9;
A15: ( 0 <= |.(s1 . m).| & 0 <= |.((s2 . m) - g2).| ) by COMPLEX1:46;
|.(s1 . m).| < R by A5;
then |.(s1 . m).| * |.((s2 . m) - g2).| < R * (p / (|.g2.| + R)) by A15, A14, XREAL_1:96;
then A16: |.((s1 . m) * ((s2 . m) - g2)).| < R * (p / (|.g2.| + R)) by COMPLEX1:65;
(R * (p / (|.g2.| + R))) + (|.g2.| * (p / (|.g2.| + R))) = (p / (|.g2.| + R)) * (|.g2.| + R)
.= p by A6, XCMPLX_1:87 ;
then |.((s1 . m) * ((s2 . m) - g2)).| + |.(((s1 . m) - g1) * g2).| < p by A16, A12, XREAL_1:8;
hence |.((s . m) - g).| < p by A1, A13, XXREAL_0:2; :: thesis: verum