let s, s1 be Complex_Sequence; :: thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim ((s (#) s1) *') = 0c )

assume A1: ( s is convergent & s1 is bounded & lim s = 0c ) ; :: thesis: lim ((s (#) s1) *') = 0c

then s (#) s1 is convergent by Th29;

hence lim ((s (#) s1) *') = (lim (s (#) s1)) *' by Th11

.= 0c by A1, Th30, COMPLEX1:28 ;

:: thesis: verum

assume A1: ( s is convergent & s1 is bounded & lim s = 0c ) ; :: thesis: lim ((s (#) s1) *') = 0c

then s (#) s1 is convergent by Th29;

hence lim ((s (#) s1) *') = (lim (s (#) s1)) *' by Th11

.= 0c by A1, Th30, COMPLEX1:28 ;

:: thesis: verum