theorem :: EUCLID_3:20

for r being Real
for p being Point of (TOP-REAL 2) holds euc2cpx (r * p) = r * (euc2cpx p)