let X be Complex_Banach_Algebra; :: thesis: 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; :: thesis: for s being sequence of X st s is convergent holds
z * s is convergent
let s be sequence of X; :: thesis: ( s is convergent implies z * s is convergent )
assume A1: s is convergent ; :: thesis: z * s 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, CLVECT_1:def 16;
take g = z * g1; :: according to CLVECT_1:def 16 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= ||.(((z * s) . b₃) - g).|| ) )
A3: 0 <= ||.z.|| by CLVECT_1:106;
A4: 0 + 0 < ||.z.|| + 1 by CLVECT_1:106, XREAL_1:10;
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((z * s) . b₂) - g).|| ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((z * s) . b₂) - g).|| )
then A5: 0 < p / (||.z.|| + 1) by A4;
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 b₁ being Element of NAT holds
( not n <= b₁ or not p <= ||.(((z * s) . b₁) - g).|| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= ||.(((z * s) . m) - g).|| )
assume A7: n <= m ; :: thesis: not p <= ||.(((z * s) . m) - g).||
A8: ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A6, A7;
A9: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by CLOPBAN3:def 8
.= ||.(z * ((s . m) - g1)).|| by CLOPBAN3:42 ;
A10: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * ||.((s . m) - g1).|| by CLOPBAN3:42;
0 <= ||.((s . m) - g1).|| by CLVECT_1:106;
then ||.z.|| * ||.((s . m) - g1).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A3, A8, XREAL_1:68;
then A11: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A10, XXREAL_0:2;
0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:10;
then A12: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A3, A5, XREAL_1:99;
(||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A4, XCMPLX_1:88;
hence not p <= ||.(((z * s) . m) - g).|| by A9, A11, A12, XXREAL_0:2; :: thesis: verum