theorem Th31: :: NDIFF11:31

for m being non zero Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS m)
for x being Point of (REAL-NS m) st f is_differentiable_in x holds
( diff (f,x) is invertible iff Det (Jacobian (f,x)) <> 0. F_Real )