let E be RealNormSpace; :: thesis:
let G, F be non trivial RealBanachSpace; :: thesis:
let Z0 be Subset of [:E,F:]; :: thesis:
let f0 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 A1: ( Z0 is open & dom f0 = Z0 & f0 is_differentiable_on Z0 & f0 `| Z0 is_continuous_on Z0 & [a,b] in Z0 & f0 . (a,b) = c & z = [a,b] & partdiff`2 (f0,z) is invertible ) ; :: thesis:
then A2: ( f0 is_partial_differentiable_on`1 Z0 & f0 is_partial_differentiable_on`2 Z0 & f0 `partial`1| Z0 is_continuous_on Z0 & f0 `partial`2| Z0 is_continuous_on Z0 ) by NDIFF_7:52;
set DF0 = f0 `| Z0;
set PDF2 = f0 `partial`2| Z0;
A3: dom (f0 `partial`2| Z0) = Z0 by A2, NDIFF_7:def 11;
A4: partdiff`2 (f0,z) in InvertibleOperators (F,G) by A1;
A5: (f0 `partial`2| Z0) . z = (f0 `partial`2| Z0) /. z by A1, A3, PARTFUN1:def 6;
then (f0 `partial`2| Z0) . z = partdiff`2 (f0,z) by A1, A2, NDIFF_7:def 11;
then consider p1 being Real such that
A8: ( 0 < p1 & Ball (((f0 `partial`2| Z0) /. z),p1) c= InvertibleOperators (F,G) ) by A4, A5, NDIFF_8:20;
consider s1 being Real such that
A9: ( 0 < s1 & ( for z1 being Point of [:E,F:] st z1 in Z0 & ||.(z1 - z).|| < s1 holds
||.(((f0 `partial`2| Z0) /. z1) - ((f0 `partial`2| Z0) /. z)).|| < p1 ) ) by A1, A2, A8, NFCONT_1:19;
consider s2 being Real such that
A10: ( 0 < s2 & Ball (z,s2) c= Z0 ) by A1, NDIFF_8:20;
set s = min (s1,s2);
A11: ( 0 < min (s1,s2) & min (s1,s2) <= s1 & min (s1,s2) <= s2 ) by A9, A10, XXREAL_0:17, XXREAL_0:21;
set Z = Ball (z,(min (s1,s2)));
set f = f0 | (Ball (z,(min (s1,s2))));
A12: z in Ball (z,(min (s1,s2))) by A11, NDIFF_8:13;
A15: (f0 | (Ball (z,(min (s1,s2))))) . (a,b) = c by A1, A11, FUNCT_1:49, NDIFF_8:13;
A16: Ball (z,(min (s1,s2))) c= Ball (z,s2) by A11, NDIFF_8:15;
then A18: Ball (z,(min (s1,s2))) c= Z0 by A10, XBOOLE_1:1;
A19: dom (f0 | (Ball (z,(min (s1,s2))))) = Ball (z,(min (s1,s2))) by A1, A10, A16, RELAT_1:62, XBOOLE_1:1;
f0 is_differentiable_on Ball (z,(min (s1,s2))) by A1, A10, A16, XBOOLE_1:1, NDIFF_1:46;
then A20: for x being Point of [:E,F:] st x in Ball (z,(min (s1,s2))) holds
f0 | (Ball (z,(min (s1,s2)))) is_differentiable_in x by NDIFF_1:def 8;
A21: (f0 | (Ball (z,(min (s1,s2))))) | (Ball (z,(min (s1,s2)))) = f0 | (Ball (z,(min (s1,s2)))) by RELAT_1:72;
then A22: f0 | (Ball (z,(min (s1,s2)))) is_differentiable_on Ball (z,(min (s1,s2))) by A19, A20, NDIFF_1:def 8;
set DF = (f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))));
A23: dom ((f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))))) = Ball (z,(min (s1,s2))) by A22, NDIFF_1:def 9;
A24: for z being Point of [:E,F:] st z in Ball (z,(min (s1,s2))) holds
diff (f0,z) = diff ((f0 | (Ball (z,(min (s1,s2))))),z)

let z be Point of [:E,F:]; :: thesis:
assume A25: z in Ball (z,(min (s1,s2))) ; :: thesis:
then f0 is_differentiable_in z by A1, A18, NDIFF_1:31;
hence diff (f0,z) = diff ((f0 | (Ball (z,(min (s1,s2))))),z) by A1, A18, A25, LMDIFF; :: thesis:

end;

for x0 being Point of [:E,F:]
for r being Real st x0 in Ball (z,(min (s1,s2))) & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Ball (z,(min (s1,s2))) & ||.(x1 - x0).|| < s holds
||.((((f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))))) /. x1) - (((f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))))) /. x0)).|| < r ) )

proof

let x0 be Point of [:E,F:]; :: thesis:
let r be Real; :: thesis:
assume A26: ( x0 in Ball (z,(min (s1,s2))) & 0 < r ) ; :: thesis:
then consider s being Real such that
A28: ( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z0 & ||.(x1 - x0).|| < s holds
||.(((f0 `| Z0) /. x1) - ((f0 `| Z0) /. x0)).|| < r ) ) by A1, A18, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A28; :: thesis:
let x1 be Point of [:E,F:]; :: thesis:
assume A29: ( x1 in Ball (z,(min (s1,s2))) & ||.(x1 - x0).|| < s ) ; :: thesis:
then A32: ((f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))))) /. x1 = diff ((f0 | (Ball (z,(min (s1,s2))))),x1) by A22, NDIFF_1:def 9
.= diff (f0,x1) by A24, A29
.= (f0 `| Z0) /. x1 by A1, A18, A29, NDIFF_1:def 9 ;
((f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))))) /. x0 = diff ((f0 | (Ball (z,(min (s1,s2))))),x0) by A22, A26, NDIFF_1:def 9
.= diff (f0,x0) by A24, A26
.= (f0 `| Z0) /. x0 by A1, A18, A26, NDIFF_1:def 9 ;
hence ||.((((f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))))) /. x1) - (((f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2))))) /. x0)).|| < r by A18, A28, A29, A32; :: thesis:

end;

then A34: (f0 | (Ball (z,(min (s1,s2))))) `| (Ball (z,(min (s1,s2)))) is_continuous_on Ball (z,(min (s1,s2))) by A23, NFCONT_1:19;
A35: f0 | (Ball (z,(min (s1,s2)))) is_continuous_on Ball (z,(min (s1,s2))) by A19, A20, A21, NDIFF_1:45, NDIFF_1:def 8;
A36: ( f0 | (Ball (z,(min (s1,s2)))) is_partial_differentiable_on`1 Ball (z,(min (s1,s2))) & f0 | (Ball (z,(min (s1,s2)))) is_partial_differentiable_on`2 Ball (z,(min (s1,s2))) & (f0 | (Ball (z,(min (s1,s2))))) `partial`1| (Ball (z,(min (s1,s2)))) is_continuous_on Ball (z,(min (s1,s2))) & (f0 | (Ball (z,(min (s1,s2))))) `partial`2| (Ball (z,(min (s1,s2)))) is_continuous_on Ball (z,(min (s1,s2))) ) by A22, A34, NDIFF_7:52;
A37: for z being Point of [:E,F:] st z in Ball (z,(min (s1,s2))) holds
( partdiff`1 (f0,z) = partdiff`1 ((f0 | (Ball (z,(min (s1,s2))))),z) & partdiff`2 (f0,z) = partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),z) )

proof

let z be Point of [:E,F:]; :: thesis:
assume A38: z in Ball (z,(min (s1,s2))) ; :: thesis:
then f0 | Z0 is_partial_differentiable_in`1 z by A2, A18;
then f0 is_partial_differentiable_in`1 z by A1, RELAT_1:69;
hence partdiff`1 (f0,z) = partdiff`1 ((f0 | (Ball (z,(min (s1,s2))))),z) by A1, A18, A38, LMPDIFF; :: thesis:
f0 | Z0 is_partial_differentiable_in`2 z by A2, A18, A38;
then f0 is_partial_differentiable_in`2 z by A1, RELAT_1:69;
hence partdiff`2 (f0,z) = partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),z) by A1, A18, A38, LMPDIFF; :: thesis:

end;

then partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),z) in { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) : v is invertible } by A4, A12;
then A44: ex v being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),z) = v & v is invertible ) ;
then (partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),z)) " is Lipschitzian LinearOperator of G,F by LOPBAN_1:def 9;
then consider r1, r2 being Real such that
A47: ( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Ball (z,(min (s1,s2))) & ( 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) & (f0 | (Ball (z,(min (s1,s2))))) . (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) & (f0 | (Ball (z,(min (s1,s2))))) . (x,y1) = c & (f0 | (Ball (z,(min (s1,s2))))) . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
(f0 | (Ball (z,(min (s1,s2))))) . (x,(g . x)) = c ) ) & ( 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
(f0 | (Ball (z,(min (s1,s2))))) . (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
(f0 | (Ball (z,(min (s1,s2))))) . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) by A1, A11, A15, A19, A35, A36, A44, NDIFF_8:13, NDIFF_8:36;
Ball (b,r2) c= cl_Ball (b,r2) by NDIFF_8:15;
then [:(Ball (a,r1)),(Ball (b,r2)):] c= [:(Ball (a,r1)),(cl_Ball (b,r2)):] by ZFMISC_1:95;
then A48: [:(Ball (a,r1)),(Ball (b,r2)):] c= Ball (z,(min (s1,s2))) by A47, XBOOLE_1:1;
A49: for x being Point of E
for y being Point of F st x in Ball (a,r1) & y in Ball (b,r2) holds
f0 . (x,y) = (f0 | (Ball (z,(min (s1,s2))))) . (x,y)

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
assume ( x in Ball (a,r1) & y in Ball (b,r2) ) ; :: thesis:
then [x,y] in [:(Ball (a,r1)),(Ball (b,r2)):] by ZFMISC_1:87;
hence f0 . (x,y) = (f0 | (Ball (z,(min (s1,s2))))) . (x,y) by A48, FUNCT_1:49; :: thesis:

end;

take r1 ; :: thesis:
take r2 ; :: thesis:
thus ( 0 < r1 & 0 < r2 ) by A47; :: thesis:
thus [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z0 by A18, A47, XBOOLE_1:1; :: thesis:
thus 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) & f0 . (x,y) = c ) :: thesis:

proof

let x be Point of E; :: thesis:
assume A52: x in Ball (a,r1) ; :: thesis:
then consider y being Point of F such that
A53: ( y in Ball (b,r2) & (f0 | (Ball (z,(min (s1,s2))))) . (x,y) = c ) by A47;
take y ; :: thesis:
thus y in Ball (b,r2) by A53; :: thesis:
thus f0 . (x,y) = c by A49, A52, A53; :: thesis:

end;

thus 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) & f0 . (x,y1) = c & f0 . (x,y2) = c holds
y1 = y2 :: thesis:

proof

let x be Point of E; :: thesis:
assume A54: x in Ball (a,r1) ; :: thesis:
let y1, y2 be Point of F; :: thesis:
assume A55: ( y1 in Ball (b,r2) & y2 in Ball (b,r2) & f0 . (x,y1) = c & f0 . (x,y2) = c ) ; :: thesis:
A56: (f0 | (Ball (z,(min (s1,s2))))) . (x,y1) = c by A49, A54, A55;
(f0 | (Ball (z,(min (s1,s2))))) . (x,y2) = c by A49, A54, A55;
hence y1 = y2 by A47, A54, A55, A56; :: thesis:

end;

consider g being PartFunc of E,F such that
A57: ( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
(f0 | (Ball (z,(min (s1,s2))))) . (x,(g . x)) = c ) ) by A47;
A58: for x being Point of E
for w being Point of [:E,F:] st x in Ball (a,r1) & w = [x,(g . x)] holds
partdiff`2 (f0,w) is invertible

proof

let x be Point of E; :: thesis:
let w be Point of [:E,F:]; :: thesis:
assume A59: ( x in Ball (a,r1) & w = [x,(g . x)] ) ; :: thesis:
then g . x in rng g by A57, FUNCT_1:3;
then w in [:(Ball (a,r1)),(Ball (b,r2)):] by A57, A59, ZFMISC_1:87;
then A60: w in Ball (z,(min (s1,s2))) by A48;
then w in { y where y is Point of [:E,F:] : ||.(y - z).|| < min (s1,s2) } by NDIFF_8:17;
then ex y being Point of [:E,F:] st
( w = y & ||.(y - z).|| < min (s1,s2) ) ;
then ||.(w - z).|| < s1 by A11, XXREAL_0:2;
then ||.(((f0 `partial`2| Z0) /. w) - ((f0 `partial`2| Z0) /. z)).|| < p1 by A9, A18, A60;
then (f0 `partial`2| Z0) /. w in { y where y is Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) : ||.(y - ((f0 `partial`2| Z0) /. z)).|| < p1 } ;
then (f0 `partial`2| Z0) /. w in Ball (((f0 `partial`2| Z0) /. z),p1) by NDIFF_8:17;
then (f0 `partial`2| Z0) /. w in InvertibleOperators (F,G) by A8;
then partdiff`2 (f0,w) in InvertibleOperators (F,G) by A2, A18, A60, NDIFF_7:def 11;
then ex v being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( partdiff`2 (f0,w) = v & v is invertible ) ;
hence partdiff`2 (f0,w) is invertible ; :: thesis:

end;

A63: for x being Point of E
for w being Point of [:E,F:] st x in Ball (a,r1) & w = [x,(g . x)] holds
partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),w) is invertible

proof

let x be Point of E; :: thesis:
let w be Point of [:E,F:]; :: thesis:
assume A64: ( x in Ball (a,r1) & w = [x,(g . x)] ) ; :: thesis:
then g . x in rng g by A57, FUNCT_1:3;
then w in [:(Ball (a,r1)),(Ball (b,r2)):] by A57, A64, ZFMISC_1:87;
then ( partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),w) = partdiff`2 (f0,w) & partdiff`1 ((f0 | (Ball (z,(min (s1,s2))))),w) = partdiff`1 (f0,w) ) by A37, A48;
hence partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),w) is invertible by A58, A64; :: thesis:

end;

A68: for x being Point of E st x in Ball (a,r1) holds
f0 . (x,(g . x)) = c

proof

let x be Point of E; :: thesis:
assume A69: x in Ball (a,r1) ; :: thesis:
then g . x in rng g by A57, FUNCT_1:3;
then f0 . (x,(g . x)) = (f0 | (Ball (z,(min (s1,s2))))) . (x,(g . x)) by A49, A57, A69;
hence f0 . (x,(g . x)) = c by A57, A69; :: thesis:

end;

A70: ( 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 (f0,z))) * (partdiff`1 (f0,z))) ) )

proof

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 (f0,z))) * (partdiff`1 (f0,z)))

proof

let x be Point of E; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A73: ( x in Ball (a,r1) & z = [x,(g . x)] ) ; :: thesis:
then g . x in rng g by A57, FUNCT_1:3;
then z in [:(Ball (a,r1)),(Ball (b,r2)):] by A57, A73, ZFMISC_1:87;
then ( partdiff`2 ((f0 | (Ball (z,(min (s1,s2))))),z) = partdiff`2 (f0,z) & partdiff`1 ((f0 | (Ball (z,(min (s1,s2))))),z) = partdiff`1 (f0,z) ) by A37, A48;
hence diff (g,x) = - ((Inv (partdiff`2 (f0,z))) * (partdiff`1 (f0,z))) by A19, A22, A34, A48, A57, A63, A73, Th47; :: thesis:

end;

hence ( 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 (f0,z))) * (partdiff`1 (f0,z))) ) ) by A19, A22, A34, A48, A57, A63, Th47; :: thesis:

end;

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
f0 . (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
f0 . (x,(g2 . x)) = c ) holds
g1 = g2

proof

let g1, g2 be PartFunc of E,F; :: thesis:
assume A75: ( dom g1 = Ball (a,r1) & rng g1 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f0 . (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
f0 . (x,(g2 . x)) = c ) ) ; :: thesis:

A76: now :: thesis:

let x be Point of E; :: thesis:
assume A77: x in Ball (a,r1) ; :: thesis:
then g1 . x in rng g1 by A75, FUNCT_1:3;
then f0 . (x,(g1 . x)) = (f0 | (Ball (z,(min (s1,s2))))) . (x,(g1 . x)) by A49, A75, A77;
hence (f0 | (Ball (z,(min (s1,s2))))) . (x,(g1 . x)) = c by A75, A77; :: thesis:

end;

now :: thesis:

let x be Point of E; :: thesis:
assume A78: x in Ball (a,r1) ; :: thesis:
then g2 . x in rng g2 by A75, FUNCT_1:3;
then f0 . (x,(g2 . x)) = (f0 | (Ball (z,(min (s1,s2))))) . (x,(g2 . x)) by A49, A75, A78;
hence (f0 | (Ball (z,(min (s1,s2))))) . (x,(g2 . x)) = c by A75, A78; :: thesis:

end;

hence g1 = g2 by A47, A75, A76; :: thesis:

end;

hence ( 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
f0 . (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 (f0,z))) * (partdiff`1 (f0,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 (f0,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
f0 . (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
f0 . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) by A57, A58, A68, A70; :: thesis: