for n being Nat
for x1, x2 being Element of REAL n holds
( |.(x1 - x2).| = 0 iff x1 = x2 )