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