for E being RealNormSpace
for G, F 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`2 (f,z) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in Ball (b,r2) & y2 in Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g is_continuous_on Ball (a,r1) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & g is_differentiable_on Ball (a,r1) & g `| (Ball (a,r1)) is_continuous_on Ball (a,r1) & ( for x being Point of E
for z being Point of [:E,F:] st x in Ball (a,r1) & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) & ( for x being Point of E
for z being Point of [:E,F:] st x in Ball (a,r1) & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )