for a being Complex
for X being ComplexUnitarySpace
for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||