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:66 ;
:: thesis: verum