:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama

::

:: Received November 29, 2017

:: Copyright (c) 2017-2021 Association of Mizar Users

theorem LMNR0: :: NDIFF_8:1

for X, Y being RealNormSpace

for x being Point of X

for y being Point of Y

for z being Point of [:X,Y:] st z = [x,y] holds

||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))

for x being Point of X

for y being Point of Y

for z being Point of [:X,Y:] st z = [x,y] holds

||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))

proof end;

theorem LMNR1: :: NDIFF_8:2

for X, Y being RealNormSpace

for x being Point of X

for z being Point of [:X,Y:] st z = [x,(0. Y)] holds

||.z.|| = ||.x.||

for x being Point of X

for z being Point of [:X,Y:] st z = [x,(0. Y)] holds

||.z.|| = ||.x.||

proof end;

theorem :: NDIFF_8:3

for X, Y being RealNormSpace

for y being Point of Y

for z being Point of [:X,Y:] st z = [(0. X),y] holds

||.z.|| = ||.y.||

for y being Point of Y

for z being Point of [:X,Y:] st z = [(0. X),y] holds

||.z.|| = ||.y.||

proof end;

theorem :: NDIFF_8:4

for X, Y, Z, W being RealNormSpace

for f being Lipschitzian LinearOperator of Z,W

for g being Lipschitzian LinearOperator of Y,Z

for h being Lipschitzian LinearOperator of X,Y holds f * (g * h) = (f * g) * h by RELAT_1:36;

for f being Lipschitzian LinearOperator of Z,W

for g being Lipschitzian LinearOperator of Y,Z

for h being Lipschitzian LinearOperator of X,Y holds f * (g * h) = (f * g) * h by RELAT_1:36;

theorem LPB2Th4: :: NDIFF_8:5

for X, Y, Z being RealNormSpace

for g being Lipschitzian LinearOperator of X,Y

for f being Lipschitzian LinearOperator of Y,Z

for h being Lipschitzian LinearOperator of X,Z holds

( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )

for g being Lipschitzian LinearOperator of X,Y

for f being Lipschitzian LinearOperator of Y,Z

for h being Lipschitzian LinearOperator of X,Z holds

( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )

proof end;

theorem LPB2Th6: :: NDIFF_8:6

for X, Y being RealNormSpace

for f being Lipschitzian LinearOperator of X,Y holds

( f * (id the carrier of X) = f & (id the carrier of Y) * f = f )

for f being Lipschitzian LinearOperator of X,Y holds

( f * (id the carrier of X) = f & (id the carrier of Y) * f = f )

proof end;

theorem :: NDIFF_8:7

for X, Y, Z, W being RealNormSpace

for f being Element of BoundedLinearOperators (Z,W)

for g being Element of BoundedLinearOperators (Y,Z)

for h being Element of BoundedLinearOperators (X,Y) holds f * (g * h) = (f * g) * h

for f being Element of BoundedLinearOperators (Z,W)

for g being Element of BoundedLinearOperators (Y,Z)

for h being Element of BoundedLinearOperators (X,Y) holds f * (g * h) = (f * g) * h

proof end;

theorem :: NDIFF_8:8

for X, Y being RealNormSpace

for f being Element of BoundedLinearOperators (X,Y) holds

( f * (FuncUnit X) = f & (FuncUnit Y) * f = f )

for f being Element of BoundedLinearOperators (X,Y) holds

( f * (FuncUnit X) = f & (FuncUnit Y) * f = f )

proof end;

theorem LPB2Th9: :: NDIFF_8:9

for X, Y, Z being RealNormSpace

for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds f * (g + h) = (f * g) + (f * h)

for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds f * (g + h) = (f * g) + (f * h)

proof end;

theorem :: NDIFF_8:10

for X, Y, Z being RealNormSpace

for f being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (g + h) * f = (g * f) + (h * f)

for f being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (g + h) * f = (g * f) + (h * f)

proof end;

theorem LPB2Th11: :: NDIFF_8:11

for X, Y, Z being RealNormSpace

for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)

for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)

proof end;

theorem :: NDIFF_8:12

for X, Y, Z being RealNormSpace

for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds a * (f * g) = (a * f) * g

for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds a * (f * g) = (a * f) * g

proof end;

definition

let M be RealNormSpace;

let p be Element of M;

let r be Real;

coherence

{ q where q is Element of M : ||.(p - q).|| <= r } is Subset of M;

end;
let p be Element of M;

let r be Real;

func cl_Ball (p,r) -> Subset of M equals :: NDIFF_8:def 1

{ q where q is Element of M : ||.(p - q).|| <= r } ;

correctness { q where q is Element of M : ||.(p - q).|| <= r } ;

coherence

{ q where q is Element of M : ||.(p - q).|| <= r } is Subset of M;

proof end;

:: deftheorem defines cl_Ball NDIFF_8:def 1 :

for M being RealNormSpace

for p being Element of M

for r being Real holds cl_Ball (p,r) = { q where q is Element of M : ||.(p - q).|| <= r } ;

for M being RealNormSpace

for p being Element of M

for r being Real holds cl_Ball (p,r) = { q where q is Element of M : ||.(p - q).|| <= r } ;

theorem LMBALL2: :: NDIFF_8:13

for S being RealNormSpace

for p being Element of S

for r being Real st 0 < r holds

( p in Ball (p,r) & p in cl_Ball (p,r) )

for p being Element of S

for r being Real st 0 < r holds

( p in Ball (p,r) & p in cl_Ball (p,r) )

proof end;

theorem :: NDIFF_8:14

theorem LMBALL1: :: NDIFF_8:15

for M being RealNormSpace

for p being Element of M

for r1, r2 being Real st r1 <= r2 holds

( cl_Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= Ball (p,r2) )

for p being Element of M

for r1, r2 being Real st r1 <= r2 holds

( cl_Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= cl_Ball (p,r2) & Ball (p,r1) c= Ball (p,r2) )

proof end;

theorem LMBALL1X: :: NDIFF_8:16

for M being RealNormSpace

for p being Element of M

for r1, r2 being Real st r1 < r2 holds

cl_Ball (p,r1) c= Ball (p,r2)

for p being Element of M

for r1, r2 being Real st r1 < r2 holds

cl_Ball (p,r1) c= Ball (p,r2)

proof end;

theorem LMBALL: :: NDIFF_8:17

for S being RealNormSpace

for p being Element of S

for r being Real holds Ball (p,r) = { y where y is Point of S : ||.(y - p).|| < r }

for p being Element of S

for r being Real holds Ball (p,r) = { y where y is Point of S : ||.(y - p).|| < r }

proof end;

theorem :: NDIFF_8:18

for S being RealNormSpace

for p being Element of S

for r being Real holds cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r }

for p being Element of S

for r being Real holds cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r }

proof end;

theorem :: NDIFF_8:19

for S being RealNormSpace

for p being Element of S

for r being Real st 0 < r holds

Ball (p,r) is Neighbourhood of p

for p being Element of S

for r being Real st 0 < r holds

Ball (p,r) is Neighbourhood of p

proof end;

registration

let X be RealNormSpace;

let x be Point of X;

let r be Real;

coherence

Ball (x,r) is open

cl_Ball (x,r) is closed

end;
let x be Point of X;

let r be Real;

coherence

Ball (x,r) is open

proof end;

coherence cl_Ball (x,r) is closed

proof end;

theorem NORMSP27: :: NDIFF_8:20

for X being RealNormSpace

for V being Subset of X holds

( V is open iff for x being Point of X st x in V holds

ex r being Real st

( r > 0 & Ball (x,r) c= V ) )

for V being Subset of X holds

( V is open iff for x being Point of X st x in V holds

ex r being Real st

( r > 0 & Ball (x,r) c= V ) )

proof end;

theorem NORMSP35: :: NDIFF_8:21

for X, Y being RealNormSpace

for x being Point of X

for y being Point of Y

for z being Point of [:X,Y:] st z = [x,y] holds

( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )

for x being Point of X

for y being Point of Y

for z being Point of [:X,Y:] st z = [x,y] holds

( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )

proof end;

theorem NORMSP31: :: NDIFF_8:22

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 being Real st 0 < r1 & z = [x,y] holds

ex r2 being Real st

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

for x being Point of X

for y being Point of Y

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

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

ex r2 being Real st

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

proof end;

theorem :: NDIFF_8:23

for X, Y being RealNormSpace

for x being Point of X

for y being Point of Y

for V being Subset of [:X,Y:] st V is open & [x,y] in V holds

ex r being Real st

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

for x being Point of X

for y being Point of Y

for V being Subset of [:X,Y:] st V is open & [x,y] in V holds

ex r being Real st

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

proof end;

theorem :: NDIFF_8:24

for X, Y being RealNormSpace

for x being Point of X

for y being Point of Y

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

for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds

V is open

for x being Point of X

for y being Point of Y

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

for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds

V is open

proof end;

theorem LQ2: :: NDIFF_8:25

for E, F being RealNormSpace

for Q being LinearOperator of E,F

for v being Point of E st Q is one-to-one holds

( Q . v = 0. F iff v = 0. E )

for Q being LinearOperator of E,F

for v being Point of E st Q is one-to-one holds

( Q . v = 0. F iff v = 0. E )

proof end;

theorem OP1: :: NDIFF_8:26

for E being RealNormSpace

for X, Y being Subset of E

for v being Point of E st X is open & Y = { (x + v) where x is Point of E : x in X } holds

Y is open

for X, Y being Subset of E

for v being Point of E st X is open & Y = { (x + v) where x is Point of E : x in X } holds

Y is open

proof end;

theorem OP2: :: NDIFF_8:27

for E being RealNormSpace

for X, Y being Subset of E

for v being Point of E st X is open & Y = { (x - v) where x is Point of E : x in X } holds

Y is open

for X, Y being Subset of E

for v being Point of E st X is open & Y = { (x - v) where x is Point of E : x in X } holds

Y is open

proof end;

theorem FIXPOINT: :: NDIFF_8:28

for X being RealBanachSpace

for S being non empty Subset of X

for f being PartFunc of X,X st S is closed & dom f = S & rng f c= S & ex k being Real st

( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds

||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) holds

( ex x0 being Point of X st

( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds

x0 = y0 ) )

for S being non empty Subset of X

for f being PartFunc of X,X st S is closed & dom f = S & rng f c= S & ex k being Real st

( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds

||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) holds

( ex x0 being Point of X st

( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds

x0 = y0 ) )

proof end;

theorem FIXPOINT2: :: NDIFF_8:29

for E being RealNormSpace

for F being RealBanachSpace

for E0 being non empty Subset of E

for F0 being non empty Subset of F

for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E

for y being Point of F st x in E0 & y in F0 holds

Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds

for x0 being Point of E st x0 in E0 holds

for e being Real st 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds

||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st

( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds

for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds

||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds

( ( for x being Point of E st x in E0 holds

( ex y being Point of F st

( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds

y1 = y2 ) ) ) & ( for x0 being Point of E

for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds

for e being Real st 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of E

for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds

||.(y1 - y0).|| < e ) ) ) )

for F being RealBanachSpace

for E0 being non empty Subset of E

for F0 being non empty Subset of F

for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E

for y being Point of F st x in E0 & y in F0 holds

Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds

for x0 being Point of E st x0 in E0 holds

for e being Real st 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds

||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st

( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds

for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds

||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds

( ( for x being Point of E st x in E0 holds

( ex y being Point of F st

( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds

y1 = y2 ) ) ) & ( for x0 being Point of E

for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds

for e being Real st 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of E

for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds

||.(y1 - y0).|| < e ) ) ) )

proof end;

theorem FIXPOINT3: :: NDIFF_8:30

for E being RealNormSpace

for F being RealBanachSpace

for A being non empty Subset of E

for B being non empty Subset of F

for Fai being PartFunc of [:E,F:],F st B is closed & [:A,B:] c= dom Fai & ( for x being Point of E

for y being Point of F st x in A & y in B holds

Fai . (x,y) in B ) & ( for y being Point of F st y in B holds

for x0 being Point of E st x0 in A holds

for e being Real st 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of E st x1 in A & ||.(x1 - x0).|| < d holds

||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st

( 0 < k & k < 1 & ( for x being Point of E st x in A holds

for y1, y2 being Point of F st y1 in B & y2 in B holds

||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds

( ex g being PartFunc of E,F st

( g is_continuous_on A & dom g = A & rng g c= B & ( for x being Point of E st x in A holds

Fai . (x,(g . x)) = g . x ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = A & rng g1 c= B & dom g2 = A & rng g2 c= B & ( for x being Point of E st x in A holds

Fai . (x,(g1 . x)) = g1 . x ) & ( for x being Point of E st x in A holds

Fai . (x,(g2 . x)) = g2 . x ) holds

g1 = g2 ) )

for F being RealBanachSpace

for A being non empty Subset of E

for B being non empty Subset of F

for Fai being PartFunc of [:E,F:],F st B is closed & [:A,B:] c= dom Fai & ( for x being Point of E

for y being Point of F st x in A & y in B holds

Fai . (x,y) in B ) & ( for y being Point of F st y in B holds

for x0 being Point of E st x0 in A holds

for e being Real st 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of E st x1 in A & ||.(x1 - x0).|| < d holds

||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st

( 0 < k & k < 1 & ( for x being Point of E st x in A holds

for y1, y2 being Point of F st y1 in B & y2 in B holds

||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds

( ex g being PartFunc of E,F st

( g is_continuous_on A & dom g = A & rng g c= B & ( for x being Point of E st x in A holds

Fai . (x,(g . x)) = g . x ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = A & rng g1 c= B & dom g2 = A & rng g2 c= B & ( for x being Point of E st x in A holds

Fai . (x,(g1 . x)) = g1 . x ) & ( for x being Point of E st x in A holds

Fai . (x,(g2 . x)) = g2 . x ) holds

g1 = g2 ) )

proof end;

theorem :: NDIFF_8:31

for E, F being RealNormSpace

for s1, s2 being Point of [:E,F:] st s1 `2 = s2 `2 holds

reproj1 s1 = reproj1 s2

for s1, s2 being Point of [:E,F:] st s1 `2 = s2 `2 holds

reproj1 s1 = reproj1 s2

proof end;

theorem REP2: :: NDIFF_8:32

for E, F being RealNormSpace

for s1, s2 being Point of [:E,F:] st s1 `1 = s2 `1 holds

reproj2 s1 = reproj2 s2

for s1, s2 being Point of [:E,F:] st s1 `1 = s2 `1 holds

reproj2 s1 = reproj2 s2

proof end;

theorem LMCLOSE2: :: NDIFF_8:33

for E being RealNormSpace

for r being Real

for z, y1, y2 being Point of E st y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) holds

[.y1,y2.] c= cl_Ball (z,r)

for r being Real

for z, y1, y2 being Point of E st y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) holds

[.y1,y2.] c= cl_Ball (z,r)

proof end;

theorem NEIB1: :: NDIFF_8:34

for E being RealNormSpace

for x, b being Point of E

for N being Neighbourhood of x holds

( { (z - b) where z is Point of E : z in N } is Neighbourhood of x - b & { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b )

for x, b being Point of E

for N being Neighbourhood of x holds

( { (z - b) where z is Point of E : z in N } is Neighbourhood of x - b & { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b )

proof end;

theorem Th1: :: NDIFF_8:35

for E, G being RealNormSpace

for F being 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_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F 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 cl_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 cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds

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

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

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

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

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

g1 = g2 ) )

for F being 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_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F 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 cl_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 cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds

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

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

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

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

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

g1 = g2 ) )

proof end;

theorem :: NDIFF_8:36

for E, G being RealNormSpace

for F being 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_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F 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

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

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

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 F being 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_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F 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

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

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

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;