theorem :: PDIFF_2:15

for Z being Subset of (REAL 2)
for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`1_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,1 ) )