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