let s be Complex_Sequence; ( s = s1 (#) s2 implies s is convergent )
assume A1:
s = s1 (#) s2
; 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; COMSEQ_2:def 5 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; ( 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
; 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; for m being Nat st n <= m holds
|.((s . m) - g).| < p
let m be Nat; ( n <= m implies |.((s . m) - g).| < p )
assume A10:
n <= m
; |.((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; verum