theorem Th14: :: NDIFF10:14

for F being RealNormSpace
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 ) )