theorem :: EUCLID_3:19

for z being Complex
for r being Real holds cpx2euc (r * z) = r * (cpx2euc z)