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;

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_{1} being object holds

( b_{1} <= 0 or ex b_{2} being set st

for b_{3} being set holds

( not b_{2} <= b_{3} or not b_{1} <= ||.(((s * s9) . b_{3}) - g).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.(((s * s9) . b_{2}) - 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_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.(((s * s9) . b_{2}) - 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_{1} being set holds

( not n <= b_{1} or not p <= ||.(((s * s9) . b_{1}) - 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

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

||.(s . 1).|| = ||.s.|| . 1
by NORMSP_0:def 4;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 . n).|| = ||.s.|| . n by NORMSP_0:def 4;

hence ||.(s . n).|| < R by A4; :: thesis: verum

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

( b

for b

( not b

let p be Real; :: thesis: ( p <= 0 or ex b

for b

( not b

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

for b

( not b

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

( not n <= b

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