let F, G be Function of (REAL n),REAL; :: thesis: ( ( for z being Element of REAL n holds F . z = partdiff (f,z,i) ) & ( for z being Element of REAL n holds G . z = partdiff (f,z,i) ) implies F = G )
assume that
A2: for z being Element of REAL n holds F . z = partdiff (f,z,i) and
A3: for z being Element of REAL n holds G . z = partdiff (f,z,i) ; :: thesis: F = G

now :: thesis: for z being Element of REAL n holds F . z = G . z

let z be Element of REAL n; :: thesis: F . z = G . z
F . z = partdiff (f,z,i) by A2;
hence F . z = G . z by A3; :: thesis: verum

end;

hence F = G by FUNCT_2:63; :: thesis: verum