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