theorem :: PDIFF_5:54

for u0 being Element of REAL 3
for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`13_in u0 & f2 is_hpartial_differentiable`13_in u0 holds
( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in u0,3 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),u0,3) = (hpartdiff13 (f1,u0)) - (hpartdiff13 (f2,u0)) )