deffunc H₁( Element of REAL n, Element of REAL n) -> Element of REAL = In ((sup (rng (abs ($1 - $2)))),REAL);
consider f being Function of [:(REAL n),(REAL n):],REAL such that
A1: for x, y being Element of REAL n holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
take f ; :: thesis: for x, y being Element of REAL n holds f . (x,y) = sup (rng (abs (x - y)))
let x, y be Element of REAL n; :: thesis: f . (x,y) = sup (rng (abs (x - y)))
not dom (abs (x - y)) is empty ;
then consider a being object such that
A2: a in dom (abs (x - y)) ;
(abs (x - y)) . a in rng (abs (x - y)) by A2, FUNCT_1:def 3;
then sup (rng (abs (x - y))) in rng (abs (x - y)) by XXREAL_2:def 6;
then ( f . (x,y) = In ((sup (rng (abs (x - y)))),REAL) & sup (rng (abs (x - y))) in REAL ) by A1;
hence f . (x,y) = sup (rng (abs (x - y))) by SUBSET_1:def 8; :: thesis: verum