:: by Kazuhisa Nakasho and Yasunari Shidama

::

:: Received May 27, 2019

:: Copyright (c) 2019 Association of Mizar Users

theorem LMDIFF: :: NDIFF_9:1

for E, F being RealNormSpace

for f being PartFunc of E,F

for Z being Subset of E

for z being Point of E st Z is open & z in Z & Z c= dom f & f is_differentiable_in z holds

( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )

for f being PartFunc of E,F

for Z being Subset of E

for z being Point of E st Z is open & z in Z & Z c= dom f & f is_differentiable_in z holds

( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )

proof end;

theorem LMPDIFF: :: NDIFF_9:2

for E, F, G being RealNormSpace

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

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

for z being Point of [:E,F:] st Z is open & z in Z & Z c= dom f holds

( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )

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

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

for z being Point of [:E,F:] st Z is open & z in Z & Z c= dom f holds

( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )

proof end;

theorem LmTh47: :: NDIFF_9:3

for X, E, G, F being RealNormSpace

for BL being BilinearOperator of E,F,G

for f being PartFunc of X,E

for g being PartFunc of X,F

for S being Subset of X st BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds

f is_continuous_in s ) & ( for s being Point of X st s in S holds

g is_continuous_in s ) holds

ex H being PartFunc of X,G st

( dom H = S & ( for s being Point of X st s in S holds

H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )

for BL being BilinearOperator of E,F,G

for f being PartFunc of X,E

for g being PartFunc of X,F

for S being Subset of X st BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds

f is_continuous_in s ) & ( for s being Point of X st s in S holds

g is_continuous_in s ) holds

ex H being PartFunc of X,G st

( dom H = S & ( for s being Point of X st s in S holds

H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )

proof end;

theorem LmTh471: :: NDIFF_9:4

for E, F being RealNormSpace

for g being PartFunc of E,F

for A being Subset of E st g is_continuous_on A & dom g = A holds

ex xg being PartFunc of E,[:E,F:] st

( dom xg = A & ( for x being Point of E st x in A holds

xg . x = [x,(g . x)] ) & xg is_continuous_on A )

for g being PartFunc of E,F

for A being Subset of E st g is_continuous_on A & dom g = A holds

ex xg being PartFunc of E,[:E,F:] st

( dom xg = A & ( for x being Point of E st x in A holds

xg . x = [x,(g . x)] ) & xg is_continuous_on A )

proof end;

theorem NFCONT112: :: NDIFF_9:5

for S, T, V being RealNormSpace

for x0 being Point of V

for f1 being PartFunc of the carrier of V, the carrier of S

for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds

f2 * f1 is_continuous_in x0

for x0 being Point of V

for f1 being PartFunc of the carrier of V, the carrier of S

for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds

f2 * f1 is_continuous_in x0

proof end;

theorem LM0: :: NDIFF_9:6

for E, F being RealNormSpace

for z being Point of [:E,F:]

for x being Point of E

for y being Point of F st z = [x,y] holds

||.z.|| <= ||.x.|| + ||.y.||

for z being Point of [:E,F:]

for x being Point of E

for y being Point of F st z = [x,y] holds

||.z.|| <= ||.x.|| + ||.y.||

proof end;

theorem Th0: :: NDIFF_9:7

for E, F, G being RealNormSpace

for L being LinearOperator of [:E,F:],G ex L1 being LinearOperator of E,G ex L2 being LinearOperator of F,G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

for L being LinearOperator of [:E,F:],G ex L1 being LinearOperator of E,G ex L2 being LinearOperator of F,G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem Th0X: :: NDIFF_9:8

for E, F, G being RealNormSpace

for L being LinearOperator of [:E,F:],G

for L11 being LinearOperator of E,G

for L12 being LinearOperator of F,G

for L21 being LinearOperator of E,G

for L22 being LinearOperator of F,G st ( for x being Point of E

for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E

for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds

( L11 = L21 & L12 = L22 )

for L being LinearOperator of [:E,F:],G

for L11 being LinearOperator of E,G

for L12 being LinearOperator of F,G

for L21 being LinearOperator of E,G

for L22 being LinearOperator of F,G st ( for x being Point of E

for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E

for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds

( L11 = L21 & L12 = L22 )

proof end;

theorem Th1: :: NDIFF_9:9

for E, F, G being RealNormSpace

for L1 being LinearOperator of E,G

for L2 being LinearOperator of F,G ex L being LinearOperator of [:E,F:],G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

for L1 being LinearOperator of E,G

for L2 being LinearOperator of F,G ex L being LinearOperator of [:E,F:],G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem Th2: :: NDIFF_9:10

for E, F, G being RealNormSpace

for L being Lipschitzian LinearOperator of [:E,F:],G ex L1 being Lipschitzian LinearOperator of E,G ex L2 being Lipschitzian LinearOperator of F,G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

for L being Lipschitzian LinearOperator of [:E,F:],G ex L1 being Lipschitzian LinearOperator of E,G ex L2 being Lipschitzian LinearOperator of F,G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem :: NDIFF_9:11

for E, F, G being RealNormSpace

for L1 being Lipschitzian LinearOperator of E,G

for L2 being Lipschitzian LinearOperator of F,G ex L being Lipschitzian LinearOperator of [:E,F:],G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

for L1 being Lipschitzian LinearOperator of E,G

for L2 being Lipschitzian LinearOperator of F,G ex L being Lipschitzian LinearOperator of [:E,F:],G st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem :: NDIFF_9:12

for E, F, G being RealNormSpace

for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) ex L1 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) ex L2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L . [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L . [(0. E),y] ) & ||.L.|| <= ||.L1.|| + ||.L2.|| & ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.|| )

for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) ex L1 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) ex L2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st

( ( for x being Point of E

for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L . [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L . [(0. E),y] ) & ||.L.|| <= ||.L1.|| + ||.L2.|| & ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.|| )

proof end;

theorem :: NDIFF_9:13

for E, F, G being RealNormSpace

for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))

for L11, L12 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G))

for L21, L22 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st ( for x being Point of E

for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ) & ( for x being Point of E

for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ) holds

( L11 = L12 & L21 = L22 )

for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))

for L11, L12 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G))

for L21, L22 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st ( for x being Point of E

for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ) & ( for x being Point of E

for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ) holds

( L11 = L12 & L21 = L22 )

proof end;

theorem Th4: :: NDIFF_9:14

for E, G, F being RealNormSpace

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

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

for z being Point of [:E,F:] st f is_differentiable_in z holds

( f is_partial_differentiable_in`1 z & f is_partial_differentiable_in`2 z & ( for dx being Point of E

for dy being Point of F holds (diff (f,z)) . [dx,dy] = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy) ) )

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

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

for z being Point of [:E,F:] st f is_differentiable_in z holds

( f is_partial_differentiable_in`1 z & f is_partial_differentiable_in`2 z & ( for dx being Point of E

for dy being Point of F holds (diff (f,z)) . [dx,dy] = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy) ) )

proof end;

theorem Th5: :: NDIFF_9:15

for E, G, F being RealNormSpace

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:]

for r1, r2 being Real

for g being PartFunc of E,F

for P being Lipschitzian LinearOperator of E,G

for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds

f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds

( g is_differentiable_in a & diff (g,a) = - (Q * P) )

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:]

for r1, r2 being Real

for g being PartFunc of E,F

for P being Lipschitzian LinearOperator of E,G

for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds

f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds

( g is_differentiable_in a & diff (g,a) = - (Q * P) )

proof end;

theorem LMTh3: :: NDIFF_9:16

for X, Y being non trivial RealBanachSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

ex K, s being Real st

( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds

( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) )

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

ex K, s being Real st

( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds

( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) )

proof end;

theorem LM80: :: NDIFF_9:17

for X, Y being non trivial RealBanachSpace

for I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st dom I = InvertibleOperators (X,Y) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) holds

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )

for I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st dom I = InvertibleOperators (X,Y) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) holds

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )

proof end;

theorem :: NDIFF_9:18

for X, Y being non trivial RealBanachSpace ex I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st

( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_differentiable_on InvertibleOperators (X,Y) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) st

( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_differentiable_on InvertibleOperators (Y,X) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) & ( for u, du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

(diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )

( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_differentiable_on InvertibleOperators (X,Y) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) st

( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_differentiable_on InvertibleOperators (Y,X) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) & ( for u, du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

(diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )

proof end;

theorem Th45: :: NDIFF_9:19

for E, G, F being RealNormSpace

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:]

for A being Subset of E

for B being Subset of F

for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds

f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds

( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )

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:]

for A being Subset of E

for B being Subset of F

for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds

f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds

( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )

proof end;

theorem Th47: :: NDIFF_9:20

for E being RealNormSpace

for G, F being non trivial RealBanachSpace

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

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

for c being Point of G

for A being Subset of E

for B being Subset of F

for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds

f . (x,(g . x)) = c ) & ( for x being Point of E

for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds

partdiff`2 (f,z) is invertible ) holds

( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E

for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds

diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )

for G, F being non trivial RealBanachSpace

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

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

for c being Point of G

for A being Subset of E

for B being Subset of F

for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds

f . (x,(g . x)) = c ) & ( for x being Point of E

for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds

partdiff`2 (f,z) is invertible ) holds

( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E

for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds

diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )

proof end;

theorem :: NDIFF_9:21

for E being RealNormSpace

for G, F 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`2 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) 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,r1) 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

( 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

f . (x,(g . x)) = c ) & g is_differentiable_on Ball (a,r1) & g `| (Ball (a,r1)) is_continuous_on Ball (a,r1) & ( for x being Point of 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 (f,z))) * (partdiff`1 (f,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 (f,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

f . (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

f . (x,(g2 . x)) = c ) holds

g1 = g2 ) )

for G, F 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`2 (f,z) is invertible holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) 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,r1) 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

( 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

f . (x,(g . x)) = c ) & g is_differentiable_on Ball (a,r1) & g `| (Ball (a,r1)) is_continuous_on Ball (a,r1) & ( for x being Point of 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 (f,z))) * (partdiff`1 (f,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 (f,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

f . (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

f . (x,(g2 . x)) = c ) holds

g1 = g2 ) )

proof end;