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 COMSEQ_2:34;
hence lim |.(s ").| = |.(lim (s ")).| by Th27
.= |.((lim s) ").| by A1, COMSEQ_2:35
.= |.(lim s).| " by COMPLEX1:66 ;
:: thesis: verum