theorem Th22: :: MESFUN9C:22

for X being non empty set
for D being set
for F being Functional_Sequence of X,COMPLEX holds Im (F || D) = (Im F) || D