for n being non zero Nat
for x, y being Element of REAL n holds (Infty_dist n) . (x,y) = (Infty_dist n) . (y,x)