let X be Banach_Algebra; 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; ( s is convergent & s9 is convergent implies s * s9 is convergent )
assume that
A1:
s is convergent
and
A2:
s9 is convergent
; 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, NORMSP_1:23, SEQ_2:13;
then consider R being Real such that
A4:
for n being Nat holds ||.s.|| . n < R
by SEQ_2:def 3;
||.(s . 1).|| = ||.s.|| . 1
by NORMSP_0:def 4;
then
0 <= ||.s.|| . 1
by NORMSP_1:4;
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; NORMSP_1:def 6 for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= ||.(((s * s9) . b3) - g).|| ) )
let p be Real; ( p <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.(((s * s9) . b2) - g).|| ) )
reconsider R = R as Real ;
A8:
0 + 0 < ||.g2.|| + R
by A6, NORMSP_1:4, XREAL_1:8;
assume A9:
0 < p
; ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.(((s * s9) . b2) - 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, XREAL_1:139;
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, XREAL_1:139;
take n = n1 + n2; for b1 being set holds
( not n <= b1 or not p <= ||.(((s * s9) . b1) - g).|| )
let m be Nat; ( not n <= m or not p <= ||.(((s * s9) . m) - g).|| )
assume A12:
n <= m
; 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 NORMSP_1:4;
A15:
||.((s . m) * ((s9 . m) - g2)).|| <= ||.(s . m).|| * ||.((s9 . m) - g2).||
by LOPBAN_3:38;
A16:
0 <= ||.((s9 . m) - g2).||
by NORMSP_1:4;
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 LOPBAN_3:38
.=
||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).||
by LOPBAN_3:38
.=
||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).||
by LOPBAN_3:38
;
then A18:
||.(((s * s9) . m) - g).|| <= ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||
by NORMSP_1:def 1;
||.(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 LOPBAN_3:38;
0 <= ||.g2.||
by NORMSP_1:4;
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
||.(((s * s9) . m) - g).|| < p
by A18, XXREAL_0:2; verum