let c be Complex_Sequence; :: thesis: ( Re c is convergent & Im c is convergent implies ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) )
assume A1: ( Re c is convergent & Im c is convergent ) ; :: thesis: ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) )
A2: ( ( 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;
then lim c = (lim (Re c)) + ((lim (Im c)) * <i>) by A1, Th39;
hence ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) by A1, A2, Th39, COMPLEX1:12; :: thesis: verum