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

now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
then A7: 0 < p / (|.(lim s9).| + R) by A5, XREAL_1:139;
then consider n1 being Element of NAT such that
A8: for m being Element of NAT st n1 <= m holds
|.((s . m) - (lim s)).| < p / (|.(lim s9).| + R) by A1, Def5;
consider n2 being Element of NAT such that
A9: for m being Element of NAT st n2 <= m holds
|.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A2, A7, Def5;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p )
assume A10: n <= m ; :: thesis: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A10, XXREAL_0:2;
then A11: |.((s . m) - (lim s)).| <= p / (|.(lim s9).| + R) by A8;
|.(((s . m) - (lim s)) * (lim s9)).| = |.(lim s9).| * |.((s . m) - (lim s)).| by COMPLEX1:65;
then A12: |.(((s . m) - (lim s)) * (lim s9)).| <= |.(lim s9).| * (p / (|.(lim s9).| + R)) by A6, A11, XREAL_1:64;
A13: ( 0 <= |.(s . m).| & 0 <= |.((s9 . m) - (lim s9)).| ) by COMPLEX1:46;
n2 <= n by NAT_1:12;
then n2 <= m by A10, XXREAL_0:2;
then A14: |.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A9;
|.(((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 A15: |.(((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 A4;
then |.(s . m).| * |.((s9 . m) - (lim s9)).| < R * (p / (|.(lim s9).| + R)) by A13, A14, XREAL_1:96;
then A16: |.((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 A5, XCMPLX_1:87 ;
then |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| < p by A16, A12, XREAL_1:8;
hence |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p by A15, XXREAL_0:2; :: thesis: verum

end;

hence lim (s (#) s9) = (lim s) * (lim s9) by A1, A2, Def5; :: thesis: verum