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:132, XREAL_1:10;
A6: 0 <= |.(lim s9).| by COMPLEX1:132;

A7: 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 A8: 0 < p / (|.(lim s9).| + R) by A5, XREAL_1:141;
then consider n1 being Element of NAT such that
A9: 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
A10: for m being Element of NAT st n2 <= m holds
|.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A2, A8, 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 A11: n <= m ; :: thesis: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A12: |.((s . m) - (lim s)).| <= p / (|.(lim s9).| + R) by A9;
|.(((s . m) - (lim s)) * (lim s9)).| = |.(lim s9).| * |.((s . m) - (lim s)).| by COMPLEX1:151;
then A13: |.(((s . m) - (lim s)) * (lim s9)).| <= |.(lim s9).| * (p / (|.(lim s9).| + R)) by A6, A12, XREAL_1:66;
A14: ( 0 <= |.(s . m).| & 0 <= |.((s9 . m) - (lim s9)).| ) by COMPLEX1:132;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A15: |.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A10;
|.(((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 A16: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| <= |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| by COMPLEX1:142;
|.(s . m).| < R by A4;
then |.(s . m).| * |.((s9 . m) - (lim s9)).| < R * (p / (|.(lim s9).| + R)) by A14, A15, XREAL_1:98;
then A17: |.((s . m) * ((s9 . m) - (lim s9))).| < R * (p / (|.(lim s9).| + R)) by COMPLEX1:151;
(R * (p / (|.(lim s9).| + R))) + (|.(lim s9).| * (p / (|.(lim s9).| + R))) = (p / (|.(lim s9).| + R)) * (|.(lim s9).| + R)
.= p by A5, XCMPLX_1:88 ;
then |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| < p by A17, A13, XREAL_1:10;
hence |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p by A16, XXREAL_0:2; :: thesis: verum

end;

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