let E, G be RealNormSpace; :: thesis:
let F be RealBanachSpace; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
let a be Point of E; :: thesis:
let b be Point of F; :: thesis:
let c be Point of G; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume that
A1: Z is open and
A2: dom f = Z and
A3: f is_continuous_on Z and
A4: f is_partial_differentiable_on`2 Z and
A5: f `partial`2| Z is_continuous_on Z and
A6: ( z = [a,b] & z in Z ) and
A7: f . (a,b) = c and
A8: partdiff`2 (f,z) is one-to-one and
A9: (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F ; :: thesis:
consider r1, r2 being Real such that
A10: ( 0 < r1 & 0 < r2 ) and
A11: [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z and
for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) and
A12: for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 and
A13: ( ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_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= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th1;
consider g being PartFunc of E,F such that
A14: ( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_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= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) by A13;
a in Ball (a,r1) by A10, LMBALL2;
then g | (Ball (a,r1)) is_continuous_in a by A14, NFCONT_1:def 7;
then consider r3 being Real such that
A15: ( 0 < r3 & ( for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < r3 holds
||.((g /. x1) - (g /. a)).|| < r2 ) ) by A10, A14, NFCONT_1:7;
reconsider r0 = min (r1,r3) as Real ;
A16: 0 < r0 by A10, A15, XXREAL_0:21;
A17: ( r0 <= r1 & r0 <= r3 ) by XXREAL_0:17;
take r0 ; :: thesis:
take r2 ; :: thesis:
thus ( 0 < r0 & 0 < r2 ) by A10, A15, XXREAL_0:21; :: thesis:
A18: ( Ball (a,r0) c= Ball (a,r1) & Ball (a,r0) c= Ball (a,r3) ) by A17, LMBALL1;
then A19: [:(Ball (a,r0)),(cl_Ball (b,r2)):] c= [:(Ball (a,r1)),(cl_Ball (b,r2)):] by ZFMISC_1:96;
A20: for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in Ball (b,r2) & f . (x,y) = c )

let x be Point of E; :: thesis:
assume A21: x in Ball (a,r0) ; :: thesis:
A22: g /. x = g . x by A14, A18, A21, PARTFUN1:def 6;
take y = g /. x; :: thesis:
x in Ball (a,r3) by A18, A21;
then ex q being Element of E st
( x = q & ||.(a - q).|| < r3 ) ;
then ||.(x - a).|| < r3 by NORMSP_1:7;
then ||.((g /. x) - (g /. a)).|| < r2 by A14, A15, A18, A21;
then A23: ||.((g /. a) - (g /. x)).|| < r2 by NORMSP_1:7;
g /. a = b by A10, A14, LMBALL2, PARTFUN1:def 6;
hence y in Ball (b,r2) by A23; :: thesis:
thus f . (x,y) = c by A14, A18, A21, A22; :: thesis:

end;

A24: for x being Point of E st x in Ball (a,r0) 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

proof

let x be Point of E; :: thesis:
assume A25: x in Ball (a,r0) ; :: thesis:
let y1, y2 be Point of F; :: thesis:
assume A26: ( y1 in Ball (b,r2) & y2 in Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c ) ; :: thesis:
Ball (b,r2) c= cl_Ball (b,r2) by LMBALL1;
hence y1 = y2 by A12, A18, A25, A26; :: thesis:

end;

reconsider g1 = g | (Ball (a,r0)) as PartFunc of E,F ;
g is_continuous_on Ball (a,r0) by A14, A18, NFCONT_1:23;
then A27: g1 is_continuous_on Ball (a,r0) by NFCONT_1:21;
A28: dom g1 = Ball (a,r0) by A14, A17, LMBALL1, RELAT_1:62;
A29: for y being object st y in rng g1 holds
y in Ball (b,r2)

proof

let y be object ; :: thesis:
assume y in rng g1 ; :: thesis:
then consider x being object such that
A30: ( x in dom g1 & y = g1 . x ) by FUNCT_1:def 3;
reconsider x = x as Point of E by A30;
A31: g /. x = g . x by A14, A18, A28, A30, PARTFUN1:def 6;
A32: g1 . x = g . x by A30, FUNCT_1:47;
x in Ball (a,r3) by A18, A28, A30;
then ex q being Element of E st
( x = q & ||.(a - q).|| < r3 ) ;
then ||.(x - a).|| < r3 by NORMSP_1:7;
then ||.((g /. x) - (g /. a)).|| < r2 by A14, A15, A18, A28, A30;
then A33: ||.((g /. a) - (g /. x)).|| < r2 by NORMSP_1:7;
g /. a = b by A10, A14, LMBALL2, PARTFUN1:def 6;
hence y in Ball (b,r2) by A30, A31, A32, A33; :: thesis:

end;

A34: g1 . a = b by A14, A16, A28, FUNCT_1:47, LMBALL2;
A35: for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c

proof

let x be Point of E; :: thesis:
assume A36: x in Ball (a,r0) ; :: thesis:
hence f . (x,(g1 . x)) = f . (x,(g . x)) by A28, FUNCT_1:47
.= c by A14, A18, A36 ;
:: thesis:

end;

for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2

proof

let g1, g2 be PartFunc of E,F; :: thesis:
assume A38: ( dom g1 = Ball (a,r0) & rng g1 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) ) ; :: thesis:
for x being object st x in dom g1 holds
g1 . x = g2 . x

proof

let x0 be object ; :: thesis:
assume A39: x0 in dom g1 ; :: thesis:
then reconsider x = x0 as Point of E ;
A40: g1 . x0 in rng g1 by A39, FUNCT_1:3;
then reconsider y1 = g1 . x0 as Point of F ;
A41: g2 . x0 in rng g2 by A38, A39, FUNCT_1:3;
then reconsider y2 = g2 . x0 as Point of F ;
( y1 in Ball (b,r2) & y2 in Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c ) by A38, A39, A40, A41;
hence g1 . x0 = g2 . x0 by A24, A38, A39; :: thesis:

end;

hence g1 = g2 by A38, FUNCT_1:2; :: thesis:

end;

hence ( [:(Ball (a,r0)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r0) 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,r0) 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
( g is_continuous_on Ball (a,r0) & dom g = Ball (a,r0) & rng g c= Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) by A11, A19, A20, A24, A27, A28, A29, A34, A35, TARSKI:def 3, XBOOLE_1:1; :: thesis: