for s being Complex_Sequence st s is convergent holds
lim (s *') = (lim s) *'