let F be RealNormSpace; :: thesis: for G, E being non trivial RealBanachSpace

for Z being Subset of [:E,F:]

for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let G, E be non trivial RealBanachSpace; :: thesis: for Z being Subset of [:E,F:]

for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let Z be Subset of [:E,F:]; :: thesis: for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let f be PartFunc of [:E,F:],G; :: thesis: for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let a be Point of E; :: thesis: for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let b be Point of F; :: thesis: for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let c be Point of G; :: thesis: for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let z be Point of [:E,F:]; :: thesis: ( Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible implies ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) ) )

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: ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

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: ex r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

take r2 ; :: thesis: ( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

thus ( 0 < r1 & 0 < r2 ) by A20; :: thesis: ( [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

for s being object st s in [:(cl_Ball (a,r1)),(Ball (b,r2)):] holds

s in Z

ex x being Point of E st

( x in Ball (a,r1) & f . (x,y) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

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: ( ( 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 ) & 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 ) ) & ( 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 ) )

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: ( 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 ) ) & ( 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 ) )

( 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: 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

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: verum

for Z being Subset of [:E,F:]

for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let G, E be non trivial RealBanachSpace; :: thesis: for Z being Subset of [:E,F:]

for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let Z be Subset of [:E,F:]; :: thesis: for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let f be PartFunc of [:E,F:],G; :: thesis: for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let a be Point of E; :: thesis: for b being Point of F

for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let b be Point of F; :: thesis: for c being Point of G

for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let c be Point of G; :: thesis: for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

let z be Point of [:E,F:]; :: thesis: ( Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible implies ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) ) )

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: ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

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: ex r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

take r2 ; :: thesis: ( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

thus ( 0 < r1 & 0 < r2 ) by A20; :: thesis: ( [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

for s being object st s in [:(cl_Ball (a,r1)),(Ball (b,r2)):] holds

s in Z

proof

hence
[:(cl_Ball (a,r1)),(Ball (b,r2)):] c= Z
; :: thesis: ( ( for y being Point of F st y in Ball (b,r2) holds
let s be object ; :: thesis: ( s in [:(cl_Ball (a,r1)),(Ball (b,r2)):] implies s in Z )

assume s in [:(cl_Ball (a,r1)),(Ball (b,r2)):] ; :: thesis: s in Z

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: verum

end;assume s in [:(cl_Ball (a,r1)),(Ball (b,r2)):] ; :: thesis: s in Z

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: verum

ex x being Point of E st

( x in Ball (a,r1) & f . (x,y) = 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 . (x1,y) = c & f . (x2,y) = 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 . ((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 ) ) & ( 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 ) )

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: ( ( 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 ) & 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 ) ) & ( 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 ) )

proof

thus
for y being Point of F st y in Ball (b,r2) holds
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) = c ) )

assume y in Ball (b,r2) ; :: thesis: ex x being Point of E st

( x in Ball (a,r1) & f . (x,y) = c )

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: ( x in Ball (a,r1) & f . (x,y) = c )

thus x in Ball (a,r1) by A26; :: thesis: f . (x,y) = c

thus f . (x,y) = c by A9, A26, Th8; :: thesis: verum

end;( x in Ball (a,r1) & f . (x,y) = c ) )

assume y in Ball (b,r2) ; :: thesis: ex x being Point of E st

( x in Ball (a,r1) & f . (x,y) = c )

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: ( x in Ball (a,r1) & f . (x,y) = c )

thus x in Ball (a,r1) by A26; :: thesis: f . (x,y) = c

thus f . (x,y) = c by A9, A26, Th8; :: thesis: verum

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: ( 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 ) ) & ( 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 ) )

proof

thus
ex g being PartFunc of F,E st
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) = c & f . (x2,y) = c 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) = c & f . (x2,y) = c holds

x1 = x2

let x1, x2 be Point of E; :: thesis: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f . (x1,y) = c & f . (x2,y) = c implies x1 = x2 )

assume A28: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f . (x1,y) = c & f . (x2,y) = c ) ; :: thesis: x1 = x2

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: verum

end;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) = c & f . (x2,y) = c holds

x1 = x2

let x1, x2 be Point of E; :: thesis: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f . (x1,y) = c & f . (x2,y) = c implies x1 = x2 )

assume A28: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f . (x1,y) = c & f . (x2,y) = c ) ; :: thesis: x1 = x2

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: verum

( 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: 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

proof

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

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

thus for y being Point of F st y in Ball (b,r2) holds

f . ((g . y),y) = c :: thesis: ( 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 ) )

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

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

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: verum

end;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: ( 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 ) )

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

thus for y being Point of F st y in Ball (b,r2) holds

f . ((g . y),y) = c :: thesis: ( 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 ) )

proof

thus
( g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) )
by A30; :: thesis: ( ( for y being Point of F
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies f . ((g . y),y) = c )

assume A31: y in Ball (b,r2) ; :: thesis: f . ((g . y),y) = c

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: verum

end;assume A31: y in Ball (b,r2) ; :: thesis: f . ((g . y),y) = c

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: verum

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

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

proof

thus
for y being Point of F
let y be Point of F; :: thesis: 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)))

let z be Point of [:E,F:]; :: thesis: ( y in Ball (b,r2) & z = [(g . y),y] implies diff (g,y) = - ((Inv (partdiff`1 (f,z))) * (partdiff`2 (f,z))) )

assume A33: ( y in Ball (b,r2) & z = [(g . y),y] ) ; :: thesis: diff (g,y) = - ((Inv (partdiff`1 (f,z))) * (partdiff`2 (f,z)))

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: verum

end;diff (g,y) = - ((Inv (partdiff`1 (f,z))) * (partdiff`2 (f,z)))

let z be Point of [:E,F:]; :: thesis: ( y in Ball (b,r2) & z = [(g . y),y] implies diff (g,y) = - ((Inv (partdiff`1 (f,z))) * (partdiff`2 (f,z))) )

assume A33: ( y in Ball (b,r2) & z = [(g . y),y] ) ; :: thesis: diff (g,y) = - ((Inv (partdiff`1 (f,z))) * (partdiff`2 (f,z)))

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: verum

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: verum

proof

let y be Point of F; :: thesis: for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

partdiff`1 (f,z) is invertible

let z be Point of [:E,F:]; :: thesis: ( y in Ball (b,r2) & z = [(g . y),y] implies partdiff`1 (f,z) is invertible )

assume A37: ( y in Ball (b,r2) & z = [(g . y),y] ) ; :: thesis: partdiff`1 (f,z) is invertible

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: verum

end;partdiff`1 (f,z) is invertible

let z be Point of [:E,F:]; :: thesis: ( y in Ball (b,r2) & z = [(g . y),y] implies partdiff`1 (f,z) is invertible )

assume A37: ( y in Ball (b,r2) & z = [(g . y),y] ) ; :: thesis: partdiff`1 (f,z) is invertible

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: verum

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: 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) = 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 ) implies g1 = g2 )

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: g1 = g2

A42: for y being Point of F st y in Ball (b,r2) holds

(f * (Exch (F,E))) . (y,(g1 . y)) = c

(f * (Exch (F,E))) . (y,(g2 . y)) = c

end;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 ) implies g1 = g2 )

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: g1 = g2

A42: for y being Point of F st y in Ball (b,r2) holds

(f * (Exch (F,E))) . (y,(g1 . y)) = c

proof

for y being Point of F st y in Ball (b,r2) holds
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies (f * (Exch (F,E))) . (y,(g1 . y)) = c )

assume A43: y in Ball (b,r2) ; :: thesis: (f * (Exch (F,E))) . (y,(g1 . y)) = c

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: verum

end;assume A43: y in Ball (b,r2) ; :: thesis: (f * (Exch (F,E))) . (y,(g1 . y)) = c

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: verum

(f * (Exch (F,E))) . (y,(g2 . y)) = c

proof

hence
g1 = g2
by A20, A41, A42; :: thesis: verum
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies (f * (Exch (F,E))) . (y,(g2 . y)) = c )

assume A45: y in Ball (b,r2) ; :: thesis: (f * (Exch (F,E))) . (y,(g2 . y)) = c

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: verum

end;assume A45: y in Ball (b,r2) ; :: thesis: (f * (Exch (F,E))) . (y,(g2 . y)) = c

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: verum