let m be non zero Element of NAT ; :: thesis: 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))) ) )
let Z be Subset of (REAL-NS m); :: thesis: 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))) ) )
let f be PartFunc of (REAL-NS m),(REAL-NS m); :: thesis: 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))) ) )
let a, b be Point of (REAL-NS m); :: thesis: ( 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 implies 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))) ) ) )
assume A1: ( 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 ) ; :: thesis: 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))) ) )
then f is_differentiable_in a ;
then diff (f,a) is invertible by A1, Th31;
hence 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))) ) ) by A1, NDIFF10:17; :: thesis: verum