theorem Th24: :: MESFUN7C:24

for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )