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

A4: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((s * z) . m) - ((lim s) * z)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.(((s * z) . m) - ((lim s) * z)).|| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((s * z) . m) - ((lim s) * z)).|| < p
then A5: 0 < p / (||.z.|| + 1) by A2, XREAL_1:139;
then consider n being Nat such that
A6: for m being Nat st n <= m holds
||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A1, NORMSP_1:def 7;
take n = n; :: thesis: for m being Nat st n <= m holds
||.(((s * z) . m) - ((lim s) * z)).|| < p
let m be Nat; :: thesis: ( n <= m implies ||.(((s * z) . m) - ((lim s) * z)).|| < p )
assume n <= m ; :: thesis: ||.(((s * z) . m) - ((lim s) * z)).|| < p
then A7: ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A6;
0 <= ||.((s . m) - (lim s)).|| by NORMSP_1:4;
then A8: ||.((s . m) - (lim s)).|| * ||.z.|| <= (p / (||.z.|| + 1)) * ||.z.|| by A3, A7, XREAL_1:66;
||.(((s . m) - (lim s)) * z).|| <= ||.((s . m) - (lim s)).|| * ||.z.|| by LOPBAN_3:38;
then A9: ||.(((s . m) - (lim s)) * z).|| <= (p / (||.z.|| + 1)) * ||.z.|| by A8, XXREAL_0:2;
A10: ||.(((s * z) . m) - ((lim s) * z)).|| = ||.(((s . m) * z) - ((lim s) * z)).|| by LOPBAN_3:def 6
.= ||.(((s . m) - (lim s)) * z).|| by LOPBAN_3:38 ;
0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8;
then A11: (p / (||.z.|| + 1)) * ||.z.|| < (p / (||.z.|| + 1)) * (||.z.|| + 1) by A3, A5, XREAL_1:97;
(p / (||.z.|| + 1)) * (||.z.|| + 1) = p by A2, XCMPLX_1:87;
hence ||.(((s * z) . m) - ((lim s) * z)).|| < p by A10, A9, A11, XXREAL_0:2; :: thesis: verum

end;

s * z is convergent by A1, Th5;
hence lim (s * z) = (lim s) * z by A4, NORMSP_1:def 7; :: thesis: verum