let s, s9 be Complex_Sequence; :: thesis: ( s is convergent & s9 is convergent implies lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *') )
assume A1: ( s is convergent & s9 is convergent ) ; :: thesis: lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *')
hence lim ((s (#) s9) *') = (lim (s (#) s9)) *' by Th12
.= ((lim s) * (lim s9)) *' by A1, Th30
.= ((lim s) *') * ((lim s9) *') by COMPLEX1:35 ;
:: thesis: verum