let s, s' be Complex_Sequence; :: thesis: ( s is convergent Complex_Sequence & s' is convergent Complex_Sequence implies lim (s (#) s') = (lim s) * (lim s') )
assume that
A1: s is convergent Complex_Sequence and
A2: s' is convergent Complex_Sequence ; :: thesis: lim (s (#) s') = (lim s) * (lim s')
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 s').| + R by A3, COMPLEX1:132, XREAL_1:10;
A6: 0 <= |.(lim s').| 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 (#) s') . m) - ((lim s) * (lim s'))).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s') . m) - ((lim s) * (lim s'))).| < p
then A8: 0 < p / (|.(lim s').| + 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 s').| + R) by A1, Def5;
consider n2 being Element of NAT such that
A10: for m being Element of NAT st n2 <= m holds
|.((s' . m) - (lim s')).| < p / (|.(lim s').| + R) by A2, A8, Def5;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s') . m) - ((lim s) * (lim s'))).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s (#) s') . m) - ((lim s) * (lim s'))).| < p )
assume A11: n <= m ; :: thesis: |.(((s (#) s') . m) - ((lim s) * (lim s'))).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A12: |.((s . m) - (lim s)).| <= p / (|.(lim s').| + R) by A9;
|.(((s . m) - (lim s)) * (lim s')).| = |.(lim s').| * |.((s . m) - (lim s)).| by COMPLEX1:151;
then A13: |.(((s . m) - (lim s)) * (lim s')).| <= |.(lim s').| * (p / (|.(lim s').| + R)) by A6, A12, XREAL_1:66;
A14: ( 0 <= |.(s . m).| & 0 <= |.((s' . m) - (lim s')).| ) by COMPLEX1:132;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A15: |.((s' . m) - (lim s')).| < p / (|.(lim s').| + R) by A10;
|.(((s (#) s') . m) - ((lim s) * (lim s'))).| = |.(((((s . m) * (s' . m)) - ((s . m) * (lim s'))) + ((s . m) * (lim s'))) - ((lim s) * (lim s'))).| by VALUED_1:5
.= |.(((s . m) * ((s' . m) - (lim s'))) + (((s . m) - (lim s)) * (lim s'))).| ;
then A16: |.(((s (#) s') . m) - ((lim s) * (lim s'))).| <= |.((s . m) * ((s' . m) - (lim s'))).| + |.(((s . m) - (lim s)) * (lim s')).| by COMPLEX1:142;
|.(s . m).| < R by A4;
then |.(s . m).| * |.((s' . m) - (lim s')).| < R * (p / (|.(lim s').| + R)) by A14, A15, XREAL_1:98;
then A17: |.((s . m) * ((s' . m) - (lim s'))).| < R * (p / (|.(lim s').| + R)) by COMPLEX1:151;
(R * (p / (|.(lim s').| + R))) + (|.(lim s').| * (p / (|.(lim s').| + R))) = (p / (|.(lim s').| + R)) * (|.(lim s').| + R)
.= p by A5, XCMPLX_1:88 ;
then |.((s . m) * ((s' . m) - (lim s'))).| + |.(((s . m) - (lim s)) * (lim s')).| < p by A17, A13, XREAL_1:10;
hence |.(((s (#) s') . m) - ((lim s) * (lim s'))).| < p by A16, XXREAL_0:2; :: thesis: verum

end;

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