let X be Complex_Banach_Algebra; :: thesis: for s, s' being sequence of X st s is convergent & s' is convergent holds
s * s' is convergent
let s, s' be sequence of X; :: thesis: ( s is convergent & s' is convergent implies s * s' is convergent )
assume that
A1: s is convergent and
A2: s' is convergent ; :: thesis: s * s' is convergent
consider g1 being Point of X such that
A3: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s . m) - g1).|| < p by A1, CLVECT_1:def 16;
consider g2 being Point of X such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s' . m) - g2).|| < p by A2, CLVECT_1:def 16;
take g = g1 * g2; :: according to CLVECT_1:def 16 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= ||.(((s * s') . b₃) - g).|| ) )
||.s.|| is bounded by A1, CLVECT_1:119, SEQ_2:27;
then ||.s.|| is bounded_above ;
then consider R being real number such that
A5: for n being Element of NAT holds ||.s.|| . n < R by SEQ_2:def 3;
||.(s . 1).|| = ||.s.|| . 1 by CLVECT_1:def 17;
then 0 <= ||.s.|| . 1 by CLVECT_1:106;
then A6: 0 < R by A5;

A7: now

let n be Element of NAT ; :: thesis: ||.(s . n).|| < R
||.(s . n).|| = ||.s.|| . n by CLVECT_1:def 17;
hence ||.(s . n).|| < R by A5; :: thesis: verum

end;

reconsider R = R as Real by XREAL_0:def 1;
A8: 0 <= ||.g2.|| by CLVECT_1:106;
A9: 0 + 0 < ||.g2.|| + R by A6, CLVECT_1:106, XREAL_1:10;
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((s * s') . b₂) - g).|| ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((s * s') . b₂) - g).|| )
then A10: 0 < p / (||.g2.|| + R) by A9;
then consider n1 being Element of NAT such that
A11: for m being Element of NAT st n1 <= m holds
||.((s . m) - g1).|| < p / (||.g2.|| + R) by A3;
consider n2 being Element of NAT such that
A12: for m being Element of NAT st n2 <= m holds
||.((s' . m) - g2).|| < p / (||.g2.|| + R) by A4, A10;
take n = n1 + n2; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= ||.(((s * s') . b₁) - g).|| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= ||.(((s * s') . m) - g).|| )
assume A13: n <= m ; :: thesis: not p <= ||.(((s * s') . m) - g).||
A14: 0 <= ||.(s . m).|| by CLVECT_1:106;
A15: 0 <= ||.((s' . m) - g2).|| by CLVECT_1:106;
n2 <= n by NAT_1:12;
then n2 <= m by A13, XXREAL_0:2;
then A16: ||.((s' . m) - g2).|| < p / (||.g2.|| + R) by A12;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A13, XXREAL_0:2;
then A17: ||.((s . m) - g1).|| <= p / (||.g2.|| + R) by A11;
||.(((s * s') . m) - g).|| = ||.(((s . m) * (s' . m)) - (g1 * g2)).|| by CLOPBAN3:def 10
.= ||.((((s . m) * (s' . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3:42
.= ||.(((s . m) * ((s' . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3:42
.= ||.(((s . m) * ((s' . m) - g2)) + (((s . m) - g1) * g2)).|| by CLOPBAN3:42 ;
then A18: ||.(((s * s') . m) - g).|| <= ||.((s . m) * ((s' . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| by CLVECT_1:def 11;
||.(s . m).|| < R by A7;
then A19: ||.(s . m).|| * ||.((s' . m) - g2).|| < R * (p / (||.g2.|| + R)) by A14, A15, A16, XREAL_1:98;
||.((s . m) * ((s' . m) - g2)).|| <= ||.(s . m).|| * ||.((s' . m) - g2).|| by CLOPBAN3:42;
then A20: ||.((s . m) * ((s' . m) - g2)).|| < R * (p / (||.g2.|| + R)) by A19, XXREAL_0:2;
A21: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * ||.((s . m) - g1).|| by CLOPBAN3:42;
||.g2.|| * ||.((s . m) - g1).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A8, A17, XREAL_1:66;
then A22: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A21, XXREAL_0:2;
(R * (p / (||.g2.|| + R))) + (||.g2.|| * (p / (||.g2.|| + R))) = (p / (||.g2.|| + R)) * (||.g2.|| + R)
.= p by A9, XCMPLX_1:88 ;
then ||.((s . m) * ((s' . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| < p by A20, A22, XREAL_1:10;
hence not p <= ||.(((s * s') . m) - g).|| by A18, XXREAL_0:2; :: thesis: verum