let s, s1 be Complex_Sequence; :: thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim (s (#) s1) = 0c )
assume that
A1: s is convergent and
A2: s1 is bounded and
A3: lim s = 0c ; :: thesis: lim (s (#) s1) = 0c

A4: now

consider R being Real such that
A5: 0 < R and
A6: for m being Element of NAT holds |.(s1 . m).| < R by A2, Th8;
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 (#) s1) . m) - 0c ).| < p )
assume A7: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - 0c ).| < p
A8: 0 < p / R by A7, 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) - 0c ).| < p / R by A1, A3, Def5;
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - 0c ).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s (#) s1) . m) - 0c ).| < p )
(p / R) * R = (p * (R " )) * R by XCMPLX_0:def 9
.= p * ((R " ) * R)
.= p * 1 by A5, XCMPLX_0:def 7 ;
then A10: (p / R) * |.(s1 . m).| < p by A6, A8, XREAL_1:70;
assume n <= m ; :: thesis: |.(((s (#) s1) . m) - 0c ).| < p
then A11: |.((s . m) - 0c ).| < p / R by A9;
A12: |.(((s (#) s1) . m) - 0c ).| = |.((s . m) * (s1 . m)).| by VALUED_1:5
.= |.(s . m).| * |.(s1 . m).| by COMPLEX1:151 ;
A13: 0 <= |.(s1 . m).| by COMPLEX1:132;

now

assume |.(s1 . m).| <> 0 ; :: thesis: |.(((s (#) s1) . m) - 0c ).| < p
then |.(((s (#) s1) . m) - 0c ).| < (p / R) * |.(s1 . m).| by A11, A12, A13, XREAL_1:70;
hence |.(((s (#) s1) . m) - 0c ).| < p by A10, XXREAL_0:2; :: thesis: verum

end;

hence |.(((s (#) s1) . m) - 0c ).| < p by A7, A12; :: thesis: verum

end;

s (#) s1 is convergent by A1, A2, A3, Th42;
hence lim (s (#) s1) = 0c by A4, Def5; :: thesis: verum