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 (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 CLVECT_1:105, XREAL_1:8;

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

hence lim (s * z) = (lim s) * z by A4, CLVECT_1:def 16; :: thesis: verum

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 CLVECT_1:105, XREAL_1:8;

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

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

s * z is convergent
by A1, Th5;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 A5: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.(((s * z) . m) - ((lim s) * z)).|| < p

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, A2, CLVECT_1:def 16;

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 CLVECT_1:105;

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 CLOPBAN3: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 CLOPBAN3: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;for m being Nat st n <= m holds

||.(((s * z) . m) - ((lim s) * z)).|| < p )

assume A5: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.(((s * z) . m) - ((lim s) * z)).|| < p

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, A2, CLVECT_1:def 16;

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 CLVECT_1:105;

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 CLOPBAN3: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 CLOPBAN3: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

hence lim (s * z) = (lim s) * z by A4, CLVECT_1:def 16; :: thesis: verum