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

proof

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;

then A14: Ball (b,r2) c= f .: (Ball (a,r1)) by TARSKI:def 3;
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

let s be object ; :: thesis: ( s in f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) iff s in Ball (b,r2) )

hereby :: thesis: ( s in Ball (b,r2) implies 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;

assume A18: s in Ball (b,r2) ; :: thesis: s in f .: ((Ball (a,r1)) /\ (f " (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;

A21: rng (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = f .: ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) by RELAT_1:115
.= 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

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;

then A27: Invf is one-to-one by FUNCT_1:def 4;
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

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;

then A36: f | ((Ball (a,r1)) /\ (f " (Ball (b,r2)))) is one-to-one by FUNCT_1:def 4;
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

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;

then A47: (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) " = Invf by A3, A37, FUNCT_1:2;
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