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