let s, s9 be convergent Complex_Sequence; :: thesis: lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *')
thus lim ((s (#) s9) *') = (lim (s (#) s9)) *' by Th11
.= ((lim s) * (lim s9)) *' by Th20
.= ((lim s) *') * ((lim s9) *') by COMPLEX1:35 ; :: thesis: verum