deffunc H_{1}( Real, Real) -> Element of REAL = In (|.($1 - $2).|,REAL);

consider F being Function of [:REAL,REAL:],REAL such that

A1: for x, y being Element of REAL holds F . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

take F ; :: thesis: for x, y being Real holds F . (x,y) = |.(x - y).|

let x, y be Real; :: thesis: F . (x,y) = |.(x - y).|

reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;

F . (x,y) = H_{1}(x,y)
by A1;

hence F . (x,y) = |.(x - y).| ; :: thesis: verum

consider F being Function of [:REAL,REAL:],REAL such that

A1: for x, y being Element of REAL holds F . (x,y) = H

take F ; :: thesis: for x, y being Real holds F . (x,y) = |.(x - y).|

let x, y be Real; :: thesis: F . (x,y) = |.(x - y).|

reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;

F . (x,y) = H

hence F . (x,y) = |.(x - y).| ; :: thesis: verum