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

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:113; :: thesis: verum