let X be Banach_Algebra; for s, s9 being sequence of X st s is convergent & s9 is convergent holds
lim (s * s9) = (lim s) * (lim s9)
let s, s9 be sequence of X; ( s is convergent & s9 is convergent implies lim (s * s9) = (lim s) * (lim s9) )
assume that
A1:
s is convergent
and
A2:
s9 is convergent
; lim (s * s9) = (lim s) * (lim s9)
||.s.|| is bounded
by A1, NORMSP_1:23, SEQ_2:13;
then consider R being Real such that
A3:
for n being Nat holds ||.s.|| . n < R
by SEQ_2:def 3;
set g2 = lim s9;
set g1 = lim s;
set g = (lim s) * (lim s9);
||.(s . 1).|| = ||.s.|| . 1
by NORMSP_0:def 4;
then
0 <= ||.s.|| . 1
by NORMSP_1:4;
then A5:
0 < R
by A3;
reconsider R = R as Real ;
A6:
0 + 0 < ||.(lim s9).|| + R
by A5, NORMSP_1:4, XREAL_1:8;
A7:
0 <= ||.(lim s9).||
by NORMSP_1:4;
A8:
now for p being Real st 0 < p holds
ex n being set st
for m being Nat st n <= m holds
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < plet p be
Real;
( 0 < p implies ex n being set st
for m being Nat st n <= m holds
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p )assume
0 < p
;
ex n being set st
for m being Nat st n <= m holds
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < pthen A9:
0 < p / (||.(lim s9).|| + R)
by A6, XREAL_1:139;
then consider n1 being
Nat such that A10:
for
m being
Nat st
n1 <= m holds
||.((s . m) - (lim s)).|| < p / (||.(lim s9).|| + R)
by A1, NORMSP_1:def 7;
consider n2 being
Nat such that A11:
for
m being
Nat st
n2 <= m holds
||.((s9 . m) - (lim s9)).|| < p / (||.(lim s9).|| + R)
by A2, A9, NORMSP_1:def 7;
take n =
n1 + n2;
for m being Nat st n <= m holds
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < plet m be
Nat;
( n <= m implies ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p )assume A12:
n <= m
;
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p
n1 <= n1 + n2
by NAT_1:12;
then
n1 <= m
by A12, XXREAL_0:2;
then
||.((s . m) - (lim s)).|| <= p / (||.(lim s9).|| + R)
by A10;
then A13:
||.(lim s9).|| * ||.((s . m) - (lim s)).|| <= ||.(lim s9).|| * (p / (||.(lim s9).|| + R))
by A7, XREAL_1:64;
||.(((s . m) - (lim s)) * (lim s9)).|| <= ||.(lim s9).|| * ||.((s . m) - (lim s)).||
by LOPBAN_3:38;
then A14:
||.(((s . m) - (lim s)) * (lim s9)).|| <= ||.(lim s9).|| * (p / (||.(lim s9).|| + R))
by A13, XXREAL_0:2;
A15:
0 <= ||.(s . m).||
by NORMSP_1:4;
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| =
||.(((s . m) * (s9 . m)) - ((lim s) * (lim s9))).||
by LOPBAN_3:def 7
.=
||.((((s . m) * (s9 . m)) - ((s . m) * (lim s9))) + (((s . m) * (lim s9)) - ((lim s) * (lim s9)))).||
by LOPBAN_3:38
.=
||.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) * (lim s9)) - ((lim s) * (lim s9)))).||
by LOPBAN_3:38
.=
||.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) - (lim s)) * (lim s9))).||
by LOPBAN_3:38
;
then A16:
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| <= ||.((s . m) * ((s9 . m) - (lim s9))).|| + ||.(((s . m) - (lim s)) * (lim s9)).||
by NORMSP_1:def 1;
A17:
||.((s . m) * ((s9 . m) - (lim s9))).|| <= ||.(s . m).|| * ||.((s9 . m) - (lim s9)).||
by LOPBAN_3:38;
n2 <= n
by NAT_1:12;
then
n2 <= m
by A12, XXREAL_0:2;
then A18:
||.((s9 . m) - (lim s9)).|| < p / (||.(lim s9).|| + R)
by A11;
A19:
0 <= ||.((s9 . m) - (lim s9)).||
by NORMSP_1:4;
||.(s . m).|| < R
by A4;
then
||.(s . m).|| * ||.((s9 . m) - (lim s9)).|| < R * (p / (||.(lim s9).|| + R))
by A15, A19, A18, XREAL_1:96;
then A20:
||.((s . m) * ((s9 . m) - (lim s9))).|| < R * (p / (||.(lim s9).|| + R))
by A17, XXREAL_0:2;
(R * (p / (||.(lim s9).|| + R))) + (||.(lim s9).|| * (p / (||.(lim s9).|| + R))) =
(p / (||.(lim s9).|| + R)) * (||.(lim s9).|| + R)
.=
p
by A6, XCMPLX_1:87
;
then
||.((s . m) * ((s9 . m) - (lim s9))).|| + ||.(((s . m) - (lim s)) * (lim s9)).|| < p
by A20, A14, XREAL_1:8;
hence
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p
by A16, XXREAL_0:2;
verum end;
s * s9 is convergent
by A1, A2, Th3;
hence
lim (s * s9) = (lim s) * (lim s9)
by A8, NORMSP_1:def 7; verum