for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 + x2).| <= |.x1.| + |.x2.|