for n being Nat
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
for i being Nat st i in Seg n holds
|.(y . i).| <= ||.x.||