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 ;
f . a in Ball (b,r2) by ;
then A9: a in f " (Ball (b,r2)) by ;
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 ;
Invf /. s0 = Invf . s0 by ;
then A12: Invf /. s0 in rng Invf by ;
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 ;
hence s in f .: (Ball (a,r1)) by ; :: 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 ;
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 ;
hence s in Ball (b,r2) by ; :: 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 ;
x in f " (Ball (b,r2)) by ;
then ( x in dom f & x in (Ball (a,r1)) /\ (f " (Ball (b,r2))) & s = f . x ) by ;
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 ;
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 ;
then A23: (Ball (a,r1)) /\ (f " (Ball (b,r2))) c= dom f by ;
A24: dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) = (Ball (a,r1)) /\ (f " (Ball (b,r2))) by ;
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
.= f /. (Invf /. y2) by
.= y2 by ;
:: 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 ;
x1 in f " (Ball (b,r2)) by ;
then A31: ( x1 in dom f & f . x1 in Ball (b,r2) ) by FUNCT_1:def 7;
x2 in f " (Ball (b,r2)) by ;
then A33: ( x2 in dom f & f . x2 in Ball (b,r2) ) by FUNCT_1:def 7;
A34: f /. x1 = f . x2 by
.= f /. x2 by ;
A35: ( f /. x1 in Ball (b,r2) & f /. x2 in Ball (b,r2) ) by ;
( x1 in Ball (a,r1) & x2 in Ball (a,r1) ) by ;
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 ;
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 ;
((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y in rng ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") by ;
then A42: ((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y in (Ball (a,r1)) /\ (f " (Ball (b,r2))) by ;
A44: y = (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) . (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by
.= f . (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by
.= f /. (((f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) ") . y) by ;
Invf . y in rng Invf by ;
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 ;
A49: rng Invf = dom (Invf ") by
.= dom (f | ((Ball (a,r1)) /\ (f " (Ball (b,r2))))) by
.= (Ball (a,r1)) /\ (f " (Ball (b,r2))) by ;
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 ; :: thesis: verum