theorem :: PDIFF_5:52

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