let F, G be PartFunc of (REAL 2),REAL; ( 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)
; F = G
hence
F = G
by A5, A7, PARTFUN1:5; verum