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