let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for s being sequence of X st s is convergent holds
lim (z * s) = z * (lim s)
let z be Element of X; :: thesis: for s being sequence of X st s is convergent holds
lim (z * s) = z * (lim s)
let s be sequence of X; :: thesis: ( s is convergent implies lim (z * s) = z * (lim s) )
assume A1: s is convergent ; :: thesis: lim (z * s) = z * (lim s)
set g1 = lim s;
set g = z * (lim s);
A2: 0 + 0 < ||.z.|| + 1 by CLVECT_1:106, XREAL_1:10;
A3: 0 <= ||.z.|| by CLVECT_1:106;

A4: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((z * s) . m) - (z * (lim s))).|| < p )
assume A5: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((z * s) . m) - (z * (lim s))).|| < p
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A1, A2, CLVECT_1:def 18;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
||.(((z * s) . m) - (z * (lim s))).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.(((z * s) . m) - (z * (lim s))).|| < p )
assume n <= m ; :: thesis: ||.(((z * s) . m) - (z * (lim s))).|| < p
then A7: ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A6;
0 <= ||.((s . m) - (lim s)).|| by CLVECT_1:106;
then A8: ||.z.|| * ||.((s . m) - (lim s)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A3, A7, XREAL_1:68;
||.(z * ((s . m) - (lim s))).|| <= ||.z.|| * ||.((s . m) - (lim s)).|| by CLOPBAN3:42;
then A9: ||.(z * ((s . m) - (lim s))).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A8, XXREAL_0:2;
A10: ||.(((z * s) . m) - (z * (lim s))).|| = ||.((z * (s . m)) - (z * (lim s))).|| by CLOPBAN3:def 8
.= ||.(z * ((s . m) - (lim s))).|| by CLOPBAN3:42 ;
0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:10;
then A11: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A3, A5, XREAL_1:99;
(||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A2, XCMPLX_1:88;
hence ||.(((z * s) . m) - (z * (lim s))).|| < p by A10, A9, A11, XXREAL_0:2; :: thesis: verum

end;

z * s is convergent by A1, Th4;
hence lim (z * s) = z * (lim s) by A4, CLVECT_1:def 18; :: thesis: verum