theorem :: SEQ_2:33

for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds
lim |.(s ").| = |.(lim s).| "