theorem Th1: :: INTEGR16:1

for z being Complex
for r being Real holds
( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) )