for n being Nat
for x being Element of REAL (n + 1)
for y being Element of REAL n
for w being Element of REAL st y = x | n & w = x . (n + 1) holds
|.x.| <= |.y.| + |.w.|