let s, s1 be Complex_Sequence; :: thesis: ( s is convergent & s1 is bounded & lim s = 0c implies s (#) s1 is convergent )
assume that
A1: s is convergent and
A2: s1 is bounded and
A3: lim s = 0c ; :: thesis: s (#) s1 is convergent
take g = 0c ; :: according to COMSEQ_2:def 4 :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - g).| < p
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) - g).| < p )
assume A4: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - g).| < p
consider R being Real such that
A5: 0 < R and
A6: for m being Element of NAT holds |.(s1 . m).| < R by A2, Th8;
A7: 0 < p / R by A4, A5, XREAL_1:141;
then consider n1 being Element of NAT such that
A8: 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) - g).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s (#) s1) . m) - g).| < p )
assume A9: n <= m ; :: thesis: |.(((s (#) s1) . m) - g).| < p
|.(s . m).| = |.((s . m) - 0c ).| ;
then A10: |.(s . m).| < p / R by A8, A9;
A11: |.(((s (#) s1) . m) - g).| = |.((s . m) * (s1 . m)).| by VALUED_1:5
.= |.(s . m).| * |.(s1 . m).| by COMPLEX1:151 ;

now

assume A12: |.(s1 . m).| <> 0 ; :: thesis: |.(((s (#) s1) . m) - g).| < p
(p / R) * R = (p * (R " )) * R by XCMPLX_0:def 9
.= p * ((R " ) * R)
.= p * 1 by A5, XCMPLX_0:def 7
.= p ;
then A13: (p / R) * |.(s1 . m).| < p by A6, A7, XREAL_1:70;
0 <= |.(s1 . m).| by COMPLEX1:132;
then |.(((s (#) s1) . m) - g).| < (p / R) * |.(s1 . m).| by A10, A11, A12, XREAL_1:70;
hence |.(((s (#) s1) . m) - g).| < p by A13, XXREAL_0:2; :: thesis: verum

end;

hence |.(((s (#) s1) . m) - g).| < p by A4, A11; :: thesis: verum