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 5 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((s (#) s1) . m) - g).| < p
consider R being Real such that
A4: 0 < R and
A5: for m being Nat holds |.(s1 . m).| < R by A2, Th8;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((s (#) s1) . m) - g).| < p )
assume A6: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((s (#) s1) . m) - g).| < p
A7: 0 < p / R by A6, A4;
then consider n1 being Nat such that
A8: for m being Nat st n1 <= m holds
|.((s . m) - 0c).| < p / R by A1, A3, Def6;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.(((s (#) s1) . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((s (#) s1) . m) - g).| < p )
assume A9: n <= m ; :: thesis: |.(((s (#) s1) . m) - g).| < p
A10: |.(((s (#) s1) . m) - g).| = |.((s . m) * (s1 . m)).| by VALUED_1:5
.= |.(s . m).| * |.(s1 . m).| by COMPLEX1:65 ;
|.(s . m).| = |.((s . m) - 0c).| ;
then A11: |.(s . m).| < p / R by A8, A9;

now :: thesis: ( |.(s1 . m).| <> 0 implies |.(((s (#) s1) . m) - g).| < p )

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

end;

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