deffunc H1( 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) = H1(x,y)
from BINOP_1:sch 4();
take
F
; for x, y being Real holds F . (x,y) = |.(x - y).|
let x, y be Real; F . (x,y) = |.(x - y).|
reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;
F . (x,y) = H1(x,y)
by A1;
hence
F . (x,y) = |.(x - y).|
; verum