let X be Banach_Algebra; for z being Element of X
for s being sequence of X st s is convergent holds
z * s is convergent
let z be Element of X; for s being sequence of X st s is convergent holds
z * s is convergent
let s be sequence of X; ( s is convergent implies z * s is convergent )
A1:
0 <= ||.z.||
by NORMSP_1:4;
assume
s is convergent
; z * s is convergent
then consider g1 being Point of X such that
A2:
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
;
take g = z * g1; 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 <= ||.(((z * s) . 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 <= ||.(((z * s) . b2) - g).|| ) )
A3:
0 + 0 < ||.z.|| + 1
by NORMSP_1:4, XREAL_1:8;
assume A4:
0 < p
; ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.(((z * s) . b2) - g).|| )
then consider n being Nat such that
A5:
for m being Nat st n <= m holds
||.((s . m) - g1).|| < p / (||.z.|| + 1)
by A2, A3, XREAL_1:139;
take
n
; for b1 being set holds
( not n <= b1 or not p <= ||.(((z * s) . b1) - g).|| )
let m be Nat; ( not n <= m or not p <= ||.(((z * s) . m) - g).|| )
assume
n <= m
; not p <= ||.(((z * s) . m) - g).||
then A6:
||.((s . m) - g1).|| < p / (||.z.|| + 1)
by A5;
A7:
||.(z * ((s . m) - g1)).|| <= ||.z.|| * ||.((s . m) - g1).||
by LOPBAN_3:38;
A8:
0 + ||.z.|| < ||.z.|| + 1
by XREAL_1:8;
0 < p / (||.z.|| + 1)
by A3, A4, XREAL_1:139;
then A9:
||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1))
by A1, A8, XREAL_1:97;
A10: ||.(((z * s) . m) - g).|| =
||.((z * (s . m)) - (z * g1)).||
by LOPBAN_3:def 5
.=
||.(z * ((s . m) - g1)).||
by LOPBAN_3:38
;
0 <= ||.((s . m) - g1).||
by NORMSP_1:4;
then
||.z.|| * ||.((s . m) - g1).|| <= ||.z.|| * (p / (||.z.|| + 1))
by A1, A6, XREAL_1:66;
then A11:
||.(z * ((s . m) - g1)).|| <= ||.z.|| * (p / (||.z.|| + 1))
by A7, XXREAL_0:2;
(||.z.|| + 1) * (p / (||.z.|| + 1)) = p
by A3, XCMPLX_1:87;
hence
||.(((z * s) . m) - g).|| < p
by A10, A11, A9, XXREAL_0:2; verum