theorem Th18: :: NDIFF10:18

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
for r1 being Real st 0 < r1 holds
ex r2 being Real st
( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )