deffunc H₁( Element of REAL n) -> Element of REAL = |.$1.|;
consider f being Function of (REAL n),REAL such that
A1: for x being Element of REAL n holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for x being Element of REAL n holds f . x = |.x.|
let x be Element of REAL n; :: thesis: f . x = |.x.|
thus f . x = |.x.| by A1; :: thesis: verum