let s be Complex_Sequence; :: thesis: ( s is convergent & lim s <> 0c & s is non-zero implies lim ((s " ) *' ) = ((lim s) *' ) " )
assume A1: ( s is convergent & lim s <> 0c & s is non-zero ) ; :: thesis: lim ((s " ) *' ) = ((lim s) *' ) "
then s " is convergent by Th34;
hence lim ((s " ) *' ) = (lim (s " )) *' by Th12
.= ((lim s) " ) *' by A1, Th35
.= ((lim s) *' ) " by COMPLEX1:122 ;
:: thesis: verum