for i being Nat
for m, n being non zero Nat
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)