theorem :: NDIFF11:33

for l, m being non zero Element of NAT
for Z being Subset of [:(REAL-NS l),(REAL-NS m):]
for f being PartFunc of [:(REAL-NS l),(REAL-NS m):],(REAL-NS m)
for a being Point of (REAL-NS l)
for b, c being Point of (REAL-NS m)
for z being Point of [:(REAL-NS l),(REAL-NS m):] 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] & Det (Jacobian ((f * (reproj2 z)),(z `2))) <> 0. F_Real 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 (REAL-NS l) st x in Ball (a,r1) holds
ex y being Point of (REAL-NS m) st
( y in Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
for y1, y2 being Point of (REAL-NS m) 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 (REAL-NS l),(REAL-NS m) 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 (REAL-NS l) 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 (REAL-NS l)
for z being Point of [:(REAL-NS l),(REAL-NS m):] 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 (REAL-NS l)
for z being Point of [:(REAL-NS l),(REAL-NS m):] st x in Ball (a,r1) & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) ) & ( for g1, g2 being PartFunc of (REAL-NS l),(REAL-NS m) st dom g1 = Ball (a,r1) & rng g1 c= Ball (b,r2) & ( for x being Point of (REAL-NS l) 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 (REAL-NS l) st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )