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