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