theorem :: NDIFF11:34

for m being non zero Element of NAT
for Z being Subset of (REAL-NS m)
for f being PartFunc of (REAL-NS m),(REAL-NS m)
for a, b being Point of (REAL-NS m) st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & Det (Jacobian (f,a)) <> 0. F_Real holds
ex A, B being Subset of (REAL-NS m) ex g being PartFunc of (REAL-NS m),(REAL-NS m) st
( A is open & B is open & A c= dom f & a in A & b in B & f .: A = B & dom g = B & rng g = A & dom (f | A) = A & rng (f | A) = B & f | A is one-to-one & g is one-to-one & g = (f | A) " & f | A = g " & g . b = a & g is_continuous_on B & g is_differentiable_on B & g `| B is_continuous_on B & ( for y being Point of (REAL-NS m) st y in B holds
diff (f,(g /. y)) is invertible ) & ( for y being Point of (REAL-NS m) st y in B holds
diff (g,y) = Inv (diff (f,(g /. y))) ) )