for a, b being Real_Sequence
for c being 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 ) iff c is convergent )