theorem :: PDIFF_7:23

for m being non zero Nat
for i being Nat
for h being PartFunc of (REAL m),REAL
for y being Element of REAL m st h is_differentiable_in y & 1 <= i & i <= m holds
( h is_partial_differentiable_in y,i & partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) & partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) )