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) )
A1: for n being Element of NAT holds (Re c) . n = Re (c . n) by Def3;
for n being Element of NAT holds (Im c) . n = Im (c . n) by Def4;
hence ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) ) by A1, Th40; :: thesis: verum