theorem Th46: :: MESFUN7C:46

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