deffunc H₁( Real) -> Element of REAL = abs $1;
consider f being Function of REAL,REAL such that
A1: for r being Real holds f . r = H₁(r) from FUNCT_2:sch 4();
take f ; :: thesis: for r being real number holds f . r = abs r
let r be real number ; :: thesis: f . r = abs r
r is Real by XREAL_0:def 1;
hence f . r = abs r by A1; :: thesis: verum