let X be Banach_Algebra; :: thesis: for z being Element of X
for s being sequence of X st s is convergent holds
s * z is convergent
let z be Element of X; :: thesis: for s being sequence of X st s is convergent holds
s * z is convergent
let s be sequence of X; :: thesis: ( s is convergent implies s * z is convergent )
assume A1:
s is convergent
; :: thesis: s * z is convergent
consider g1 being Point of X such that
A2:
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, NORMSP_1:def 9;
take g = g1 * z; :: according to NORMSP_1:def 9 :: thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.(((s * z) . b3) - g).|| ) )
A3:
0 <= ||.z.||
by NORMSP_1:8;
A4:
0 + 0 < ||.z.|| + 1
by NORMSP_1:8, XREAL_1:10;
let p be Real; :: thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.(((s * z) . b2) - g).|| ) )
assume
0 < p
; :: thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.(((s * z) . b2) - g).|| )
then A5:
0 < p / (||.z.|| + 1)
by A4, XREAL_1:141;
then consider n being Element of NAT such that
A6:
for m being Element of NAT st n <= m holds
||.((s . m) - g1).|| < p / (||.z.|| + 1)
by A2;
take
n
; :: thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= ||.(((s * z) . b1) - g).|| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= ||.(((s * z) . m) - g).|| )
assume A7:
n <= m
; :: thesis: not p <= ||.(((s * z) . m) - g).||
A8:
||.((s . m) - g1).|| < p / (||.z.|| + 1)
by A6, A7;
A9: ||.(((s * z) . m) - g).|| =
||.(((s . m) * z) - (g1 * z)).||
by LOPBAN_3:def 10
.=
||.(((s . m) - g1) * z).||
by LOPBAN_3:43
;
A10:
||.(((s . m) - g1) * z).|| <= ||.((s . m) - g1).|| * ||.z.||
by LOPBAN_3:43;
0 <= ||.((s . m) - g1).||
by NORMSP_1:8;
then
||.((s . m) - g1).|| * ||.z.|| <= (p / (||.z.|| + 1)) * ||.z.||
by A3, A8, XREAL_1:68;
then A11:
||.(((s . m) - g1) * z).|| <= (p / (||.z.|| + 1)) * ||.z.||
by A10, XXREAL_0:2;
0 + ||.z.|| < ||.z.|| + 1
by XREAL_1:10;
then A12:
(p / (||.z.|| + 1)) * ||.z.|| < (p / (||.z.|| + 1)) * (||.z.|| + 1)
by A3, A5, XREAL_1:99;
(p / (||.z.|| + 1)) * (||.z.|| + 1) = p
by A4, XCMPLX_1:88;
hence
||.(((s * z) . m) - g).|| < p
by A9, A11, A12, XXREAL_0:2; :: thesis: verum