theorem Th29: :: NDIFF11:29

for m, n being non zero Element of NAT
for x being Point of (REAL-NS m)
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_differentiable_in x holds
diff (f,x) = Mx2Tran (Jacobian (f,x))