let d1, d2 be Function of [:(REAL n),(REAL n):],REAL; :: thesis: ( ( for x, y being Element of REAL n holds d1 . (x,y) = sup (rng (abs (x - y))) ) & ( for x, y being Element of REAL n holds d2 . (x,y) = sup (rng (abs (x - y))) ) implies d1 = d2 )
assume that
A3: for x, y being Element of REAL n holds d1 . (x,y) = sup (rng (abs (x - y))) and
A4: for x, y being Element of REAL n holds d2 . (x,y) = sup (rng (abs (x - y))) ; :: thesis: d1 = d2

now :: thesis: for x, y being set st x in REAL n & y in REAL n holds
d1 . (x,y) = d2 . (x,y)

let x, y be set ; :: thesis: ( x in REAL n & y in REAL n implies d1 . (x,y) = d2 . (x,y) )
assume that
A5: x in REAL n and
A6: y in REAL n ; :: thesis: d1 . (x,y) = d2 . (x,y)
reconsider x1 = x, y1 = y as Element of REAL n by A5, A6;
d1 . (x1,y1) = sup (rng (abs (x1 - y1))) by A3
.= d2 . (x1,y1) by A4 ;
hence d1 . (x,y) = d2 . (x,y) ; :: thesis: verum

end;

hence d1 = d2 by BINOP_1:def 21; :: thesis: verum