let X be Banach_Algebra; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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);

A4: now :: thesis: for n being Nat holds ||.(s . n).|| < R

let n be Nat; :: thesis: ||.(s . n).|| < R
||.(s . n).|| = ||.s.|| . n by NORMSP_0:def 4;
hence ||.(s . n).|| < R by A3; :: thesis: verum

end;

||.(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 :: thesis: 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))).|| < p

let p be Real; :: thesis: ( 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 ; :: thesis: ex n being set st
for m being Nat st n <= m holds
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p
then 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; :: thesis: for m being Nat st n <= m holds
||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p
let m be Nat; :: thesis: ( n <= m implies ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p )
assume A12: n <= m ; :: thesis: ||.(((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; :: thesis: verum

end;

s * s9 is convergent by A1, A2, Th3;
hence lim (s * s9) = (lim s) * (lim s9) by A8, NORMSP_1:def 7; :: thesis: verum