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 :: 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) - 0c).| < p
consider R being Real such that
A5: 0 < R and
A6: for m being Nat holds |.(s1 . m).| < R by ;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p )

assume A7: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p

A8: 0 < p / R by A7, A5;
then consider n1 being Nat such that
A9: 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) - 0c).| < p

let m be 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 ;
then A10: (p / R) * |.(s1 . m).| < p by ;
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:65 ;
A13: 0 <= |.(s1 . m).| by COMPLEX1:46;
now :: thesis: ( |.(s1 . m).| <> 0 implies |.(((s (#) s1) . m) - 0c).| < p )
assume |.(s1 . m).| <> 0 ; :: thesis: |.(((s (#) s1) . m) - 0c).| < p
then |.(((s (#) s1) . m) - 0c).| < (p / R) * |.(s1 . m).| by ;
hence |.(((s (#) s1) . m) - 0c).| < p by ; :: thesis: verum
end;
hence |.(((s (#) s1) . m) - 0c).| < p by ; :: thesis: verum
end;
s (#) s1 is convergent by A1, A2, A3, Th29;
hence lim (s (#) s1) = 0c by ; :: thesis: verum