let F, G be PartFunc of (REAL 2),REAL ; :: thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = partdiff f,z,1 ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds
G . z = partdiff f,z,1 ) implies F = G )
assume that
A5: dom F = Z and
A6: for z being Element of REAL 2 st z in Z holds
F . z = partdiff f,z,1 and
A7: dom G = Z and
A8: for z being Element of REAL 2 st z in Z holds
G . z = partdiff f,z,1 ; :: thesis: F = G

now

let z be Element of REAL 2; :: thesis: ( z in dom F implies F . z = G . z )
assume A9: z in dom F ; :: thesis: F . z = G . z
then F . z = partdiff f,z,1 by A5, A6;
hence F . z = G . z by A5, A8, A9; :: thesis: verum

end;

hence F = G by A5, A7, PARTFUN1:34; :: thesis: verum