let l, m be non zero Element of NAT ; :: thesis: 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 ) )
let Z be Subset of [:(REAL-NS l),(REAL-NS m):]; :: thesis: 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 ) )
let f be PartFunc of [:(REAL-NS l),(REAL-NS m):],(REAL-NS m); :: thesis: 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 ) )
let a be Point of (REAL-NS l); :: thesis: 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 ) )
let b, c be Point of (REAL-NS m); :: thesis: 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 ) )
let z be Point of [:(REAL-NS l),(REAL-NS m):]; :: 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] & Det (Jacobian ((f * (reproj2 z)),(z `2))) <> 0. F_Real implies 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 ) ) )
assume A1: ( 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 ) ; :: thesis: 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 ) )
then A2: f is_differentiable_in z ;
A3: partdiff`2 (f,z) = diff ((f * (reproj2 z)),(z `2)) by NDIFF_7:def 7;
f * (reproj2 z) is_differentiable_in z `2 by A2, NDIFF_7:def 5, NDIFF_9:14;
then diff ((f * (reproj2 z)),(z `2)) is invertible by A1, Th31;
hence 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 ) ) by A1, A3, NDIFF_9:21; :: thesis: verum