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 r1, r2 being Real st
( 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 ) )

let D 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 D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( 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 ) )

let f be PartFunc of E,F; :: thesis: for a being Point of E
for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( 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 ) )

let a be Point of E; :: thesis: for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( 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 ) )

let b be Point of F; :: thesis: ( D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible implies ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( 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 ) ) )

assume that
A1: D is open and
A2: dom f = D and
A3: f is_differentiable_on D and
A4: f `| D is_continuous_on D and
A5: a in D and
A6: f . a = b and
A7: diff (f,a) is invertible ; :: thesis: ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( 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 ) )

reconsider Z = [:D, the carrier of F:] as Subset of [:E,F:] by ZFMISC_1:96;
A9: Z is open by ;
defpred S1[ object , object ] means ex x being Point of E ex y being Point of F st
( \$1 = [x,y] & \$2 = (f /. x) - y );
A10: for z being object st z in Z holds
ex y being object st
( y in the carrier of F & S1[z,y] )
proof
let z be object ; :: thesis: ( z in Z implies ex y being object st
( y in the carrier of F & S1[z,y] ) )

assume z in Z ; :: thesis: ex y being object st
( y in the carrier of F & S1[z,y] )

then consider x being Point of E, y being Point of F such that
A11: z = [x,y] by PRVECT_3:18;
take w = (f /. x) - y; :: thesis: ( w in the carrier of F & S1[z,w] )
thus ( w in the carrier of F & S1[z,w] ) by A11; :: thesis: verum
end;
consider f1 being Function of Z, the carrier of F such that
A12: for x being object st x in Z holds
S1[x,f1 . x] from A13: dom f1 = Z by FUNCT_2:def 1;
then ( dom f1 c= the carrier of [:E,F:] & rng f1 c= the carrier of F ) ;
then reconsider f1 = f1 as PartFunc of [:E,F:],F by RELSET_1:4;
A14: for s being Point of E
for t being Point of F st s in D holds
f1 . (s,t) = (f /. s) - t
proof
let s be Point of E; :: thesis: for t being Point of F st s in D holds
f1 . (s,t) = (f /. s) - t

let t be Point of F; :: thesis: ( s in D implies f1 . (s,t) = (f /. s) - t )
assume s in D ; :: thesis: f1 . (s,t) = (f /. s) - t
then consider x being Point of E, y being Point of F such that
A15: ( [s,t] = [x,y] & f1 . [s,t] = (f /. x) - y ) by ;
( s = x & t = y ) by ;
hence f1 . (s,t) = (f /. s) - t by A15; :: thesis: verum
end;
reconsider z = [a,b] as Point of [:E,F:] ;
A16: f1 is_differentiable_on Z by A1, A2, A3, A4, A5, A13, A14, Th15;
A17: f1 `| Z is_continuous_on Z by A1, A2, A3, A4, A5, A13, A14, Th15;
f . a = f /. a by ;
then (f /. a) - b = 0. F by ;
then A19: f1 . (a,b) = 0. F by ;
ex J being Point of st
( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,a) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A5, A13, A14, Th15;
then consider r1, r2 being Real such that
A21: ( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] c= Z & ( for x being Point of F st x in Ball (b,r2) holds
ex y being Point of E st
( y in Ball (a,r1) & f1 . (y,x) = 0. F ) ) & ( for x being Point of F st x in Ball (b,r2) holds
for y1, y2 being Point of E st y1 in Ball (a,r1) & y2 in Ball (a,r1) & f1 . (y1,x) = 0. F & f1 . (y2,x) = 0. F holds
y1 = y2 ) & 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 x being Point of F st x in Ball (b,r2) holds
f1 . ((g . x),x) = 0. F ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F
for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds
diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & ( for y being Point of F
for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds
partdiff`1 (f1,z) 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
f1 . ((g1 . y),y) = 0. F ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds
f1 . ((g2 . y),y) = 0. F ) holds
g1 = g2 ) ) by ;
take r1 ; :: thesis: ex r2 being Real st
( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( 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 ) )

take r2 ; :: thesis: ( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( 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 ) )

thus ( 0 < r1 & 0 < r2 ) by A21; :: thesis: ( cl_Ball (a,r1) c= D & ( 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 ) )

for s being object st s in cl_Ball (a,r1) holds
s in D
proof
let s be object ; :: thesis: ( s in cl_Ball (a,r1) implies s in D )
assume A23: s in cl_Ball (a,r1) ; :: thesis: s in D
b in Ball (b,r2) by ;
then [s,b] in [:(cl_Ball (a,r1)),(Ball (b,r2)):] by ;
hence s in D by ; :: thesis: verum
end;
hence A24: cl_Ball (a,r1) c= D by TARSKI:def 3; :: thesis: ( ( 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 ) )

Ball (a,r1) c= cl_Ball (a,r1) by NDIFF_8:15;
then A25: Ball (a,r1) c= D by ;
thus 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 ) :: thesis: ( ( 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 ) )
proof
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies ex x being Point of E st
( x in Ball (a,r1) & f /. x = y ) )

assume y in Ball (b,r2) ; :: thesis: ex x being Point of E st
( x in Ball (a,r1) & f /. x = y )

then consider x being Point of E such that
A26: ( x in Ball (a,r1) & f1 . (x,y) = 0. F ) by A21;
take x ; :: thesis: ( x in Ball (a,r1) & f /. x = y )
(f /. x) - y = 0. F by ;
hence ( x in Ball (a,r1) & f /. x = y ) by ; :: thesis: verum
end;
thus 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 :: thesis: ( 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 ) )
proof
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies 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 )

assume A27: y in Ball (b,r2) ; :: thesis: 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

let x1, x2 be Point of E; :: thesis: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y implies x1 = x2 )
assume A28: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y ) ; :: thesis: x1 = x2
then ( (f /. x1) - y = 0. F & (f /. x2) - y = 0. F ) by RLVECT_1:15;
then ( f1 . (x1,y) = 0. F & f1 . (x2,y) = 0. F ) by ;
hence x1 = x2 by ; :: thesis: verum
end;
thus 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 ) ) :: thesis: 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
proof
consider g being PartFunc of F,E such that
A29: ( 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
f1 . ((g . y),y) = 0. F ) & ( for y being Point of F
for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds
diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F
for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds
diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & ( for y being Point of F
for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds
partdiff`1 (f1,z) is invertible ) ) by A21;
take g ; :: thesis: ( 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 ) )

thus ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) ) by A29; :: thesis: ( 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 ) )

thus ( g is_continuous_on Ball (b,r2) & g . b = a ) by A29; :: thesis: ( ( 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 ) )

thus for y being Point of F st y in Ball (b,r2) holds
f /. (g /. y) = y :: thesis: ( 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 ) )
proof
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies f /. (g /. y) = y )
assume A30: y in Ball (b,r2) ; :: thesis: f /. (g /. y) = y
then A31: f1 . ((g . y),y) = 0. F by A29;
g . y in rng g by ;
then g . y in Ball (a,r1) by A29;
then A32: (f /. (g . y)) - y = 0. F by ;
g . y = g /. y by ;
hence f /. (g /. y) = y by ; :: thesis: verum
end;
thus ( g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) ) by A29; :: thesis: ( ( 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 ) )

thus for y being Point of F st y in Ball (b,r2) holds
diff (g,y) = Inv (diff (f,(g /. y))) :: thesis: for y being Point of F st y in Ball (b,r2) holds
diff (f,(g /. y)) is invertible
proof
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies diff (g,y) = Inv (diff (f,(g /. y))) )
assume A33: y in Ball (b,r2) ; :: thesis: diff (g,y) = Inv (diff (f,(g /. y)))
[(g /. y),y] is set ;
then reconsider z = [(g . y),y] as Point of [:E,F:] by ;
g . y in rng g by ;
then A34: g . y in Ball (a,r1) by A29;
g . y = g /. y by ;
then consider J being Point of such that
A35: ( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,(g /. y)) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A13, A14, A25, A34, Th15;
thus diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) by
.= (- (Inv (diff (f,(g /. y))))) * (- J) by
.= (Inv (diff (f,(g /. y)))) * J by LOPBAN13:27
.= (modetrans ((Inv (diff (f,(g /. y)))),F,E)) * (id the carrier of F) by
.= modetrans ((Inv (diff (f,(g /. y)))),F,E) by FUNCT_2:17
.= Inv (diff (f,(g /. y))) by LOPBAN_1:def 11 ; :: thesis: verum
end;
thus for y being Point of F st y in Ball (b,r2) holds
diff (f,(g /. y)) is invertible :: thesis: verum
proof
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies diff (f,(g /. y)) is invertible )
assume A36: y in Ball (b,r2) ; :: thesis: diff (f,(g /. y)) is invertible
[(g /. y),y] is set ;
then reconsider z = [(g . y),y] as Point of [:E,F:] by ;
g . y in rng g by ;
then A38: g . y in Ball (a,r1) by A29;
g . y = g /. y by ;
then ex J being Point of st
( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,(g /. y)) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A13, A14, A25, A38, Th15;
hence diff (f,(g /. y)) is invertible by ; :: thesis: verum
end;
end;
thus 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 :: thesis: verum
proof
let g1, g2 be PartFunc of F,E; :: thesis: ( 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 ) implies g1 = g2 )

assume A40: ( 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 ) ) ; :: thesis: g1 = g2
A41: for y being Point of F st y in Ball (b,r2) holds
f1 . ((g1 . y),y) = 0. F
proof
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies f1 . ((g1 . y),y) = 0. F )
assume A42: y in Ball (b,r2) ; :: thesis: f1 . ((g1 . y),y) = 0. F
then g1 . y in rng g1 by ;
then g1 . y in Ball (a,r1) by A40;
then A43: f1 . ((g1 . y),y) = (f /. (g1 . y)) - y by ;
f /. (g1 . y) = y by ;
hence f1 . ((g1 . y),y) = 0. F by ; :: thesis: verum
end;
for y being Point of F st y in Ball (b,r2) holds
f1 . ((g2 . y),y) = 0. F
proof
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies f1 . ((g2 . y),y) = 0. F )
assume A45: y in Ball (b,r2) ; :: thesis: f1 . ((g2 . y),y) = 0. F
then g2 . y in rng g2 by ;
then g2 . y in Ball (a,r1) by A40;
then A46: f1 . ((g2 . y),y) = (f /. (g2 . y)) - y by ;
f /. (g2 . y) = y by ;
hence f1 . ((g2 . y),y) = 0. F by ; :: thesis: verum
end;
hence g1 = g2 by ; :: thesis: verum
end;