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

now :: thesis: for z being Element of REAL 2 st z in dom F holds
F . z = G . z

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 = hpartdiff22 (f,z) by A5, A6;
hence F . z = G . z by A5, A8, A9; :: thesis: verum

end;

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