theorem Th43: :: CONVEX4:43
for a being Real
for z being Complex holds Im (a * z) = a * (Im z)