let c be convergent Complex_Sequence; :: thesis: ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) )
( ( for n being Nat holds (Re c) . n = Re (c . n) ) & ( for n being Nat holds (Im c) . n = Im (c . n) ) ) by Def5, Def6;
hence ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) ) by Th40; :: thesis: verum