deffunc H₁( Element of REAL n) -> Element of REAL = $1 . i;
thus ex f being Function of (REAL n),REAL st
for x being Element of REAL n holds f . x = H₁(x) from FUNCT_2:sch 4(); :: thesis: verum