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