for c being Complex_Sequence st Re c is convergent & Im c is convergent holds
( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) )