let E, F be non trivial RealBanachSpace; :: thesis:
let D be Subset of E; :: thesis:
let f be PartFunc of E,F; :: thesis:
let a be Point of E; :: thesis:
let b be Point of F; :: thesis:
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:
reconsider Z = [:D, the carrier of F:] as Subset of [:E,F:] by ZFMISC_1:96;
A9: Z is open by A1, Th4;
defpred S₁[ 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 & S₁[z,y] )

let z be object ; :: thesis:
assume z in Z ; :: thesis:
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:
thus ( w in the carrier of F & S₁[z,w] ) by A11; :: thesis:

end;

consider f1 being Function of Z, the carrier of F such that
A12: for x being object st x in Z holds
S₁[x,f1 . x] from FUNCT_2:sch 1(A10);
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:
let t be Point of F; :: thesis:
assume s in D ; :: thesis:
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 A12, ZFMISC_1:87;
( s = x & t = y ) by A15, XTUPLE_0:1;
hence f1 . (s,t) = (f /. s) - t by A15; :: thesis:

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 A2, A5, PARTFUN1:def 6;
then (f /. a) - b = 0. F by A6, RLVECT_1:15;
then A19: f1 . (a,b) = 0. F by A5, A14;
ex J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) 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 A5, A7, A9, A13, A16, A17, A19, Th14, ZFMISC_1:87;
take r1 ; :: thesis:
take r2 ; :: thesis:
thus ( 0 < r1 & 0 < r2 ) by A21; :: thesis:
for s being object st s in cl_Ball (a,r1) holds
s in D

proof

let s be object ; :: thesis:
assume A23: s in cl_Ball (a,r1) ; :: thesis:
b in Ball (b,r2) by A21, NDIFF_8:13;
then [s,b] in [:(cl_Ball (a,r1)),(Ball (b,r2)):] by A23, ZFMISC_1:87;
hence s in D by A21, ZFMISC_1:87; :: thesis:

end;

hence A24: cl_Ball (a,r1) c= D by TARSKI:def 3; :: thesis:
Ball (a,r1) c= cl_Ball (a,r1) by NDIFF_8:15;
then A25: Ball (a,r1) c= D by A24, XBOOLE_1:1;
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:

proof

let y be Point of F; :: thesis:
assume y in Ball (b,r2) ; :: thesis:
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:
(f /. x) - y = 0. F by A14, A25, A26;
hence ( x in Ball (a,r1) & f /. x = y ) by A26, RLVECT_1:21; :: thesis:

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:

proof

let y be Point of F; :: thesis:
assume A27: y in Ball (b,r2) ; :: thesis:
let x1, x2 be Point of E; :: thesis:
assume A28: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y ) ; :: thesis:
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 A14, A25, A28;
hence x1 = x2 by A21, A27, A28; :: thesis:

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:

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:
thus ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) ) by A29; :: thesis:
thus ( g is_continuous_on Ball (b,r2) & g . b = a ) by A29; :: thesis:
thus for y being Point of F st y in Ball (b,r2) holds
f /. (g /. y) = y :: thesis:

proof

let y be Point of F; :: thesis:
assume A30: y in Ball (b,r2) ; :: thesis:
then A31: f1 . ((g . y),y) = 0. F by A29;
g . y in rng g by A29, A30, FUNCT_1:3;
then g . y in Ball (a,r1) by A29;
then A32: (f /. (g . y)) - y = 0. F by A14, A25, A31;
g . y = g /. y by A29, A30, PARTFUN1:def 6;
hence f /. (g /. y) = y by A32, RLVECT_1:21; :: thesis:

end;

thus ( g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) ) by A29; :: thesis:
thus for y being Point of F st y in Ball (b,r2) holds
diff (g,y) = Inv (diff (f,(g /. y))) :: thesis:

proof

let y be Point of F; :: thesis:
assume A33: y in Ball (b,r2) ; :: thesis:
[(g /. y),y] is set ;
then reconsider z = [(g . y),y] as Point of [:E,F:] by A29, A33, PARTFUN1:def 6;
g . y in rng g by A29, A33, FUNCT_1:3;
then A34: g . y in Ball (a,r1) by A29;
g . y = g /. y by A29, A33, PARTFUN1:def 6;
then consider J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) 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 A29, A33
.= (- (Inv (diff (f,(g /. y))))) * (- J) by A35, LOPBAN13:26
.= (Inv (diff (f,(g /. y)))) * J by LOPBAN13:27
.= (modetrans ((Inv (diff (f,(g /. y)))),F,E)) * (id the carrier of F) by A35, LOPBAN_1:def 11
.= modetrans ((Inv (diff (f,(g /. y)))),F,E) by FUNCT_2:17
.= Inv (diff (f,(g /. y))) by LOPBAN_1:def 11 ; :: thesis:

end;

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

proof

let y be Point of F; :: thesis:
assume A36: y in Ball (b,r2) ; :: thesis:
[(g /. y),y] is set ;
then reconsider z = [(g . y),y] as Point of [:E,F:] by A29, A36, PARTFUN1:def 6;
g . y in rng g by A29, A36, FUNCT_1:3;
then A38: g . y in Ball (a,r1) by A29;
g . y = g /. y by A29, A36, PARTFUN1:def 6;
then ex J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) 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 A29, A36; :: thesis:

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:

proof

let g1, g2 be PartFunc of F,E; :: thesis:
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:
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:
assume A42: y in Ball (b,r2) ; :: thesis:
then g1 . y in rng g1 by A40, FUNCT_1:3;
then g1 . y in Ball (a,r1) by A40;
then A43: f1 . ((g1 . y),y) = (f /. (g1 . y)) - y by A14, A25;
f /. (g1 . y) = y by A40, A42;
hence f1 . ((g1 . y),y) = 0. F by A43, RLVECT_1:15; :: thesis:

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:
assume A45: y in Ball (b,r2) ; :: thesis:
then g2 . y in rng g2 by A40, FUNCT_1:3;
then g2 . y in Ball (a,r1) by A40;
then A46: f1 . ((g2 . y),y) = (f /. (g2 . y)) - y by A14, A25;
f /. (g2 . y) = y by A40, A45;
hence f1 . ((g2 . y),y) = 0. F by A46, RLVECT_1:15; :: thesis:

end;

hence g1 = g2 by A21, A40, A41; :: thesis:

end;