:: by Kazuhisa Nakasho and Yuichi Futa

::

:: Received March 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

theorem Th1: :: NDIFF10:1

for X, Y being RealNormSpace

for f being PartFunc of X,Y

for A being Subset of X

for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

for f being PartFunc of X,Y

for A being Subset of X

for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

proof end;

theorem Th2: :: NDIFF10:2

for X, Y being RealNormSpace

for x being Point of X

for y being Point of Y

for z being Point of [:X,Y:]

for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds

ex s being Real st

( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )

for x being Point of X

for y being Point of Y

for z being Point of [:X,Y:]

for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds

ex s being Real st

( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )

proof end;

theorem Th3: :: NDIFF10:3

for X, Y being RealNormSpace

for V being Subset of [:X,Y:] holds

( V is open iff for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

for V being Subset of [:X,Y:] holds

( V is open iff for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

proof end;

theorem Th4: :: NDIFF10:4

for X, Y being RealNormSpace

for V being Subset of [:X,Y:]

for D being Subset of X st D is open & V = [:D, the carrier of Y:] holds

V is open

for V being Subset of [:X,Y:]

for D being Subset of X st D is open & V = [:D, the carrier of Y:] holds

V is open

proof end;

theorem :: NDIFF10:5

for X, Y being RealNormSpace

for V being Subset of [:X,Y:]

for D being Subset of Y st D is open & V = [: the carrier of X,D:] holds

V is open

for V being Subset of [:X,Y:]

for D being Subset of Y st D is open & V = [: the carrier of X,D:] holds

V is open

proof end;

theorem Th6: :: NDIFF10:6

for x, y being Real

for u, v being Element of REAL 2 st u = <*x,y*> & v = <*y,x*> holds

|.u.| = |.v.|

for u, v being Element of REAL 2 st u = <*x,y*> & v = <*y,x*> holds

|.u.| = |.v.|

proof end;

definition

let X, Y be RealNormSpace;

ex b_{1} being LinearOperator of [:X,Y:],[:Y,X:] st

( b_{1} is one-to-one & b_{1} is onto & b_{1} is isometric & ( for x being Point of X

for y being Point of Y holds b_{1} . (x,y) = [y,x] ) )

for b_{1}, b_{2} being LinearOperator of [:X,Y:],[:Y,X:] st b_{1} is one-to-one & b_{1} is onto & b_{1} is isometric & ( for x being Point of X

for y being Point of Y holds b_{1} . (x,y) = [y,x] ) & b_{2} is one-to-one & b_{2} is onto & b_{2} is isometric & ( for x being Point of X

for y being Point of Y holds b_{2} . (x,y) = [y,x] ) holds

b_{1} = b_{2}

end;
func Exch (X,Y) -> LinearOperator of [:X,Y:],[:Y,X:] means :Def1: :: NDIFF10:def 1

( it is one-to-one & it is onto & it is isometric & ( for x being Point of X

for y being Point of Y holds it . (x,y) = [y,x] ) );

existence ( it is one-to-one & it is onto & it is isometric & ( for x being Point of X

for y being Point of Y holds it . (x,y) = [y,x] ) );

ex b

( b

for y being Point of Y holds b

proof end;

uniqueness for b

for y being Point of Y holds b

for y being Point of Y holds b

b

proof end;

:: deftheorem Def1 defines Exch NDIFF10:def 1 :

for X, Y being RealNormSpace

for b_{3} being LinearOperator of [:X,Y:],[:Y,X:] holds

( b_{3} = Exch (X,Y) iff ( b_{3} is one-to-one & b_{3} is onto & b_{3} is isometric & ( for x being Point of X

for y being Point of Y holds b_{3} . (x,y) = [y,x] ) ) );

for X, Y being RealNormSpace

for b

( b

for y being Point of Y holds b

theorem Th7: :: NDIFF10:7

for X, Y being RealNormSpace

for Z being Subset of [:X,Y:]

for x, y being object holds

( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )

for Z being Subset of [:X,Y:]

for x, y being object holds

( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )

proof end;

theorem Th8: :: NDIFF10:8

for X, Y being RealNormSpace

for Z being non empty set

for f being PartFunc of [:X,Y:],Z

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

for Z being non empty set

for f being PartFunc of [:X,Y:],Z

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

proof end;

theorem Th9: :: NDIFF10:9

for X, Y, Z being RealNormSpace

for f being PartFunc of Y,Z

for I being LinearOperator of X,Y

for V being Subset of Y st f is_differentiable_on V & I is one-to-one & I is onto & I is isometric holds

for y being Point of Y st y in V holds

(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")

for f being PartFunc of Y,Z

for I being LinearOperator of X,Y

for V being Subset of Y st f is_differentiable_on V & I is one-to-one & I is onto & I is isometric holds

for y being Point of Y st y in V holds

(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")

proof end;

theorem Th10: :: NDIFF10:10

for X, Y, Z being RealNormSpace

for V being Subset of Y

for g being PartFunc of Y,Z

for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

for V being Subset of Y

for g being PartFunc of Y,Z

for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

proof end;

theorem Th11: :: NDIFF10:11

for X, Y, Z being RealNormSpace

for f being PartFunc of [:X,Y:],Z

for U being Subset of [:X,Y:]

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

for f being PartFunc of [:X,Y:],Z

for U being Subset of [:X,Y:]

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

proof end;

theorem :: NDIFF10:12

for X, Y, Z being RealNormSpace

for f being PartFunc of [:X,Y:],Z

for U being Subset of [:X,Y:]

for I being LinearOperator of [:Y,X:],[:X,Y:] st U = dom f & f is_differentiable_on U & I is one-to-one & I is onto & I is isometric & ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( ( f is_partial_differentiable_in`1 u implies f * I is_partial_differentiable_in`2 v ) & ( f * I is_partial_differentiable_in`2 v implies f is_partial_differentiable_in`1 u ) & ( f is_partial_differentiable_in`2 u implies f * I is_partial_differentiable_in`1 v ) & ( f * I is_partial_differentiable_in`1 v implies f is_partial_differentiable_in`2 u ) ) by Th11;

for f being PartFunc of [:X,Y:],Z

for U being Subset of [:X,Y:]

for I being LinearOperator of [:Y,X:],[:X,Y:] st U = dom f & f is_differentiable_on U & I is one-to-one & I is onto & I is isometric & ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( ( f is_partial_differentiable_in`1 u implies f * I is_partial_differentiable_in`2 v ) & ( f * I is_partial_differentiable_in`2 v implies f is_partial_differentiable_in`1 u ) & ( f is_partial_differentiable_in`2 u implies f * I is_partial_differentiable_in`1 v ) & ( f * I is_partial_differentiable_in`1 v implies f is_partial_differentiable_in`2 u ) ) by Th11;

theorem :: NDIFF10:13

for X, Y, Z being RealNormSpace

for f being PartFunc of [:X,Y:],Z

for U being Subset of [:X,Y:]

for I being LinearOperator of [:Y,X:],[:X,Y:] st U = dom f & f is_differentiable_on U & I is one-to-one & I is onto & I is isometric & ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( partdiff`1 (f,u) = partdiff`2 ((f * I),v) & partdiff`2 (f,u) = partdiff`1 ((f * I),v) ) by Th11;

for f being PartFunc of [:X,Y:],Z

for U being Subset of [:X,Y:]

for I being LinearOperator of [:Y,X:],[:X,Y:] st U = dom f & f is_differentiable_on U & I is one-to-one & I is onto & I is isometric & ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( partdiff`1 (f,u) = partdiff`2 ((f * I),v) & partdiff`2 (f,u) = partdiff`1 ((f * I),v) ) by Th11;

theorem Th14: :: NDIFF10:14

for F being RealNormSpace

for G, E being non trivial RealBanachSpace

for Z being Subset of [:E,F:]

for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] 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] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = c ) ) & ( 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) = c & f . (x2,y) = c 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) = c ) & 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 (f,z))) * (partdiff`2 (f,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 (f,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

f . ((g1 . y),y) = c ) & 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) = c ) holds

g1 = g2 ) )

for G, E being non trivial RealBanachSpace

for Z being Subset of [:E,F:]

for f being PartFunc of [:E,F:],G

for a being Point of E

for b being Point of F

for c being Point of G

for z being Point of [:E,F:] 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] & partdiff`1 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] 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) = c ) ) & ( 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) = c & f . (x2,y) = c 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) = c ) & 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 (f,z))) * (partdiff`2 (f,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 (f,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

f . ((g1 . y),y) = c ) & 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) = c ) holds

g1 = g2 ) )

proof end;

theorem Th15: :: NDIFF10:15

for E, F being non trivial RealBanachSpace

for D being Subset of E

for f being PartFunc of E,F

for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

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

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

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

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

for D being Subset of E

for f being PartFunc of E,F

for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

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

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

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

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

proof end;

theorem Th16: :: NDIFF10:16

for E, F being non trivial RealBanachSpace

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 ) )

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 ) )

proof end;

theorem Th17: :: NDIFF10:17

for E, F being non trivial RealBanachSpace

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 A being Subset of E ex B being Subset of F ex g being PartFunc of F,E st

( A is open & B is open & A c= dom f & a in A & b in B & f .: A = B & dom g = B & rng g = A & dom (f | A) = A & rng (f | A) = B & f | A is one-to-one & g is one-to-one & g = (f | A) " & f | A = g " & g . b = a & g is_continuous_on B & g is_differentiable_on B & g `| B is_continuous_on B & ( for y being Point of F st y in B holds

diff (f,(g /. y)) is invertible ) & ( for y being Point of F st y in B holds

diff (g,y) = Inv (diff (f,(g /. y))) ) )

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 A being Subset of E ex B being Subset of F ex g being PartFunc of F,E st

( A is open & B is open & A c= dom f & a in A & b in B & f .: A = B & dom g = B & rng g = A & dom (f | A) = A & rng (f | A) = B & f | A is one-to-one & g is one-to-one & g = (f | A) " & f | A = g " & g . b = a & g is_continuous_on B & g is_differentiable_on B & g `| B is_continuous_on B & ( for y being Point of F st y in B holds

diff (f,(g /. y)) is invertible ) & ( for y being Point of F st y in B holds

diff (g,y) = Inv (diff (f,(g /. y))) ) )

proof end;

theorem Th18: :: NDIFF10:18

for E, F being non trivial RealBanachSpace

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

for r1 being Real st 0 < r1 holds

ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )

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

for r1 being Real st 0 < r1 holds

ex r2 being Real st

( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )

proof end;

theorem :: NDIFF10:19

for E, F being non trivial RealBanachSpace

for Z being Subset of E

for f being PartFunc of E,F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & ( for x being Point of E st x in Z holds

diff (f,x) is invertible ) holds

( ( for x being Point of E

for r1 being Real st x in Z & 0 < r1 holds

ex y being Point of F ex r2 being Real st

( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) ) & f .: Z is open )

for Z being Subset of E

for f being PartFunc of E,F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & ( for x being Point of E st x in Z holds

diff (f,x) is invertible ) holds

( ( for x being Point of E

for r1 being Real st x in Z & 0 < r1 holds

ex y being Point of F ex r2 being Real st

( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) ) & f .: Z is open )

proof end;