deffunc H₁( Element of REAL n) -> Element of REAL = partdiff (f,$1,i);
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)
thus for z being Element of REAL n holds g . z = partdiff (f,z,i) by A1; :: thesis: verum