theorem :: PDIFF_2:16

for Z being Subset of (REAL 2)
for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`2_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) )