let n be non zero Nat; :: thesis: 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; :: thesis: (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))
proof
now :: thesis: for t being ExtReal st t in rng (abs (x - y)) holds
t <= (abs (x - y)) . (max_diff_index (x,y))
let t be ExtReal; :: thesis: ( t in rng (abs (x - y)) implies t <= (abs (x - y)) . (max_diff_index (x,y)) )
assume t in rng (abs (x - y)) ; :: thesis: t <= (abs (x - y)) . (max_diff_index (x,y))
then ex u being object st
( u in dom (abs (x - y)) & t = (abs (x - y)) . u ) by FUNCT_1:def 3;
hence t <= (abs (x - y)) . (max_diff_index (x,y)) by EUCLID_9:5; :: thesis: verum
end;
then (abs (x - y)) . (max_diff_index (x,y)) is UpperBound of rng (abs (x - y)) by XXREAL_2:def 1;
then sup (rng (abs (x - y))) <= (abs (x - y)) . (max_diff_index (x,y)) by XXREAL_2:def 3;
hence (Infty_dist n) . (x,y) <= (abs (x - y)) . (max_diff_index (x,y)) by Def7; :: thesis: verum
end;
hence (Infty_dist n) . (x,y) = (abs (x - y)) . (max_diff_index (x,y)) by A3, XXREAL_0:1; :: thesis: verum