for X being RealUnitarySpace
for x being Point of X holds
( ||.x.|| = 0 iff x = 0. X )