theorem Th39: :: COMSEQ_3:39

for a, b being convergent Real_Sequence
for c being Complex_Sequence st ( for n being Nat holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds
( c is convergent & lim c = (lim a) + ((lim b) * <i>) )