for X being RealUnitarySpace
for x being Point of X
for x1 being Point of (RUSp2RNSp X) st x = x1 holds
||.x.|| = ||.x1.|| by Def1;