for a being Real
for X being RealUnitarySpace
for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||