theorem Th17: :: NDIFF10:17

for E, F being non trivial RealBanachSpace
for Z being Subset of E
for f being PartFunc of E,F
for a being Point of E
for b being Point of F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & diff (f,a) is invertible holds
ex A being Subset of E ex B being Subset of F ex g being PartFunc of F,E 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 F st y in B holds
diff (f,(g /. y)) is invertible ) & ( for y being Point of F st y in B holds
diff (g,y) = Inv (diff (f,(g /. y))) ) )