for n being non zero Nat
for i being Nat
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )