deffunc H₁( Element of REAL , Element of REAL ) -> Element of REAL = abs ($1 - $2);
consider F being Function of [:REAL,REAL:],REAL such that
A1: for x, y being Element of REAL holds F . (x,y) = H₁(x,y) from BINOP_1:sch 4();
take F ; :: thesis: for x, y being Element of REAL holds F . (x,y) = abs (x - y)
let x, y be Element of REAL ; :: thesis: F . (x,y) = abs (x - y)
thus F . (x,y) = abs (x - y) by A1; :: thesis: verum