let X be Complex_Banach_Algebra; :: thesis: for s, s9 being sequence of X st s is convergent & s9 is convergent holds
s * s9 is convergent
let s, s9 be sequence of X; :: thesis: ( s is convergent & s9 is convergent implies s * s9 is convergent )
assume that
A1: s is convergent and
A2: s9 is convergent ; :: thesis: s * s9 is convergent
consider g1 being Point of X such that
A3: 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 by A1;
||.s.|| is bounded by A1, CLVECT_1:117, SEQ_2:13;
then consider R being Real such that
A4: for n being Nat holds ||.s.|| . n < R by SEQ_2:def 3;

A5: now :: thesis: for n being Nat holds ||.(s . n).|| < R

let n be Nat; :: thesis: ||.(s . n).|| < R
||.(s . n).|| = ||.s.|| . n by NORMSP_0:def 4;
hence ||.(s . n).|| < R by A4; :: thesis: verum

end;

||.(s . 1).|| = ||.s.|| . 1 by NORMSP_0:def 4;
then 0 <= ||.s.|| . 1 by CLVECT_1:105;
then A6: 0 < R by A4;
consider g2 being Point of X such that
A7: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((s9 . m) - g2).|| < p by A2;
take g = g1 * g2; :: according to CLVECT_1:def 15 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= ||.(((s * s9) . b₃) - g).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((s * s9) . b₂) - g).|| ) )
reconsider R = R as Real ;
A8: 0 + 0 < ||.g2.|| + R by A6, CLVECT_1:105, XREAL_1:8;
assume A9: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((s * s9) . b₂) - g).|| )
then consider n1 being Nat such that
A10: for m being Nat st n1 <= m holds
||.((s . m) - g1).|| < p / (||.g2.|| + R) by A3, A8;
consider n2 being Nat such that
A11: for m being Nat st n2 <= m holds
||.((s9 . m) - g2).|| < p / (||.g2.|| + R) by A7, A8, A9;
take n = n1 + n2; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= ||.(((s * s9) . b₁) - g).|| )
let m be Nat; :: thesis: ( not n <= m or not p <= ||.(((s * s9) . m) - g).|| )
assume A12: n <= m ; :: thesis: not p <= ||.(((s * s9) . m) - g).||
n2 <= n by NAT_1:12;
then n2 <= m by A12, XXREAL_0:2;
then A13: ||.((s9 . m) - g2).|| < p / (||.g2.|| + R) by A11;
A14: 0 <= ||.(s . m).|| by CLVECT_1:105;
A15: ||.((s . m) * ((s9 . m) - g2)).|| <= ||.(s . m).|| * ||.((s9 . m) - g2).|| by CLOPBAN3:38;
A16: 0 <= ||.((s9 . m) - g2).|| by CLVECT_1:105;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A12, XXREAL_0:2;
then A17: ||.((s . m) - g1).|| <= p / (||.g2.|| + R) by A10;
||.(((s * s9) . m) - g).|| = ||.(((s . m) * (s9 . m)) - (g1 * g2)).|| by LOPBAN_3:def 7
.= ||.((((s . m) * (s9 . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3:38
.= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3:38
.= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).|| by CLOPBAN3:38 ;
then A18: ||.(((s * s9) . m) - g).|| <= ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| by CLVECT_1:def 13;
||.(s . m).|| < R by A5;
then ||.(s . m).|| * ||.((s9 . m) - g2).|| < R * (p / (||.g2.|| + R)) by A14, A16, A13, XREAL_1:96;
then A19: ||.((s . m) * ((s9 . m) - g2)).|| < R * (p / (||.g2.|| + R)) by A15, XXREAL_0:2;
A20: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * ||.((s . m) - g1).|| by CLOPBAN3:38;
0 <= ||.g2.|| by CLVECT_1:105;
then ||.g2.|| * ||.((s . m) - g1).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A17, XREAL_1:64;
then A21: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A20, XXREAL_0:2;
(R * (p / (||.g2.|| + R))) + (||.g2.|| * (p / (||.g2.|| + R))) = (p / (||.g2.|| + R)) * (||.g2.|| + R)
.= p by A8, XCMPLX_1:87 ;
then ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| < p by A19, A21, XREAL_1:8;
hence not p <= ||.(((s * s9) . m) - g).|| by A18, XXREAL_0:2; :: thesis: verum