let F be RealNormSpace; :: thesis:
let G, E be non trivial RealBanachSpace; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
let a be Point of E; :: thesis:
let b be Point of F; :: thesis:
let c be Point of G; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume that
A1: Z is open and
A2: dom f = Z and
A3: f is_differentiable_on Z and
A4: f `| Z is_continuous_on Z and
A5: [a,b] in Z and
A6: f . (a,b) = c and
A7: z = [a,b] and
A8: partdiff`1 (f,z) is invertible ; :: thesis:
set I = Exch (F,E);
A9: ( Exch (F,E) is one-to-one & Exch (F,E) is onto & Exch (F,E) is isometric & ( for s being Point of F
for t being Point of E holds (Exch (F,E)) . (s,t) = [t,s] ) ) by Def1;
then consider J being LinearOperator of [:E,F:],[:F,E:] such that
A10: ( J = (Exch (F,E)) " & J is one-to-one & J is onto & J is isometric ) by NDIFF_7:9;
set Z1 = J .: Z;
set f1 = f * (Exch (F,E));
A11: J .: Z is open by A1, A10, NDIFF_7:13;
A12: (Exch (F,E)) " Z = J .: Z by A9, A10, FUNCT_1:85;
A13: dom (f * (Exch (F,E))) = (Exch (F,E)) " (dom f) by A9, Th8
.= J .: Z by A2, A9, A10, FUNCT_1:85 ;
A14: f * (Exch (F,E)) is_differentiable_on J .: Z by A3, A9, A12, NDIFF_7:29;
reconsider z1 = [b,a] as Point of [:F,E:] ;
A16: (f * (Exch (F,E))) `| (J .: Z) is_continuous_on J .: Z by A3, A4, A9, A12, Th10;
A18: (f * (Exch (F,E))) . (b,a) = c by A6, A9, Th8;
A19: partdiff`1 (f,z) = partdiff`2 ((f * (Exch (F,E))),z1) by A7, A9, Th11;
consider r2, r1 being Real such that
A20: ( 0 < r2 & 0 < r1 & [:(Ball (b,r2)),(cl_Ball (a,r1)):] c= J .: 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 * (Exch (F,E))) . (y,x) = c ) ) & ( 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 * (Exch (F,E))) . (y,x1) = c & (f * (Exch (F,E))) . (y,x2) = c 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 * (Exch (F,E))) . (y,(g . y)) = c ) & 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 [:F,E:] st y in Ball (b,r2) & z = [y,(g . y)] holds
diff (g,y) = - ((Inv (partdiff`2 ((f * (Exch (F,E))),z))) * (partdiff`1 ((f * (Exch (F,E))),z))) ) & ( for y being Point of F
for z being Point of [:F,E:] st y in Ball (b,r2) & z = [y,(g . y)] holds
partdiff`2 ((f * (Exch (F,E))),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
(f * (Exch (F,E))) . (y,(g1 . y)) = c ) & 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 * (Exch (F,E))) . (y,(g2 . y)) = c ) holds
g1 = g2 ) ) by A5, A8, A11, A12, A13, A14, A16, A18, A19, Th7, NDIFF_9:21;
take r1 ; :: thesis:
take r2 ; :: thesis:
thus ( 0 < r1 & 0 < r2 ) by A20; :: thesis:
for s being object st s in [:(cl_Ball (a,r1)),(Ball (b,r2)):] holds
s in Z

let s be object ; :: thesis:
assume s in [:(cl_Ball (a,r1)),(Ball (b,r2)):] ; :: thesis:
then consider x, y being object such that
A22: ( x in cl_Ball (a,r1) & y in Ball (b,r2) & s = [x,y] ) by ZFMISC_1:def 2;
[y,x] in [:(Ball (b,r2)),(cl_Ball (a,r1)):] by A22, ZFMISC_1:def 2;
hence s in Z by A12, A20, A22, Th7; :: thesis:

end;

hence [:(cl_Ball (a,r1)),(Ball (b,r2)):] c= Z ; :: thesis:
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) = c ) :: 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) & (f * (Exch (F,E))) . (y,x) = c ) by A20;
take x ; :: thesis:
thus x in Ball (a,r1) by A26; :: thesis:
thus f . (x,y) = c by A9, A26, Th8; :: 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) = c & f . (x2,y) = c 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) = c & f . (x2,y) = c ) ; :: thesis:
A29: (f * (Exch (F,E))) . (y,x1) = f . (x1,y) by A9, Th8;
(f * (Exch (F,E))) . (y,x2) = f . (x2,y) by A9, Th8;
hence x1 = x2 by A20, A27, A28, A29; :: 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) = c ) & 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 (f,z))) * (partdiff`2 (f,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 (f,z) is invertible ) ) :: thesis:

proof

consider g being PartFunc of F,E such that
A30: ( 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 * (Exch (F,E))) . (y,(g . y)) = c ) & 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 [:F,E:] st y in Ball (b,r2) & z = [y,(g . y)] holds
diff (g,y) = - ((Inv (partdiff`2 ((f * (Exch (F,E))),z))) * (partdiff`1 ((f * (Exch (F,E))),z))) ) & ( for y being Point of F
for z being Point of [:F,E:] st y in Ball (b,r2) & z = [y,(g . y)] holds
partdiff`2 ((f * (Exch (F,E))),z) is invertible ) ) by A20;
take g ; :: thesis:
thus ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a ) by A30; :: thesis:
thus for y being Point of F st y in Ball (b,r2) holds
f . ((g . y),y) = c :: thesis:

proof

let y be Point of F; :: thesis:
assume A31: y in Ball (b,r2) ; :: thesis:
then A32: (f * (Exch (F,E))) . (y,(g . y)) = c by A30;
g . y in rng g by A30, A31, FUNCT_1:3;
hence f . ((g . y),y) = c by A9, A32, Th8; :: thesis:

end;

thus ( g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) ) by A30; :: thesis:
thus 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 (f,z))) * (partdiff`2 (f,z))) :: thesis:

proof

let y be Point of F; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A33: ( y in Ball (b,r2) & z = [(g . y),y] ) ; :: thesis:
then g . y in rng g by A30, FUNCT_1:3;
then reconsider x = g . y as Point of E ;
reconsider z0 = [y,x] as Point of [:F,E:] ;
( partdiff`1 (f,z) = partdiff`2 ((f * (Exch (F,E))),z0) & partdiff`2 (f,z) = partdiff`1 ((f * (Exch (F,E))),z0) ) by A9, A33, Th11;
hence diff (g,y) = - ((Inv (partdiff`1 (f,z))) * (partdiff`2 (f,z))) by A30, A33; :: thesis:

end;

thus 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 (f,z) is invertible :: thesis:

proof

let y be Point of F; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A37: ( y in Ball (b,r2) & z = [(g . y),y] ) ; :: thesis:
then g . y in rng g by A30, FUNCT_1:3;
then reconsider x = g . y as Point of E ;
reconsider z0 = [y,x] as Point of [:F,E:] ;
( partdiff`1 (f,z) = partdiff`2 ((f * (Exch (F,E))),z0) & partdiff`2 (f,z) = partdiff`1 ((f * (Exch (F,E))),z0) ) by A9, A37, Th11;
hence partdiff`1 (f,z) is invertible by A30, A37; :: 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) = c ) & 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) = c ) holds
g1 = g2 :: thesis:

proof

let g1, g2 be PartFunc of F,E; :: thesis:
assume A41: ( 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) = c ) & 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) = c ) ) ; :: thesis:
A42: for y being Point of F st y in Ball (b,r2) holds
(f * (Exch (F,E))) . (y,(g1 . y)) = c

proof

let y be Point of F; :: thesis:
assume A43: y in Ball (b,r2) ; :: thesis:
then A44: f . ((g1 . y),y) = c by A41;
g1 . y in rng g1 by A41, A43, FUNCT_1:3;
hence (f * (Exch (F,E))) . (y,(g1 . y)) = c by A9, A44, Th8; :: thesis:

end;

for y being Point of F st y in Ball (b,r2) holds
(f * (Exch (F,E))) . (y,(g2 . y)) = c

proof

let y be Point of F; :: thesis:
assume A45: y in Ball (b,r2) ; :: thesis:
then A46: f . ((g2 . y),y) = c by A41;
g2 . y in rng g2 by A41, A45, FUNCT_1:3;
hence (f * (Exch (F,E))) . (y,(g2 . y)) = c by A9, A46, Th8; :: thesis:

end;

hence g1 = g2 by A20, A41, A42; :: thesis:

end;