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

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