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