theorem :: PDIFF_4:22

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