theorem :: PDIFF_4:24

for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_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,3 ) )