theorem Th42: :: CONVEX4:42

for a being Real
for z being Complex holds Re (a * z) = a * (Re z)