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