theorem :: PDIFF_4:23

for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) )