for m, n being non zero Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>