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 Th23;
hence lim ((s ") *') = (lim (s ")) *' by Th11
.= ((lim s) ") *' by A1, Th24
.= ((lim s) *') " by COMPLEX1:36 ;
:: thesis: verum