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

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

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

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

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

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

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

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

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

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

then consider r1, r2 being Real such that

A2: ( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= Z & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) ) by Th16;

consider Invf being PartFunc of F,E such that

A3: ( dom Invf = Ball (b,r2) & rng Invf c= Ball (a,r1) & Invf is_continuous_on Ball (b,r2) & Invf . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (Invf /. y) = y ) & Invf is_differentiable_on Ball (b,r2) & Invf `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (Invf,y) = Inv (diff (f,(Invf /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(Invf /. y)) is invertible ) ) by A2;

A4: Ball (a,r1) c= cl_Ball (a,r1) by NDIFF_8:15;

set B = Ball (b,r2);

set A = (Ball (a,r1)) /\ (f " (Ball (b,r2)));

A7: a in Ball (a,r1) by A2, NDIFF_8:13;

f . a in Ball (b,r2) by A1, A2, NDIFF_8:13;

then A9: a in f " (Ball (b,r2)) by A1, FUNCT_1:def 7;

for s being object st s in Ball (b,r2) holds

s in f .: (Ball (a,r1))

A16: f " (Ball (b,r2)) is open by A1, NDIFF_1:45, Th1;

B16: for s being object holds

( s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) iff s in Ball (b,r2) )

.= Ball (b,r2) by B16, TARSKI:2 ;

A22: (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= Ball (a,r1) by XBOOLE_1:17;

then B22: (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= cl_Ball (a,r1) by A4, XBOOLE_1:1;

then A23: (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f by A1, A2, XBOOLE_1:1;

A24: dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) by A1, A2, B22, RELAT_1:62, XBOOLE_1:1;

for y1, y2 being object st y1 in dom Invf & y2 in dom Invf & Invf . y1 = Invf . y2 holds

y1 = y2

B27: for x1, x2 being object st x1 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & x2 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x1 = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x2 holds

x1 = x2

then A37: dom ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") = Ball (b,r2) by A21, FUNCT_1:33;

for x being object st x in dom ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") holds

((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . x = Invf . x

A49: rng Invf = dom (Invf ") by A27, FUNCT_1:33

.= dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) by B27, A47, FUNCT_1:43, FUNCT_1:def 4

.= (Ball (a,r1)) /\ (f " (Ball (b,r2))) by A1, A2, B22, RELAT_1:62, XBOOLE_1:1 ;

take (Ball (a,r1)) /\ (f " (Ball (b,r2))) ; :: thesis: ex B being Subset of F ex g being PartFunc of F,E st

( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & B is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in B & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = B & dom g = B & rng g = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = B & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & g is one-to-one & g = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = 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))) ) )

take Ball (b,r2) ; :: thesis: ex g being PartFunc of F,E st

( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & Ball (b,r2) is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in Ball (b,r2) & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Ball (b,r2) & dom g = Ball (b,r2) & rng g = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = Ball (b,r2) & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & g is one-to-one & g = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = g " & g . b = a & g is_continuous_on Ball (b,r2) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) )

take Invf ; :: thesis: ( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & Ball (b,r2) is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in Ball (b,r2) & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Ball (b,r2) & dom Invf = Ball (b,r2) & rng Invf = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = Ball (b,r2) & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & Invf is one-to-one & Invf = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Invf " & Invf . b = a & Invf is_continuous_on Ball (b,r2) & Invf is_differentiable_on Ball (b,r2) & Invf `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(Invf /. y)) is invertible ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (Invf,y) = Inv (diff (f,(Invf /. y))) ) )

thus ( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & Ball (b,r2) is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in Ball (b,r2) & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Ball (b,r2) & dom Invf = Ball (b,r2) & rng Invf = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = Ball (b,r2) & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & Invf is one-to-one & Invf = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Invf " & Invf . b = a & Invf is_continuous_on Ball (b,r2) & Invf is_differentiable_on Ball (b,r2) & Invf `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(Invf /. y)) is invertible ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (Invf,y) = Inv (diff (f,(Invf /. y))) ) ) by A1, A2, A3, A7, A9, A16, B16, A21, B22, A36, A47, A49, FUNCT_1:43, NDIFF_8:13, RELAT_1:62, TARSKI:2, XBOOLE_0:def 4, 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

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

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

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

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

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

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

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

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

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

then consider r1, r2 being Real such that

A2: ( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= Z & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) ) by Th16;

consider Invf being PartFunc of F,E such that

A3: ( dom Invf = Ball (b,r2) & rng Invf c= Ball (a,r1) & Invf is_continuous_on Ball (b,r2) & Invf . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (Invf /. y) = y ) & Invf is_differentiable_on Ball (b,r2) & Invf `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (Invf,y) = Inv (diff (f,(Invf /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(Invf /. y)) is invertible ) ) by A2;

A4: Ball (a,r1) c= cl_Ball (a,r1) by NDIFF_8:15;

set B = Ball (b,r2);

set A = (Ball (a,r1)) /\ (f " (Ball (b,r2)));

A7: a in Ball (a,r1) by A2, NDIFF_8:13;

f . a in Ball (b,r2) by A1, A2, NDIFF_8:13;

then A9: a in f " (Ball (b,r2)) by A1, FUNCT_1:def 7;

for s being object st s in Ball (b,r2) holds

s in f .: (Ball (a,r1))

proof

then A14:
Ball (b,r2) c= f .: (Ball (a,r1))
by TARSKI:def 3;
let s be object ; :: thesis: ( s in Ball (b,r2) implies s in f .: (Ball (a,r1)) )

assume A10: s in Ball (b,r2) ; :: thesis: s in f .: (Ball (a,r1))

then reconsider s0 = s as Point of F ;

A11: f /. (Invf /. s0) = s0 by A3, A10;

Invf /. s0 = Invf . s0 by A3, A10, PARTFUN1:def 6;

then A12: Invf /. s0 in rng Invf by A3, A10, FUNCT_1:3;

then Invf /. s0 in Ball (a,r1) by A3;

then B12: Invf /. s0 in cl_Ball (a,r1) by A4;

then f /. (Invf /. s0) = f . (Invf /. s0) by A1, A2, PARTFUN1:def 6;

hence s in f .: (Ball (a,r1)) by A1, A2, A3, A11, A12, B12, FUNCT_1:def 6; :: thesis: verum

end;assume A10: s in Ball (b,r2) ; :: thesis: s in f .: (Ball (a,r1))

then reconsider s0 = s as Point of F ;

A11: f /. (Invf /. s0) = s0 by A3, A10;

Invf /. s0 = Invf . s0 by A3, A10, PARTFUN1:def 6;

then A12: Invf /. s0 in rng Invf by A3, A10, FUNCT_1:3;

then Invf /. s0 in Ball (a,r1) by A3;

then B12: Invf /. s0 in cl_Ball (a,r1) by A4;

then f /. (Invf /. s0) = f . (Invf /. s0) by A1, A2, PARTFUN1:def 6;

hence s in f .: (Ball (a,r1)) by A1, A2, A3, A11, A12, B12, FUNCT_1:def 6; :: thesis: verum

A16: f " (Ball (b,r2)) is open by A1, NDIFF_1:45, Th1;

B16: for s being object holds

( s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) iff s in Ball (b,r2) )

proof

A21: rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) =
f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2))))
by RELAT_1:115
let s be object ; :: thesis: ( s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) iff s in Ball (b,r2) )

then consider x being object such that

A19: ( x in dom f & x in Ball (a,r1) & s = f . x ) by A14, FUNCT_1:def 6;

x in f " (Ball (b,r2)) by A18, A19, FUNCT_1:def 7;

then ( x in dom f & x in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & s = f . x ) by A19, XBOOLE_0:def 4;

hence s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) by FUNCT_1:def 6; :: thesis: verum

end;hereby :: thesis: ( s in Ball (b,r2) implies s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) )

assume A18:
s in Ball (b,r2)
; :: thesis: s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2))))assume
s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2))))
; :: thesis: s in Ball (b,r2)

then consider x being object such that

A17: ( x in dom f & x in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & s = f . x ) by FUNCT_1:def 6;

x in f " (Ball (b,r2)) by A17, XBOOLE_0:def 4;

hence s in Ball (b,r2) by A17, FUNCT_1:def 7; :: thesis: verum

end;then consider x being object such that

A17: ( x in dom f & x in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & s = f . x ) by FUNCT_1:def 6;

x in f " (Ball (b,r2)) by A17, XBOOLE_0:def 4;

hence s in Ball (b,r2) by A17, FUNCT_1:def 7; :: thesis: verum

then consider x being object such that

A19: ( x in dom f & x in Ball (a,r1) & s = f . x ) by A14, FUNCT_1:def 6;

x in f " (Ball (b,r2)) by A18, A19, FUNCT_1:def 7;

then ( x in dom f & x in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & s = f . x ) by A19, XBOOLE_0:def 4;

hence s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) by FUNCT_1:def 6; :: thesis: verum

.= Ball (b,r2) by B16, TARSKI:2 ;

A22: (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= Ball (a,r1) by XBOOLE_1:17;

then B22: (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= cl_Ball (a,r1) by A4, XBOOLE_1:1;

then A23: (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f by A1, A2, XBOOLE_1:1;

A24: dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) by A1, A2, B22, RELAT_1:62, XBOOLE_1:1;

for y1, y2 being object st y1 in dom Invf & y2 in dom Invf & Invf . y1 = Invf . y2 holds

y1 = y2

proof

then A27:
Invf is one-to-one
by FUNCT_1:def 4;
let y1, y2 be object ; :: thesis: ( y1 in dom Invf & y2 in dom Invf & Invf . y1 = Invf . y2 implies y1 = y2 )

assume A25: ( y1 in dom Invf & y2 in dom Invf & Invf . y1 = Invf . y2 ) ; :: thesis: y1 = y2

hence y1 = f /. (Invf /. y1) by A3

.= f /. (Invf . y2) by A25, PARTFUN1:def 6

.= f /. (Invf /. y2) by A25, PARTFUN1:def 6

.= y2 by A3, A25 ;

:: thesis: verum

end;assume A25: ( y1 in dom Invf & y2 in dom Invf & Invf . y1 = Invf . y2 ) ; :: thesis: y1 = y2

hence y1 = f /. (Invf /. y1) by A3

.= f /. (Invf . y2) by A25, PARTFUN1:def 6

.= f /. (Invf /. y2) by A25, PARTFUN1:def 6

.= y2 by A3, A25 ;

:: thesis: verum

B27: for x1, x2 being object st x1 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & x2 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x1 = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x2 holds

x1 = x2

proof

then A36:
f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & x2 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x1 = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x2 implies x1 = x2 )

assume A28: ( x1 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & x2 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x1 = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x2 ) ; :: thesis: x1 = x2

then A29: f . x1 = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x2 by FUNCT_1:47

.= f . x2 by A28, FUNCT_1:47 ;

x1 in f " (Ball (b,r2)) by A28, XBOOLE_0:def 4;

then A31: ( x1 in dom f & f . x1 in Ball (b,r2) ) by FUNCT_1:def 7;

x2 in f " (Ball (b,r2)) by A28, XBOOLE_0:def 4;

then A33: ( x2 in dom f & f . x2 in Ball (b,r2) ) by FUNCT_1:def 7;

A34: f /. x1 = f . x2 by A29, A31, PARTFUN1:def 6

.= f /. x2 by A33, PARTFUN1:def 6 ;

A35: ( f /. x1 in Ball (b,r2) & f /. x2 in Ball (b,r2) ) by A31, A33, PARTFUN1:def 6;

( x1 in Ball (a,r1) & x2 in Ball (a,r1) ) by A28, XBOOLE_0:def 4;

hence x1 = x2 by A2, A34, A35; :: thesis: verum

end;assume A28: ( x1 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & x2 in dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) & (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x1 = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x2 ) ; :: thesis: x1 = x2

then A29: f . x1 = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . x2 by FUNCT_1:47

.= f . x2 by A28, FUNCT_1:47 ;

x1 in f " (Ball (b,r2)) by A28, XBOOLE_0:def 4;

then A31: ( x1 in dom f & f . x1 in Ball (b,r2) ) by FUNCT_1:def 7;

x2 in f " (Ball (b,r2)) by A28, XBOOLE_0:def 4;

then A33: ( x2 in dom f & f . x2 in Ball (b,r2) ) by FUNCT_1:def 7;

A34: f /. x1 = f . x2 by A29, A31, PARTFUN1:def 6

.= f /. x2 by A33, PARTFUN1:def 6 ;

A35: ( f /. x1 in Ball (b,r2) & f /. x2 in Ball (b,r2) ) by A31, A33, PARTFUN1:def 6;

( x1 in Ball (a,r1) & x2 in Ball (a,r1) ) by A28, XBOOLE_0:def 4;

hence x1 = x2 by A2, A34, A35; :: thesis: verum

then A37: dom ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") = Ball (b,r2) by A21, FUNCT_1:33;

for x being object st x in dom ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") holds

((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . x = Invf . x

proof

then A47:
(f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " = Invf
by A3, A37, FUNCT_1:2;
let x be object ; :: thesis: ( x in dom ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") implies ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . x = Invf . x )

assume A39: x in dom ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") ; :: thesis: ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . x = Invf . x

then reconsider y = x as Point of F by A37;

A41: y = f /. (Invf /. y) by A3, A37, A39

.= f /. (Invf . y) by A3, A37, A39, PARTFUN1:def 6 ;

((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y in rng ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") by A39, FUNCT_1:3;

then A42: ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y in (Ball (a,r1)) /\ (f " (Ball (b,r2))) by A24, A36, FUNCT_1:33;

A44: y = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by A21, A36, A37, A39, FUNCT_1:35

.= f . (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by A42, FUNCT_1:49

.= f /. (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by A23, A42, PARTFUN1:def 6 ;

Invf . y in rng Invf by A3, A37, A39, FUNCT_1:3;

hence ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . x = Invf . x by A2, A3, A22, A37, A39, A41, A42, A44; :: thesis: verum

end;assume A39: x in dom ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") ; :: thesis: ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . x = Invf . x

then reconsider y = x as Point of F by A37;

A41: y = f /. (Invf /. y) by A3, A37, A39

.= f /. (Invf . y) by A3, A37, A39, PARTFUN1:def 6 ;

((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y in rng ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") by A39, FUNCT_1:3;

then A42: ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y in (Ball (a,r1)) /\ (f " (Ball (b,r2))) by A24, A36, FUNCT_1:33;

A44: y = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by A21, A36, A37, A39, FUNCT_1:35

.= f . (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by A42, FUNCT_1:49

.= f /. (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by A23, A42, PARTFUN1:def 6 ;

Invf . y in rng Invf by A3, A37, A39, FUNCT_1:3;

hence ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . x = Invf . x by A2, A3, A22, A37, A39, A41, A42, A44; :: thesis: verum

A49: rng Invf = dom (Invf ") by A27, FUNCT_1:33

.= dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) by B27, A47, FUNCT_1:43, FUNCT_1:def 4

.= (Ball (a,r1)) /\ (f " (Ball (b,r2))) by A1, A2, B22, RELAT_1:62, XBOOLE_1:1 ;

take (Ball (a,r1)) /\ (f " (Ball (b,r2))) ; :: thesis: ex B being Subset of F ex g being PartFunc of F,E st

( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & B is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in B & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = B & dom g = B & rng g = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = B & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & g is one-to-one & g = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = 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))) ) )

take Ball (b,r2) ; :: thesis: ex g being PartFunc of F,E st

( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & Ball (b,r2) is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in Ball (b,r2) & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Ball (b,r2) & dom g = Ball (b,r2) & rng g = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = Ball (b,r2) & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & g is one-to-one & g = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = g " & g . b = a & g is_continuous_on Ball (b,r2) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) )

take Invf ; :: thesis: ( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & Ball (b,r2) is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in Ball (b,r2) & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Ball (b,r2) & dom Invf = Ball (b,r2) & rng Invf = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = Ball (b,r2) & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & Invf is one-to-one & Invf = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Invf " & Invf . b = a & Invf is_continuous_on Ball (b,r2) & Invf is_differentiable_on Ball (b,r2) & Invf `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(Invf /. y)) is invertible ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (Invf,y) = Inv (diff (f,(Invf /. y))) ) )

thus ( (Ball (a,r1)) /\ (f " (Ball (b,r2))) is open & Ball (b,r2) is open & (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f & a in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & b in Ball (b,r2) & f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Ball (b,r2) & dom Invf = Ball (b,r2) & rng Invf = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) & rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = Ball (b,r2) & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one & Invf is one-to-one & Invf = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " & f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) = Invf " & Invf . b = a & Invf is_continuous_on Ball (b,r2) & Invf is_differentiable_on Ball (b,r2) & Invf `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(Invf /. y)) is invertible ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (Invf,y) = Inv (diff (f,(Invf /. y))) ) ) by A1, A2, A3, A7, A9, A16, B16, A21, B22, A36, A47, A49, FUNCT_1:43, NDIFF_8:13, RELAT_1:62, TARSKI:2, XBOOLE_0:def 4, XBOOLE_1:1; :: thesis: verum