deffunc H₁( Element of REAL n) -> Element of REAL = In (($1 . i),REAL);
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 . i
let x be Element of REAL n; :: thesis: f . x = x . i
f . x = H₁(x) by A1;
hence f . x = x . i ; :: thesis: verum