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 Th11
.= |.((lim s) " ).| by A1, Th35
.= |.(lim s).| " by COMPLEX1:152 ;
:: thesis: verum