theorem Th6: :: INTEGR16:6

for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Im (F ^ <*x*>) = (Im F) ^ <*(Im x)*>