let n be 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))
let x, y be Element of REAL n; (Infty_dist n) . (x,y) = (abs (x - y)) . (max_diff_index (x,y))
max_diff_index (x,y) in dom x
by EUCLID_9:4;
then A1:
max_diff_index (x,y) in Seg n
by FINSEQ_2:124;
dom (abs (x - y)) = Seg n
by FINSEQ_2:124;
then A2:
(abs (x - y)) . (max_diff_index (x,y)) in rng (abs (x - y))
by A1, FUNCT_1:def 3;
sup (rng (abs (x - y))) is UpperBound of rng (abs (x - y))
by XXREAL_2:def 3;
then
(abs (x - y)) . (max_diff_index (x,y)) <= sup (rng (abs (x - y)))
by A2, XXREAL_2:def 1;
then A3:
(abs (x - y)) . (max_diff_index (x,y)) <= (Infty_dist n) . (x,y)
by Def7;
(Infty_dist n) . (x,y) <= (abs (x - y)) . (max_diff_index (x,y))
hence
(Infty_dist n) . (x,y) = (abs (x - y)) . (max_diff_index (x,y))
by A3, XXREAL_0:1; verum