let s be Complex_Sequence; :: thesis: ( s is convergent & lim s <> 0c & s is non-empty implies lim ((s ") *') = ((lim s) *') " )
assume A1: ( s is convergent & lim s <> 0c & s is non-empty ) ; :: 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:36 ;
:: thesis: verum