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
A6: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = partdiff f,z,1 ) ) and
A7: ( dom G = Z & ( 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 A8: z in dom F ; :: thesis: F . z = G . z
then F . z = partdiff f,z,1 by A6;
hence F . z = G . z by A6, A7, A8; :: thesis: verum

end;

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