deffunc H_{1}( Element of REAL n) -> Element of REAL = In (|.$1.|,REAL);

consider f being Function of (REAL n),REAL such that

A1: for x being Element of REAL n holds f . x = H_{1}(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.|

f . x = H_{1}(x)
by A1;

hence f . x = |.x.| ; :: thesis: verum

consider f being Function of (REAL n),REAL such that

A1: for x being Element of REAL n holds f . x = H

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.|

f . x = H

hence f . x = |.x.| ; :: thesis: verum