for r being Real
for p being Point of (TOP-REAL 2) holds r * p = |[(r * (p `1)),(r * (p `2))]|