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 )

A1: 0 <= ||.z.|| by CLVECT_1:105;

assume s is convergent ; :: thesis: 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; :: according to CLVECT_1:def 15 :: thesis: for b_{1} being object holds

( b_{1} <= 0 or ex b_{2} being set st

for b_{3} being set holds

( not b_{2} <= b_{3} or not b_{1} <= ||.(((z * s) . b_{3}) - g).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.(((z * s) . b_{2}) - g).|| ) )

assume A3: 0 < p ; :: thesis: ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.(((z * s) . b_{2}) - g).|| )

A4: 0 + 0 < ||.z.|| + 1 by CLVECT_1:105, XREAL_1:8;

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;

take n ; :: thesis: for b_{1} being set holds

( not n <= b_{1} or not p <= ||.(((z * s) . b_{1}) - g).|| )

let m be Nat; :: thesis: ( not n <= m or not p <= ||.(((z * s) . m) - g).|| )

assume n <= m ; :: thesis: 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 CLOPBAN3:38;

0 <= ||.((s . m) - g1).|| by CLVECT_1:105;

then ||.z.|| * ||.((s . m) - g1).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A1, A6, XREAL_1:66;

then A8: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A7, XXREAL_0:2;

A9: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by LOPBAN_3:def 5

.= ||.(z * ((s . m) - g1)).|| by CLOPBAN3:38 ;

0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8;

then A10: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A1, A3, XREAL_1:97;

(||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A4, XCMPLX_1:87;

hence not p <= ||.(((z * s) . m) - g).|| by A9, A8, A10, XXREAL_0:2; :: thesis: verum

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 )

A1: 0 <= ||.z.|| by CLVECT_1:105;

assume s is convergent ; :: thesis: 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; :: according to CLVECT_1:def 15 :: thesis: for b

( b

for b

( not b

let p be Real; :: thesis: ( p <= 0 or ex b

for b

( not b

assume A3: 0 < p ; :: thesis: ex b

for b

( not b

A4: 0 + 0 < ||.z.|| + 1 by CLVECT_1:105, XREAL_1:8;

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;

take n ; :: thesis: for b

( not n <= b

let m be Nat; :: thesis: ( not n <= m or not p <= ||.(((z * s) . m) - g).|| )

assume n <= m ; :: thesis: 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 CLOPBAN3:38;

0 <= ||.((s . m) - g1).|| by CLVECT_1:105;

then ||.z.|| * ||.((s . m) - g1).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A1, A6, XREAL_1:66;

then A8: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A7, XXREAL_0:2;

A9: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by LOPBAN_3:def 5

.= ||.(z * ((s . m) - g1)).|| by CLOPBAN3:38 ;

0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8;

then A10: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A1, A3, XREAL_1:97;

(||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A4, XCMPLX_1:87;

hence not p <= ||.(((z * s) . m) - g).|| by A9, A8, A10, XXREAL_0:2; :: thesis: verum