theorem Th40: :: COMSEQ_3:40

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