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 )
A1: 0 <= ||.z.|| by NORMSP_1:4;
assume s is convergent ; :: thesis: s * z 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 = g1 * z; :: according to NORMSP_1:def 6 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= ||.(((s * z) . b₃) - g).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((s * z) . b₂) - g).|| ) )
A3: 0 + 0 < ||.z.|| + 1 by NORMSP_1:4, XREAL_1:8;
assume A4: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((s * z) . b₂) - 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 ; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= ||.(((s * z) . b₁) - g).|| )
let m be Nat; :: thesis: ( not n <= m or not p <= ||.(((s * z) . m) - g).|| )
assume n <= m ; :: thesis: not p <= ||.(((s * z) . m) - g).||
then A6: ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A5;
A7: ||.(((s . m) - g1) * z).|| <= ||.((s . m) - g1).|| * ||.z.|| 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: (p / (||.z.|| + 1)) * ||.z.|| < (p / (||.z.|| + 1)) * (||.z.|| + 1) by A1, A8, XREAL_1:97;
A10: ||.(((s * z) . m) - g).|| = ||.(((s . m) * z) - (g1 * z)).|| by LOPBAN_3:def 6
.= ||.(((s . m) - g1) * z).|| by LOPBAN_3:38 ;
0 <= ||.((s . m) - g1).|| by NORMSP_1:4;
then ||.((s . m) - g1).|| * ||.z.|| <= (p / (||.z.|| + 1)) * ||.z.|| by A1, A6, XREAL_1:66;
then A11: ||.(((s . m) - g1) * z).|| <= (p / (||.z.|| + 1)) * ||.z.|| by A7, XXREAL_0:2;
(p / (||.z.|| + 1)) * (||.z.|| + 1) = p by A3, XCMPLX_1:87;
hence ||.(((s * z) . m) - g).|| < p by A10, A11, A9, XXREAL_0:2; :: thesis: verum