let E, F be non trivial RealBanachSpace; :: thesis: 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)) )

let Z be Subset of E; :: thesis: 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)) )

let f be PartFunc of E,F; :: thesis: 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)) )

let a be Point of E; :: thesis: 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)) )

let b be Point of F; :: thesis: ( 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 implies for r1 being Real st 0 < r1 holds

ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) ) )

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 & diff (f,a) is invertible ) ; :: thesis: for r1 being Real st 0 < r1 holds

ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )

then consider A being Subset of E, B being Subset of F, g being PartFunc of F,E such that

A2: ( 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))) ) ) by Th17;

let r1 be Real; :: thesis: ( 0 < r1 implies ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) ) )

assume A3: 0 < r1 ; :: thesis: ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )

A5: g " (Ball (a,r1)) = (f | A) .: (Ball (a,r1)) by A2, FUNCT_1:85;

A6: (f | A) .: (Ball (a,r1)) c= f .: (Ball (a,r1)) by RELAT_1:128;

( a in dom (f | A) & a in Ball (a,r1) & f . a = (f | A) . a ) by A2, A3, FUNCT_1:49, NDIFF_8:13;

then f . a in (f | A) .: (Ball (a,r1)) by FUNCT_1:def 6;

then consider r2 being Real such that

A7: ( 0 < r2 & Ball (b,r2) c= (f | A) .: (Ball (a,r1)) ) by A1, A2, A5, Th1, NDIFF_8:20;

thus ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) ) by A6, A7, XBOOLE_1:1; :: thesis: verum

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)) )

let Z be Subset of E; :: thesis: 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)) )

let f be PartFunc of E,F; :: thesis: 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)) )

let a be Point of E; :: thesis: 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)) )

let b be Point of F; :: thesis: ( 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 implies for r1 being Real st 0 < r1 holds

ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) ) )

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 & diff (f,a) is invertible ) ; :: thesis: for r1 being Real st 0 < r1 holds

ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )

then consider A being Subset of E, B being Subset of F, g being PartFunc of F,E such that

A2: ( 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))) ) ) by Th17;

let r1 be Real; :: thesis: ( 0 < r1 implies ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) ) )

assume A3: 0 < r1 ; :: thesis: ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )

A5: g " (Ball (a,r1)) = (f | A) .: (Ball (a,r1)) by A2, FUNCT_1:85;

A6: (f | A) .: (Ball (a,r1)) c= f .: (Ball (a,r1)) by RELAT_1:128;

( a in dom (f | A) & a in Ball (a,r1) & f . a = (f | A) . a ) by A2, A3, FUNCT_1:49, NDIFF_8:13;

then f . a in (f | A) .: (Ball (a,r1)) by FUNCT_1:def 6;

then consider r2 being Real such that

A7: ( 0 < r2 & Ball (b,r2) c= (f | A) .: (Ball (a,r1)) ) by A1, A2, A5, Th1, NDIFF_8:20;

thus ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) ) by A6, A7, XBOOLE_1:1; :: thesis: verum