let s, s9 be convergent Complex_Sequence; :: thesis: lim (s (#) s9) = (lim s) * (lim s9)
consider R being Real such that
A1: 0 < R and
A2: for n being Nat holds |.(s . n).| < R by Th8;
A3: 0 + 0 < |.(lim s9).| + R by A1, COMPLEX1:46, XREAL_1:8;
A4: 0 <= |.(lim s9).| by COMPLEX1:46;

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 A5: 0 < p / (|.(lim s9).| + R) by A3;
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.((s . m) - (lim s)).| < p / (|.(lim s9).| + R) by Def6;
consider n2 being Nat such that
A7: for m being Nat st n2 <= m holds
|.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A5, Def6;
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 A8: n <= m ; :: thesis: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A8, XXREAL_0:2;
then A9: |.((s . m) - (lim s)).| <= p / (|.(lim s9).| + R) by A6;
|.(((s . m) - (lim s)) * (lim s9)).| = |.(lim s9).| * |.((s . m) - (lim s)).| by COMPLEX1:65;
then A10: |.(((s . m) - (lim s)) * (lim s9)).| <= |.(lim s9).| * (p / (|.(lim s9).| + R)) by A4, A9, XREAL_1:64;
A11: ( 0 <= |.(s . m).| & 0 <= |.((s9 . m) - (lim s9)).| ) by COMPLEX1:46;
n2 <= n by NAT_1:12;
then n2 <= m by A8, XXREAL_0:2;
then A12: |.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A7;
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| = |.(((((s . m) * (s9 . m)) - ((s . m) * (lim s9))) + ((s . m) * (lim s9))) - ((lim s) * (lim s9))).| by VALUED_1:5
.= |.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) - (lim s)) * (lim s9))).| ;
then A13: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| <= |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| by COMPLEX1:56;
|.(s . m).| < R by A2;
then |.(s . m).| * |.((s9 . m) - (lim s9)).| < R * (p / (|.(lim s9).| + R)) by A11, A12, XREAL_1:96;
then A14: |.((s . m) * ((s9 . m) - (lim s9))).| < R * (p / (|.(lim s9).| + R)) by COMPLEX1:65;
(R * (p / (|.(lim s9).| + R))) + (|.(lim s9).| * (p / (|.(lim s9).| + R))) = (p / (|.(lim s9).| + R)) * (|.(lim s9).| + R)
.= p by A3, XCMPLX_1:87 ;
then |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| < p by A14, A10, XREAL_1:8;
hence |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p by A13, XXREAL_0:2; :: thesis: verum

end;

hence lim (s (#) s9) = (lim s) * (lim s9) by Def6; :: thesis: verum