deffunc H₁( Element of REAL n, Element of REAL n) -> Real = |.($1 - $2).|;
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 = |.(x - y).|
let x, y be Element of REAL n; :: thesis: f . x,y = |.(x - y).|
thus f . x,y = |.(x - y).| by A1; :: thesis: verum