theorem Th47: :: MESFUN7C:47

for c being FinSequence of COMPLEX
for n being Nat st n in dom (Im c) holds
(Im c) . n = Im (c . n)