deffunc H1( Element of REAL n, Element of REAL n) -> Element of REAL = In (|.($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) = H1(x,y)
from BINOP_1:sch 4();
take
f
; for x, y being Element of REAL n holds f . (x,y) = |.(x - y).|
let x, y be Element of REAL n; f . (x,y) = |.(x - y).|
f . (x,y) = H1(x,y)
by A1;
hence
f . (x,y) = |.(x - y).|
; verum