theorem Th17: :: COMSEQ_3:17

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