theorem :: PDIFF_1:24

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