for n being non zero Nat
for x, y being Element of REAL n holds
( { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } is real-membered & { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } = rng (abs (x - y)) )