let X be Banach_Algebra; 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; for s being sequence of X st s is convergent holds
lim (s * z) = (lim s) * z
let s be sequence of X; ( s is convergent implies lim (s * z) = (lim s) * z )
assume A1:
s is convergent
; 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 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)).|| < plet p be
Real;
( 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
;
ex n being Nat st
for m being Nat st n <= m holds
||.(((s * z) . m) - ((lim s) * z)).|| < pthen 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;
for m being Nat st n <= m holds
||.(((s * z) . m) - ((lim s) * z)).|| < plet m be
Nat;
( n <= m implies ||.(((s * z) . m) - ((lim s) * z)).|| < p )assume
n <= m
;
||.(((s * z) . m) - ((lim s) * z)).|| < pthen 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;
verum end;
s * z is convergent
by A1, Th5;
hence
lim (s * z) = (lim s) * z
by A4, NORMSP_1:def 7; verum