let s, s1 be Complex_Sequence; :: thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim |.(s (#) s1).| = 0 )
assume A1: ( s is convergent & s1 is bounded & lim s = 0c ) ; :: thesis: lim |.(s (#) s1).| = 0
then s (#) s1 is convergent by COMSEQ_2:42;
hence lim |.(s (#) s1).| = |.(lim (s (#) s1)).| by Th27
.= 0 by A1, COMPLEX1:44, COMSEQ_2:43 ;
:: thesis: verum