let E, F be non trivial RealBanachSpace; :: thesis: for Z being Subset of E

for f being PartFunc of E,F

for a being Point of E

for b being Point of F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= Z & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let D be Subset of E; :: thesis: for f being PartFunc of E,F

for a being Point of E

for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let f be PartFunc of E,F; :: thesis: for a being Point of E

for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let a be Point of E; :: thesis: for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let b be Point of F; :: thesis: ( D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible implies ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) ) )

assume that

A1: D is open and

A2: dom f = D and

A3: f is_differentiable_on D and

A4: f `| D is_continuous_on D and

A5: a in D and

A6: f . a = b and

A7: diff (f,a) is invertible ; :: thesis: ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

reconsider Z = [:D, the carrier of F:] as Subset of [:E,F:] by ZFMISC_1:96;

A9: Z is open by A1, Th4;

defpred S_{1}[ object , object ] means ex x being Point of E ex y being Point of F st

( $1 = [x,y] & $2 = (f /. x) - y );

A10: for z being object st z in Z holds

ex y being object st

( y in the carrier of F & S_{1}[z,y] )

A12: for x being object st x in Z holds

S_{1}[x,f1 . x]
from FUNCT_2:sch 1(A10);

A13: dom f1 = Z by FUNCT_2:def 1;

then ( dom f1 c= the carrier of [:E,F:] & rng f1 c= the carrier of F ) ;

then reconsider f1 = f1 as PartFunc of [:E,F:],F by RELSET_1:4;

A14: for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t

A16: f1 is_differentiable_on Z by A1, A2, A3, A4, A5, A13, A14, Th15;

A17: f1 `| Z is_continuous_on Z by A1, A2, A3, A4, A5, A13, A14, Th15;

f . a = f /. a by A2, A5, PARTFUN1:def 6;

then (f /. a) - b = 0. F by A6, RLVECT_1:15;

then A19: f1 . (a,b) = 0. F by A5, A14;

ex J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,a) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A5, A13, A14, Th15;

then consider r1, r2 being Real such that

A21: ( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] c= Z & ( for x being Point of F st x in Ball (b,r2) holds

ex y being Point of E st

( y in Ball (a,r1) & f1 . (y,x) = 0. F ) ) & ( for x being Point of F st x in Ball (b,r2) holds

for y1, y2 being Point of E st y1 in Ball (a,r1) & y2 in Ball (a,r1) & f1 . (y1,x) = 0. F & f1 . (y2,x) = 0. F holds

y1 = y2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for x being Point of F st x in Ball (b,r2) holds

f1 . ((g . x),x) = 0. F ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

partdiff`1 (f1,z) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f1 . ((g1 . y),y) = 0. F ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f1 . ((g2 . y),y) = 0. F ) holds

g1 = g2 ) ) by A5, A7, A9, A13, A16, A17, A19, Th14, ZFMISC_1:87;

take r1 ; :: thesis: ex r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

take r2 ; :: thesis: ( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

thus ( 0 < r1 & 0 < r2 ) by A21; :: thesis: ( cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

for s being object st s in cl_Ball (a,r1) holds

s in D

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

Ball (a,r1) c= cl_Ball (a,r1) by NDIFF_8:15;

then A25: Ball (a,r1) c= D by A24, XBOOLE_1:1;

thus for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) :: thesis: ( ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 :: thesis: ( ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) :: thesis: for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 :: thesis: verum

for f being PartFunc of E,F

for a being Point of E

for b being Point of F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= Z & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let D be Subset of E; :: thesis: for f being PartFunc of E,F

for a being Point of E

for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let f be PartFunc of E,F; :: thesis: for a being Point of E

for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let a be Point of E; :: thesis: for b being Point of F st D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

let b be Point of F; :: thesis: ( D is open & dom f = D & f is_differentiable_on D & f `| D is_continuous_on D & a in D & f . a = b & diff (f,a) is invertible implies ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) ) )

assume that

A1: D is open and

A2: dom f = D and

A3: f is_differentiable_on D and

A4: f `| D is_continuous_on D and

A5: a in D and

A6: f . a = b and

A7: diff (f,a) is invertible ; :: thesis: ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

reconsider Z = [:D, the carrier of F:] as Subset of [:E,F:] by ZFMISC_1:96;

A9: Z is open by A1, Th4;

defpred S

( $1 = [x,y] & $2 = (f /. x) - y );

A10: for z being object st z in Z holds

ex y being object st

( y in the carrier of F & S

proof

consider f1 being Function of Z, the carrier of F such that
let z be object ; :: thesis: ( z in Z implies ex y being object st

( y in the carrier of F & S_{1}[z,y] ) )

assume z in Z ; :: thesis: ex y being object st

( y in the carrier of F & S_{1}[z,y] )

then consider x being Point of E, y being Point of F such that

A11: z = [x,y] by PRVECT_3:18;

take w = (f /. x) - y; :: thesis: ( w in the carrier of F & S_{1}[z,w] )

thus ( w in the carrier of F & S_{1}[z,w] )
by A11; :: thesis: verum

end;( y in the carrier of F & S

assume z in Z ; :: thesis: ex y being object st

( y in the carrier of F & S

then consider x being Point of E, y being Point of F such that

A11: z = [x,y] by PRVECT_3:18;

take w = (f /. x) - y; :: thesis: ( w in the carrier of F & S

thus ( w in the carrier of F & S

A12: for x being object st x in Z holds

S

A13: dom f1 = Z by FUNCT_2:def 1;

then ( dom f1 c= the carrier of [:E,F:] & rng f1 c= the carrier of F ) ;

then reconsider f1 = f1 as PartFunc of [:E,F:],F by RELSET_1:4;

A14: for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t

proof

reconsider z = [a,b] as Point of [:E,F:] ;
let s be Point of E; :: thesis: for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t

let t be Point of F; :: thesis: ( s in D implies f1 . (s,t) = (f /. s) - t )

assume s in D ; :: thesis: f1 . (s,t) = (f /. s) - t

then consider x being Point of E, y being Point of F such that

A15: ( [s,t] = [x,y] & f1 . [s,t] = (f /. x) - y ) by A12, ZFMISC_1:87;

( s = x & t = y ) by A15, XTUPLE_0:1;

hence f1 . (s,t) = (f /. s) - t by A15; :: thesis: verum

end;f1 . (s,t) = (f /. s) - t

let t be Point of F; :: thesis: ( s in D implies f1 . (s,t) = (f /. s) - t )

assume s in D ; :: thesis: f1 . (s,t) = (f /. s) - t

then consider x being Point of E, y being Point of F such that

A15: ( [s,t] = [x,y] & f1 . [s,t] = (f /. x) - y ) by A12, ZFMISC_1:87;

( s = x & t = y ) by A15, XTUPLE_0:1;

hence f1 . (s,t) = (f /. s) - t by A15; :: thesis: verum

A16: f1 is_differentiable_on Z by A1, A2, A3, A4, A5, A13, A14, Th15;

A17: f1 `| Z is_continuous_on Z by A1, A2, A3, A4, A5, A13, A14, Th15;

f . a = f /. a by A2, A5, PARTFUN1:def 6;

then (f /. a) - b = 0. F by A6, RLVECT_1:15;

then A19: f1 . (a,b) = 0. F by A5, A14;

ex J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,a) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A5, A13, A14, Th15;

then consider r1, r2 being Real such that

A21: ( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] c= Z & ( for x being Point of F st x in Ball (b,r2) holds

ex y being Point of E st

( y in Ball (a,r1) & f1 . (y,x) = 0. F ) ) & ( for x being Point of F st x in Ball (b,r2) holds

for y1, y2 being Point of E st y1 in Ball (a,r1) & y2 in Ball (a,r1) & f1 . (y1,x) = 0. F & f1 . (y2,x) = 0. F holds

y1 = y2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for x being Point of F st x in Ball (b,r2) holds

f1 . ((g . x),x) = 0. F ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

partdiff`1 (f1,z) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f1 . ((g1 . y),y) = 0. F ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f1 . ((g2 . y),y) = 0. F ) holds

g1 = g2 ) ) by A5, A7, A9, A13, A16, A17, A19, Th14, ZFMISC_1:87;

take r1 ; :: thesis: ex r2 being Real st

( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

take r2 ; :: thesis: ( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

thus ( 0 < r1 & 0 < r2 ) by A21; :: thesis: ( cl_Ball (a,r1) c= D & ( for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

for s being object st s in cl_Ball (a,r1) holds

s in D

proof

hence A24:
cl_Ball (a,r1) c= D
by TARSKI:def 3; :: thesis: ( ( for y being Point of F st y in Ball (b,r2) holds
let s be object ; :: thesis: ( s in cl_Ball (a,r1) implies s in D )

assume A23: s in cl_Ball (a,r1) ; :: thesis: s in D

b in Ball (b,r2) by A21, NDIFF_8:13;

then [s,b] in [:(cl_Ball (a,r1)),(Ball (b,r2)):] by A23, ZFMISC_1:87;

hence s in D by A21, ZFMISC_1:87; :: thesis: verum

end;assume A23: s in cl_Ball (a,r1) ; :: thesis: s in D

b in Ball (b,r2) by A21, NDIFF_8:13;

then [s,b] in [:(cl_Ball (a,r1)),(Ball (b,r2)):] by A23, ZFMISC_1:87;

hence s in D by A21, ZFMISC_1:87; :: thesis: verum

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

Ball (a,r1) c= cl_Ball (a,r1) by NDIFF_8:15;

then A25: Ball (a,r1) c= D by A24, XBOOLE_1:1;

thus for y being Point of F st y in Ball (b,r2) holds

ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) :: thesis: ( ( for y being Point of F st y in Ball (b,r2) holds

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 ) & ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

proof

thus
for y being Point of F st y in Ball (b,r2) holds
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies ex x being Point of E st

( x in Ball (a,r1) & f /. x = y ) )

assume y in Ball (b,r2) ; :: thesis: ex x being Point of E st

( x in Ball (a,r1) & f /. x = y )

then consider x being Point of E such that

A26: ( x in Ball (a,r1) & f1 . (x,y) = 0. F ) by A21;

take x ; :: thesis: ( x in Ball (a,r1) & f /. x = y )

(f /. x) - y = 0. F by A14, A25, A26;

hence ( x in Ball (a,r1) & f /. x = y ) by A26, RLVECT_1:21; :: thesis: verum

end;( x in Ball (a,r1) & f /. x = y ) )

assume y in Ball (b,r2) ; :: thesis: ex x being Point of E st

( x in Ball (a,r1) & f /. x = y )

then consider x being Point of E such that

A26: ( x in Ball (a,r1) & f1 . (x,y) = 0. F ) by A21;

take x ; :: thesis: ( x in Ball (a,r1) & f /. x = y )

(f /. x) - y = 0. F by A14, A25, A26;

hence ( x in Ball (a,r1) & f /. x = y ) by A26, RLVECT_1:21; :: thesis: verum

for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 :: thesis: ( ex g being PartFunc of F,E st

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 ) )

proof

thus
ex g being PartFunc of F,E st
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2 )

assume A27: y in Ball (b,r2) ; :: thesis: for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2

let x1, x2 be Point of E; :: thesis: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y implies x1 = x2 )

assume A28: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y ) ; :: thesis: x1 = x2

then ( (f /. x1) - y = 0. F & (f /. x2) - y = 0. F ) by RLVECT_1:15;

then ( f1 . (x1,y) = 0. F & f1 . (x2,y) = 0. F ) by A14, A25, A28;

hence x1 = x2 by A21, A27, A28; :: thesis: verum

end;x1 = x2 )

assume A27: y in Ball (b,r2) ; :: thesis: for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds

x1 = x2

let x1, x2 be Point of E; :: thesis: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y implies x1 = x2 )

assume A28: ( x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y ) ; :: thesis: x1 = x2

then ( (f /. x1) - y = 0. F & (f /. x2) - y = 0. F ) by RLVECT_1:15;

then ( f1 . (x1,y) = 0. F & f1 . (x2,y) = 0. F ) by A14, A25, A28;

hence x1 = x2 by A21, A27, A28; :: thesis: verum

( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) ) :: thesis: for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2

proof

thus
for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds
consider g being PartFunc of F,E such that

A29: ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f1 . ((g . y),y) = 0. F ) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

partdiff`1 (f1,z) is invertible ) ) by A21;

take g ; :: thesis: ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) ) by A29; :: thesis: ( g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus ( g is_continuous_on Ball (b,r2) & g . b = a ) by A29; :: thesis: ( ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y :: thesis: ( g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) :: thesis: for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible

diff (f,(g /. y)) is invertible :: thesis: verum

end;A29: ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f1 . ((g . y),y) = 0. F ) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) ) & ( for y being Point of F

for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds

partdiff`1 (f1,z) is invertible ) ) by A21;

take g ; :: thesis: ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus ( dom g = Ball (b,r2) & rng g c= Ball (a,r1) ) by A29; :: thesis: ( g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus ( g is_continuous_on Ball (b,r2) & g . b = a ) by A29; :: thesis: ( ( for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus for y being Point of F st y in Ball (b,r2) holds

f /. (g /. y) = y :: thesis: ( g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

proof

thus
( g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) )
by A29; :: thesis: ( ( for y being Point of F st y in Ball (b,r2) holds
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies f /. (g /. y) = y )

assume A30: y in Ball (b,r2) ; :: thesis: f /. (g /. y) = y

then A31: f1 . ((g . y),y) = 0. F by A29;

g . y in rng g by A29, A30, FUNCT_1:3;

then g . y in Ball (a,r1) by A29;

then A32: (f /. (g . y)) - y = 0. F by A14, A25, A31;

g . y = g /. y by A29, A30, PARTFUN1:def 6;

hence f /. (g /. y) = y by A32, RLVECT_1:21; :: thesis: verum

end;assume A30: y in Ball (b,r2) ; :: thesis: f /. (g /. y) = y

then A31: f1 . ((g . y),y) = 0. F by A29;

g . y in rng g by A29, A30, FUNCT_1:3;

then g . y in Ball (a,r1) by A29;

then A32: (f /. (g . y)) - y = 0. F by A14, A25, A31;

g . y = g /. y by A29, A30, PARTFUN1:def 6;

hence f /. (g /. y) = y by A32, RLVECT_1:21; :: thesis: verum

diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible ) )

thus for y being Point of F st y in Ball (b,r2) holds

diff (g,y) = Inv (diff (f,(g /. y))) :: thesis: for y being Point of F st y in Ball (b,r2) holds

diff (f,(g /. y)) is invertible

proof

thus
for y being Point of F st y in Ball (b,r2) holds
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies diff (g,y) = Inv (diff (f,(g /. y))) )

assume A33: y in Ball (b,r2) ; :: thesis: diff (g,y) = Inv (diff (f,(g /. y)))

[(g /. y),y] is set ;

then reconsider z = [(g . y),y] as Point of [:E,F:] by A29, A33, PARTFUN1:def 6;

g . y in rng g by A29, A33, FUNCT_1:3;

then A34: g . y in Ball (a,r1) by A29;

g . y = g /. y by A29, A33, PARTFUN1:def 6;

then consider J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) such that

A35: ( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,(g /. y)) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A13, A14, A25, A34, Th15;

thus diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) by A29, A33

.= (- (Inv (diff (f,(g /. y))))) * (- J) by A35, LOPBAN13:26

.= (Inv (diff (f,(g /. y)))) * J by LOPBAN13:27

.= (modetrans ((Inv (diff (f,(g /. y)))),F,E)) * (id the carrier of F) by A35, LOPBAN_1:def 11

.= modetrans ((Inv (diff (f,(g /. y)))),F,E) by FUNCT_2:17

.= Inv (diff (f,(g /. y))) by LOPBAN_1:def 11 ; :: thesis: verum

end;assume A33: y in Ball (b,r2) ; :: thesis: diff (g,y) = Inv (diff (f,(g /. y)))

[(g /. y),y] is set ;

then reconsider z = [(g . y),y] as Point of [:E,F:] by A29, A33, PARTFUN1:def 6;

g . y in rng g by A29, A33, FUNCT_1:3;

then A34: g . y in Ball (a,r1) by A29;

g . y = g /. y by A29, A33, PARTFUN1:def 6;

then consider J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) such that

A35: ( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,(g /. y)) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A13, A14, A25, A34, Th15;

thus diff (g,y) = - ((Inv (partdiff`1 (f1,z))) * (partdiff`2 (f1,z))) by A29, A33

.= (- (Inv (diff (f,(g /. y))))) * (- J) by A35, LOPBAN13:26

.= (Inv (diff (f,(g /. y)))) * J by LOPBAN13:27

.= (modetrans ((Inv (diff (f,(g /. y)))),F,E)) * (id the carrier of F) by A35, LOPBAN_1:def 11

.= modetrans ((Inv (diff (f,(g /. y)))),F,E) by FUNCT_2:17

.= Inv (diff (f,(g /. y))) by LOPBAN_1:def 11 ; :: thesis: verum

diff (f,(g /. y)) is invertible :: thesis: verum

proof

let y be Point of F; :: thesis: ( y in Ball (b,r2) implies diff (f,(g /. y)) is invertible )

assume A36: y in Ball (b,r2) ; :: thesis: diff (f,(g /. y)) is invertible

[(g /. y),y] is set ;

then reconsider z = [(g . y),y] as Point of [:E,F:] by A29, A36, PARTFUN1:def 6;

g . y in rng g by A29, A36, FUNCT_1:3;

then A38: g . y in Ball (a,r1) by A29;

g . y = g /. y by A29, A36, PARTFUN1:def 6;

then ex J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,(g /. y)) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A13, A14, A25, A38, Th15;

hence diff (f,(g /. y)) is invertible by A29, A36; :: thesis: verum

end;assume A36: y in Ball (b,r2) ; :: thesis: diff (f,(g /. y)) is invertible

[(g /. y),y] is set ;

then reconsider z = [(g . y),y] as Point of [:E,F:] by A29, A36, PARTFUN1:def 6;

g . y in rng g by A29, A36, FUNCT_1:3;

then A38: g . y in Ball (a,r1) by A29;

g . y = g /. y by A29, A36, PARTFUN1:def 6;

then ex J being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,(g /. y)) & partdiff`2 (f1,z) = - J ) by A1, A2, A3, A4, A13, A14, A25, A38, Th15;

hence diff (f,(g /. y)) is invertible by A29, A36; :: thesis: verum

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) holds

g1 = g2 :: thesis: verum

proof

let g1, g2 be PartFunc of F,E; :: thesis: ( dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) implies g1 = g2 )

assume A40: ( dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) ) ; :: thesis: g1 = g2

A41: for y being Point of F st y in Ball (b,r2) holds

f1 . ((g1 . y),y) = 0. F

f1 . ((g2 . y),y) = 0. F

end;f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) implies g1 = g2 )

assume A40: ( dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds

f /. (g2 . y) = y ) ) ; :: thesis: g1 = g2

A41: for y being Point of F st y in Ball (b,r2) holds

f1 . ((g1 . y),y) = 0. F

proof

for y being Point of F st y in Ball (b,r2) holds
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies f1 . ((g1 . y),y) = 0. F )

assume A42: y in Ball (b,r2) ; :: thesis: f1 . ((g1 . y),y) = 0. F

then g1 . y in rng g1 by A40, FUNCT_1:3;

then g1 . y in Ball (a,r1) by A40;

then A43: f1 . ((g1 . y),y) = (f /. (g1 . y)) - y by A14, A25;

f /. (g1 . y) = y by A40, A42;

hence f1 . ((g1 . y),y) = 0. F by A43, RLVECT_1:15; :: thesis: verum

end;assume A42: y in Ball (b,r2) ; :: thesis: f1 . ((g1 . y),y) = 0. F

then g1 . y in rng g1 by A40, FUNCT_1:3;

then g1 . y in Ball (a,r1) by A40;

then A43: f1 . ((g1 . y),y) = (f /. (g1 . y)) - y by A14, A25;

f /. (g1 . y) = y by A40, A42;

hence f1 . ((g1 . y),y) = 0. F by A43, RLVECT_1:15; :: thesis: verum

f1 . ((g2 . y),y) = 0. F

proof

hence
g1 = g2
by A21, A40, A41; :: thesis: verum
let y be Point of F; :: thesis: ( y in Ball (b,r2) implies f1 . ((g2 . y),y) = 0. F )

assume A45: y in Ball (b,r2) ; :: thesis: f1 . ((g2 . y),y) = 0. F

then g2 . y in rng g2 by A40, FUNCT_1:3;

then g2 . y in Ball (a,r1) by A40;

then A46: f1 . ((g2 . y),y) = (f /. (g2 . y)) - y by A14, A25;

f /. (g2 . y) = y by A40, A45;

hence f1 . ((g2 . y),y) = 0. F by A46, RLVECT_1:15; :: thesis: verum

end;assume A45: y in Ball (b,r2) ; :: thesis: f1 . ((g2 . y),y) = 0. F

then g2 . y in rng g2 by A40, FUNCT_1:3;

then g2 . y in Ball (a,r1) by A40;

then A46: f1 . ((g2 . y),y) = (f /. (g2 . y)) - y by A14, A25;

f /. (g2 . y) = y by A40, A45;

hence f1 . ((g2 . y),y) = 0. F by A46, RLVECT_1:15; :: thesis: verum