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