:: by Yuichi Futa , Noboru Endou and Yasunari Shidama

::

:: Received December 31, 2013

:: Copyright (c) 2013-2018 Association of Mizar Users

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem LM001: :: NDIFF_7:2

for S, T being RealNormSpace

for L being LinearOperator of S,T

for x, y being Point of S holds (L . x) - (L . y) = L . (x - y)

for L being LinearOperator of S,T

for x, y being Point of S holds (L . x) - (L . y) = L . (x - y)

proof end;

theorem Th26: :: NDIFF_7:3

for X, Y, W being RealNormSpace

for I being Function of X,Y

for f1, f2 being PartFunc of Y,W holds

( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )

for I being Function of X,Y

for f1, f2 being PartFunc of Y,W holds

( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )

proof end;

theorem Th27: :: NDIFF_7:4

for X, Y, W being RealNormSpace

for I being Function of X,Y

for f being PartFunc of Y,W

for r being Real holds r (#) (f * I) = (r (#) f) * I

for I being Function of X,Y

for f being PartFunc of Y,W

for r being Real holds r (#) (f * I) = (r (#) f) * I

proof end;

theorem LM030: :: NDIFF_7:5

for S, T, W being RealNormSpace

for f being PartFunc of T,W

for g being Function of S,T

for x being Point of S st x in dom g & g /. x in dom f & g is_continuous_in x & f is_continuous_in g /. x holds

f * g is_continuous_in x

for f being PartFunc of T,W

for g being Function of S,T

for x being Point of S st x in dom g & g /. x in dom f & g is_continuous_in x & f is_continuous_in g /. x holds

f * g is_continuous_in x

proof end;

definition

let X, Y be RealNormSpace;

let x be Element of [:X,Y:];

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

for r being Element of X holds b_{1} . r = [r,(x `2)]

for b_{1}, b_{2} being Function of X,[:X,Y:] st ( for r being Element of X holds b_{1} . r = [r,(x `2)] ) & ( for r being Element of X holds b_{2} . r = [r,(x `2)] ) holds

b_{1} = b_{2}

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

for r being Element of Y holds b_{1} . r = [(x `1),r]

for b_{1}, b_{2} being Function of Y,[:X,Y:] st ( for r being Element of Y holds b_{1} . r = [(x `1),r] ) & ( for r being Element of Y holds b_{2} . r = [(x `1),r] ) holds

b_{1} = b_{2}

end;
let x be Element of [:X,Y:];

func reproj1 x -> Function of X,[:X,Y:] means :Defrep1: :: NDIFF_7:def 1

for r being Element of X holds it . r = [r,(x `2)];

existence for r being Element of X holds it . r = [r,(x `2)];

ex b

for r being Element of X holds b

proof end;

uniqueness for b

b

proof end;

func reproj2 x -> Function of Y,[:X,Y:] means :Defrep2: :: NDIFF_7:def 2

for r being Element of Y holds it . r = [(x `1),r];

existence for r being Element of Y holds it . r = [(x `1),r];

ex b

for r being Element of Y holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Defrep1 defines reproj1 NDIFF_7:def 1 :

for X, Y being RealNormSpace

for x being Element of [:X,Y:]

for b_{4} being Function of X,[:X,Y:] holds

( b_{4} = reproj1 x iff for r being Element of X holds b_{4} . r = [r,(x `2)] );

for X, Y being RealNormSpace

for x being Element of [:X,Y:]

for b

( b

:: deftheorem Defrep2 defines reproj2 NDIFF_7:def 2 :

for X, Y being RealNormSpace

for x being Element of [:X,Y:]

for b_{4} being Function of Y,[:X,Y:] holds

( b_{4} = reproj2 x iff for r being Element of Y holds b_{4} . r = [(x `1),r] );

for X, Y being RealNormSpace

for x being Element of [:X,Y:]

for b

( b

theorem LM010: :: NDIFF_7:6

for S, T being RealNormSpace

for I being LinearOperator of S,T

for x being Point of S st I is isometric holds

I is_continuous_in x

for I being LinearOperator of S,T

for x being Point of S st I is isometric holds

I is_continuous_in x

proof end;

theorem LMMAZU: :: NDIFF_7:7

for S, T being RealNormSpace

for f being LinearOperator of S,T holds

( f is isometric iff for x being Element of S holds ||.(f . x).|| = ||.x.|| )

for f being LinearOperator of S,T holds

( f is isometric iff for x being Element of S holds ||.(f . x).|| = ||.x.|| )

proof end;

theorem LM015: :: NDIFF_7:8

for S, T being RealNormSpace

for I being LinearOperator of S,T

for Z being Subset of S st I is isometric holds

I is_continuous_on Z

for I being LinearOperator of S,T

for Z being Subset of S st I is isometric holds

I is_continuous_on Z

proof end;

theorem LM020: :: NDIFF_7:9

for S, T being RealNormSpace

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds

ex J being LinearOperator of T,S st

( J = I " & J is one-to-one & J is onto & J is isometric )

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds

ex J being LinearOperator of T,S st

( J = I " & J is one-to-one & J is onto & J is isometric )

proof end;

theorem LM021: :: NDIFF_7:10

for S, T being RealNormSpace

for I being LinearOperator of S,T

for s1 being sequence of S st I is isometric & s1 is convergent holds

( I * s1 is convergent & lim (I * s1) = I . (lim s1) )

for I being LinearOperator of S,T

for s1 being sequence of S st I is isometric & s1 is convergent holds

( I * s1 is convergent & lim (I * s1) = I . (lim s1) )

proof end;

theorem LM022: :: NDIFF_7:11

for S, T being RealNormSpace

for I being LinearOperator of S,T

for s1 being sequence of S st I is one-to-one & I is onto & I is isometric holds

( s1 is convergent iff I * s1 is convergent )

for I being LinearOperator of S,T

for s1 being sequence of S st I is one-to-one & I is onto & I is isometric holds

( s1 is convergent iff I * s1 is convergent )

proof end;

LM023: for S, T being RealNormSpace

for I being LinearOperator of S,T

for Z being Subset of S st I is one-to-one & I is onto & I is isometric & Z is closed holds

I .: Z is closed

proof end;

theorem LM024: :: NDIFF_7:12

for S, T being RealNormSpace

for I being LinearOperator of S,T

for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds

( Z is closed iff I .: Z is closed )

for I being LinearOperator of S,T

for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds

( Z is closed iff I .: Z is closed )

proof end;

theorem LM025: :: NDIFF_7:13

for S, T being RealNormSpace

for I being LinearOperator of S,T

for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds

( Z is open iff I .: Z is open )

for I being LinearOperator of S,T

for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds

( Z is open iff I .: Z is open )

proof end;

LM026: for S, T being RealNormSpace

for I being LinearOperator of S,T

for Z being Subset of S st I is isometric & Z is compact holds

I .: Z is compact

proof end;

theorem :: NDIFF_7:14

for S, T being RealNormSpace

for I being LinearOperator of S,T

for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds

( Z is compact iff I .: Z is compact )

for I being LinearOperator of S,T

for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds

( Z is compact iff I .: Z is compact )

proof end;

theorem LM040: :: NDIFF_7:15

for S, T, W being RealNormSpace

for f being PartFunc of T,W

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds

for x being Point of S st I . x in dom f holds

( f * I is_continuous_in x iff f is_continuous_in I . x )

for f being PartFunc of T,W

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds

for x being Point of S st I . x in dom f holds

( f * I is_continuous_in x iff f is_continuous_in I . x )

proof end;

theorem LM045: :: NDIFF_7:16

for S, T, W being RealNormSpace

for f being PartFunc of T,W

for I being LinearOperator of S,T

for X being set st X c= the carrier of T & I is one-to-one & I is onto & I is isometric holds

( f is_continuous_on X iff f * I is_continuous_on I " X )

for f being PartFunc of T,W

for I being LinearOperator of S,T

for X being set st X c= the carrier of T & I is one-to-one & I is onto & I is isometric holds

( f is_continuous_on X iff f * I is_continuous_on I " X )

proof end;

definition

let X, Y be RealNormSpace;

ex b_{1} being LinearOperator of [:X,Y:],(product <*X,Y*>) st

for x being Point of X

for y being Point of Y holds b_{1} . (x,y) = <*x,y*>

for b_{1}, b_{2} being LinearOperator of [:X,Y:],(product <*X,Y*>) st ( for x being Point of X

for y being Point of Y holds b_{1} . (x,y) = <*x,y*> ) & ( for x being Point of X

for y being Point of Y holds b_{2} . (x,y) = <*x,y*> ) holds

b_{1} = b_{2}

end;
func IsoCPNrSP (X,Y) -> LinearOperator of [:X,Y:],(product <*X,Y*>) means :defISO: :: NDIFF_7:def 3

for x being Point of X

for y being Point of Y holds it . (x,y) = <*x,y*>;

existence for x being Point of X

for y being Point of Y holds it . (x,y) = <*x,y*>;

ex b

for x being Point of X

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 defISO defines IsoCPNrSP NDIFF_7:def 3 :

for X, Y being RealNormSpace

for b_{3} being LinearOperator of [:X,Y:],(product <*X,Y*>) holds

( b_{3} = IsoCPNrSP (X,Y) iff for x being Point of X

for y being Point of Y holds b_{3} . (x,y) = <*x,y*> );

for X, Y being RealNormSpace

for b

( b

for y being Point of Y holds b

registration

let X, Y be RealNormSpace;

correctness

coherence

( IsoCPNrSP (X,Y) is one-to-one & IsoCPNrSP (X,Y) is onto & IsoCPNrSP (X,Y) is isometric );

end;
correctness

coherence

( IsoCPNrSP (X,Y) is one-to-one & IsoCPNrSP (X,Y) is onto & IsoCPNrSP (X,Y) is isometric );

proof end;

registration

let X, Y be RealNormSpace;

existence

ex b_{1} being LinearOperator of [:X,Y:],(product <*X,Y*>) st

( b_{1} is one-to-one & b_{1} is onto & b_{1} is isometric );

end;
cluster Relation-like the carrier of [:X,Y:] -defined the carrier of (product <*X,Y*>) -valued non empty Function-like one-to-one total quasi_total onto V152([:X,Y:], product <*X,Y*>) V153([:X,Y:], product <*X,Y*>) isometric for LinearOperator of ,;

correctness existence

ex b

( b

proof end;

definition

let X, Y be RealNormSpace;

let f be one-to-one onto isometric LinearOperator of [:X,Y:],(product <*X,Y*>);

:: original: "

redefine func f " -> LinearOperator of (product <*X,Y*>),[:X,Y:];

correctness

coherence

f " is LinearOperator of (product <*X,Y*>),[:X,Y:];

end;
let f be one-to-one onto isometric LinearOperator of [:X,Y:],(product <*X,Y*>);

:: original: "

redefine func f " -> LinearOperator of (product <*X,Y*>),[:X,Y:];

correctness

coherence

f " is LinearOperator of (product <*X,Y*>),[:X,Y:];

proof end;

registration

let X, Y be RealNormSpace;

let f be one-to-one onto isometric LinearOperator of [:X,Y:],(product <*X,Y*>);

correctness

coherence

for b_{1} being LinearOperator of (product <*X,Y*>),[:X,Y:] st b_{1} = f " holds

( b_{1} is one-to-one & b_{1} is onto & b_{1} is isometric );

end;
let f be one-to-one onto isometric LinearOperator of [:X,Y:],(product <*X,Y*>);

correctness

coherence

for b

( b

proof end;

registration

let X, Y be RealNormSpace;

existence

ex b_{1} being LinearOperator of (product <*X,Y*>),[:X,Y:] st

( b_{1} is one-to-one & b_{1} is onto & b_{1} is isometric );

end;
cluster Relation-like the carrier of (product <*X,Y*>) -defined the carrier of [:X,Y:] -valued non empty Function-like one-to-one total quasi_total onto V152( product <*X,Y*>,[:X,Y:]) V153( product <*X,Y*>,[:X,Y:]) isometric for LinearOperator of ,;

correctness existence

ex b

( b

proof end;

theorem defISOA1: :: NDIFF_7:18

for X, Y being RealNormSpace

for x being Point of X

for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]

for x being Point of X

for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]

proof end;

theorem :: NDIFF_7:20

for X, Y being RealNormSpace

for Z being Subset of [:X,Y:] holds IsoCPNrSP (X,Y) is_continuous_on Z by LM015;

for Z being Subset of [:X,Y:] holds IsoCPNrSP (X,Y) is_continuous_on Z by LM015;

theorem :: NDIFF_7:21

for X, Y being RealNormSpace

for Z being Subset of (product <*X,Y*>) holds (IsoCPNrSP (X,Y)) " is_continuous_on Z by LM015;

for Z being Subset of (product <*X,Y*>) holds (IsoCPNrSP (X,Y)) " is_continuous_on Z by LM015;

theorem LMX00: :: NDIFF_7:22

for S, T, W being RealNormSpace

for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,W))

for g being Point of (R_NormSpace_of_BoundedLinearOperators (T,W))

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric & f = g * I holds

||.f.|| = ||.g.||

for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,W))

for g being Point of (R_NormSpace_of_BoundedLinearOperators (T,W))

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric & f = g * I holds

||.f.|| = ||.g.||

proof end;

registration

let S, T be RealNormSpace;

for b_{1} being LinearOperator of S,T st b_{1} is isometric holds

b_{1} is Lipschitzian

end;
cluster Function-like quasi_total V152(S,T) V153(S,T) isometric -> Lipschitzian for LinearOperator of ,;

coherence for b

b

proof end;

theorem :: NDIFF_7:23

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f, g being PartFunc of (product G),F

for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds

( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) )

for F being RealNormSpace

for i being set

for f, g being PartFunc of (product G),F

for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds

( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) )

proof end;

theorem :: NDIFF_7:24

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f, g being PartFunc of (product G),F

for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds

( f - g is_partial_differentiable_on X,i & (f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i)) )

for F being RealNormSpace

for i being set

for f, g being PartFunc of (product G),F

for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds

( f - g is_partial_differentiable_on X,i & (f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i)) )

proof end;

theorem :: NDIFF_7:25

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for r being Real

for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds

( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for r being Real

for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds

( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )

proof end;

theorem LM090: :: NDIFF_7:26

for S, T being RealNormSpace

for L being Lipschitzian LinearOperator of S,T

for x0 being Point of S holds

( L is_differentiable_in x0 & diff (L,x0) = L )

for L being Lipschitzian LinearOperator of S,T

for x0 being Point of S holds

( L is_differentiable_in x0 & diff (L,x0) = L )

proof end;

theorem LM120: :: NDIFF_7:27

for S, T, W being RealNormSpace

for f being PartFunc of T,W

for I being Lipschitzian LinearOperator of S,T

for I0 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st I0 = I holds

for x being Point of S st f is_differentiable_in I . x holds

( f * I is_differentiable_in x & diff ((f * I),x) = (diff (f,(I . x))) * I0 )

for f being PartFunc of T,W

for I being Lipschitzian LinearOperator of S,T

for I0 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st I0 = I holds

for x being Point of S st f is_differentiable_in I . x holds

( f * I is_differentiable_in x & diff ((f * I),x) = (diff (f,(I . x))) * I0 )

proof end;

theorem LM150: :: NDIFF_7:28

for S, T, W being RealNormSpace

for f being PartFunc of T,W

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds

for x being Point of S holds

( f * I is_differentiable_in x iff f is_differentiable_in I . x )

for f being PartFunc of T,W

for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds

for x being Point of S holds

( f * I is_differentiable_in x iff f is_differentiable_in I . x )

proof end;

theorem LM155: :: NDIFF_7:29

for S, T, W being RealNormSpace

for f being PartFunc of T,W

for I being LinearOperator of S,T

for X being set st X c= the carrier of T & I is one-to-one & I is onto & I is isometric holds

( f is_differentiable_on X iff f * I is_differentiable_on I " X )

for f being PartFunc of T,W

for I being LinearOperator of S,T

for X being set st X c= the carrier of T & I is one-to-one & I is onto & I is isometric holds

( f is_differentiable_on X iff f * I is_differentiable_on I " X )

proof end;

theorem :: NDIFF_7:30

for W, X, Y being RealNormSpace

for f being PartFunc of (product <*X,Y*>),W

for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds

for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds

(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")

for f being PartFunc of (product <*X,Y*>),W

for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds

for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds

(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")

proof end;

theorem LM166: :: NDIFF_7:31

for W, X, Y being RealNormSpace

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

for D being Subset of [:X,Y:] st f is_differentiable_on D holds

for z being Point of [:X,Y:] st z in dom (f `| D) holds

(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")

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

for D being Subset of [:X,Y:] st f is_differentiable_on D holds

for z being Point of [:X,Y:] st z in dom (f `| D) holds

(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")

proof end;

theorem LM180: :: NDIFF_7:32

for X, Y being RealNormSpace

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

( reproj1 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) & reproj2 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) )

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

( reproj1 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) & reproj2 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) )

proof end;

definition

let X, Y be RealNormSpace;

let z be Point of [:X,Y:];

:: original: `1

redefine func z `1 -> Point of X;

correctness

coherence

z `1 is Point of X;

redefine func z `2 -> Point of Y;

correctness

coherence

z `2 is Point of Y;

end;
let z be Point of [:X,Y:];

:: original: `1

redefine func z `1 -> Point of X;

correctness

coherence

z `1 is Point of X;

proof end;

:: original: `2redefine func z `2 -> Point of Y;

correctness

coherence

z `2 is Point of Y;

proof end;

definition

let X, Y, W be RealNormSpace;

let z be Point of [:X,Y:];

let f be PartFunc of [:X,Y:],W;

end;
let z be Point of [:X,Y:];

let f be PartFunc of [:X,Y:],W;

pred f is_partial_differentiable_in`1 z means :: NDIFF_7:def 4

f * (reproj1 z) is_differentiable_in z `1 ;

f * (reproj1 z) is_differentiable_in z `1 ;

pred f is_partial_differentiable_in`2 z means :: NDIFF_7:def 5

f * (reproj2 z) is_differentiable_in z `2 ;

f * (reproj2 z) is_differentiable_in z `2 ;

:: deftheorem defines is_partial_differentiable_in`1 NDIFF_7:def 4 :

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_in`1 z iff f * (reproj1 z) is_differentiable_in z `1 );

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_in`1 z iff f * (reproj1 z) is_differentiable_in z `1 );

:: deftheorem defines is_partial_differentiable_in`2 NDIFF_7:def 5 :

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_in`2 z iff f * (reproj2 z) is_differentiable_in z `2 );

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_in`2 z iff f * (reproj2 z) is_differentiable_in z `2 );

theorem LM190: :: NDIFF_7:33

for X, Y being RealNormSpace

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

( z `1 = (proj (In (1,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) & z `2 = (proj (In (2,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) )

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

( z `1 = (proj (In (1,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) & z `2 = (proj (In (2,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) )

proof end;

theorem LM200: :: NDIFF_7:34

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds

( ( f is_partial_differentiable_in`1 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies f is_partial_differentiable_in`1 z ) & ( f is_partial_differentiable_in`2 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies f is_partial_differentiable_in`2 z ) )

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

for f being PartFunc of [:X,Y:],W holds

( ( f is_partial_differentiable_in`1 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies f is_partial_differentiable_in`1 z ) & ( f is_partial_differentiable_in`2 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies f is_partial_differentiable_in`2 z ) )

proof end;

definition

let X, Y, W be RealNormSpace;

let z be Point of [:X,Y:];

let f be PartFunc of [:X,Y:],W;

diff ((f * (reproj1 z)),(z `1)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,W)) ;

diff ((f * (reproj2 z)),(z `2)) is Point of (R_NormSpace_of_BoundedLinearOperators (Y,W)) ;

end;
let z be Point of [:X,Y:];

let f be PartFunc of [:X,Y:],W;

func partdiff`1 (f,z) -> Point of (R_NormSpace_of_BoundedLinearOperators (X,W)) equals :: NDIFF_7:def 6

diff ((f * (reproj1 z)),(z `1));

coherence diff ((f * (reproj1 z)),(z `1));

diff ((f * (reproj1 z)),(z `1)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,W)) ;

func partdiff`2 (f,z) -> Point of (R_NormSpace_of_BoundedLinearOperators (Y,W)) equals :: NDIFF_7:def 7

diff ((f * (reproj2 z)),(z `2));

coherence diff ((f * (reproj2 z)),(z `2));

diff ((f * (reproj2 z)),(z `2)) is Point of (R_NormSpace_of_BoundedLinearOperators (Y,W)) ;

:: deftheorem defines partdiff`1 NDIFF_7:def 6 :

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds partdiff`1 (f,z) = diff ((f * (reproj1 z)),(z `1));

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds partdiff`1 (f,z) = diff ((f * (reproj1 z)),(z `1));

:: deftheorem defines partdiff`2 NDIFF_7:def 7 :

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds partdiff`2 (f,z) = diff ((f * (reproj2 z)),(z `2));

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds partdiff`2 (f,z) = diff ((f * (reproj2 z)),(z `2));

theorem LM210: :: NDIFF_7:35

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds

( partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) & partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) )

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

for f being PartFunc of [:X,Y:],W holds

( partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) & partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) )

proof end;

theorem LM215: :: NDIFF_7:36

for X, Y, W being RealNormSpace

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

for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`1 z & f2 is_partial_differentiable_in`1 z holds

( f1 + f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 + f2),z) = (partdiff`1 (f1,z)) + (partdiff`1 (f2,z)) & f1 - f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 - f2),z) = (partdiff`1 (f1,z)) - (partdiff`1 (f2,z)) )

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

for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`1 z & f2 is_partial_differentiable_in`1 z holds

( f1 + f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 + f2),z) = (partdiff`1 (f1,z)) + (partdiff`1 (f2,z)) & f1 - f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 - f2),z) = (partdiff`1 (f1,z)) - (partdiff`1 (f2,z)) )

proof end;

theorem LM216: :: NDIFF_7:37

for X, Y, W being RealNormSpace

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

for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z holds

( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )

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

for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z holds

( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )

proof end;

theorem LM217: :: NDIFF_7:38

for X, Y, W being RealNormSpace

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

for r being Real

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`1 z holds

( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )

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

for r being Real

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`1 z holds

( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )

proof end;

theorem LM218: :: NDIFF_7:39

for X, Y, W being RealNormSpace

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

for r being Real

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`2 z holds

( r (#) f is_partial_differentiable_in`2 z & partdiff`2 ((r (#) f),z) = r * (partdiff`2 (f,z)) )

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

for r being Real

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`2 z holds

( r (#) f is_partial_differentiable_in`2 z & partdiff`2 ((r (#) f),z) = r * (partdiff`2 (f,z)) )

proof end;

definition

let X, Y, W be RealNormSpace;

let Z be set ;

let f be PartFunc of [:X,Y:],W;

end;
let Z be set ;

let f be PartFunc of [:X,Y:],W;

pred f is_partial_differentiable_on`1 Z means :: NDIFF_7:def 8

( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`1 z ) );

( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`1 z ) );

pred f is_partial_differentiable_on`2 Z means :: NDIFF_7:def 9

( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`2 z ) );

( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`2 z ) );

:: deftheorem defines is_partial_differentiable_on`1 NDIFF_7:def 8 :

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_on`1 Z iff ( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`1 z ) ) );

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_on`1 Z iff ( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`1 z ) ) );

:: deftheorem defines is_partial_differentiable_on`2 NDIFF_7:def 9 :

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`2 z ) ) );

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W holds

( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds

f | Z is_partial_differentiable_in`2 z ) ) );

theorem LM300: :: NDIFF_7:40

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W holds

( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )

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

for f being PartFunc of [:X,Y:],W holds

( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )

proof end;

definition

let X, Y, W be RealNormSpace;

let Z be set ;

let f be PartFunc of [:X,Y:],W;

assume A2: f is_partial_differentiable_on`1 Z ;

ex b_{1} being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st

( dom b_{1} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{1} /. z = partdiff`1 (f,z) ) )

for b_{1}, b_{2} being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st dom b_{1} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{1} /. z = partdiff`1 (f,z) ) & dom b_{2} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{2} /. z = partdiff`1 (f,z) ) holds

b_{1} = b_{2}

end;
let Z be set ;

let f be PartFunc of [:X,Y:],W;

assume A2: f is_partial_differentiable_on`1 Z ;

func f `partial`1| Z -> PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) means :Def91: :: NDIFF_7:def 10

( dom it = Z & ( for z being Point of [:X,Y:] st z in Z holds

it /. z = partdiff`1 (f,z) ) );

existence ( dom it = Z & ( for z being Point of [:X,Y:] st z in Z holds

it /. z = partdiff`1 (f,z) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def91 defines `partial`1| NDIFF_7:def 10 :

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds

for b_{6} being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) holds

( b_{6} = f `partial`1| Z iff ( dom b_{6} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{6} /. z = partdiff`1 (f,z) ) ) );

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds

for b

( b

b

definition

let X, Y, W be RealNormSpace;

let Z be set ;

let f be PartFunc of [:X,Y:],W;

assume A2: f is_partial_differentiable_on`2 Z ;

ex b_{1} being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st

( dom b_{1} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{1} /. z = partdiff`2 (f,z) ) )

for b_{1}, b_{2} being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st dom b_{1} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{1} /. z = partdiff`2 (f,z) ) & dom b_{2} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{2} /. z = partdiff`2 (f,z) ) holds

b_{1} = b_{2}

end;
let Z be set ;

let f be PartFunc of [:X,Y:],W;

assume A2: f is_partial_differentiable_on`2 Z ;

func f `partial`2| Z -> PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) means :Def92: :: NDIFF_7:def 11

( dom it = Z & ( for z being Point of [:X,Y:] st z in Z holds

it /. z = partdiff`2 (f,z) ) );

existence ( dom it = Z & ( for z being Point of [:X,Y:] st z in Z holds

it /. z = partdiff`2 (f,z) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def92 defines `partial`2| NDIFF_7:def 11 :

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds

for b_{6} being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) holds

( b_{6} = f `partial`2| Z iff ( dom b_{6} = Z & ( for z being Point of [:X,Y:] st z in Z holds

b_{6} /. z = partdiff`2 (f,z) ) ) );

for X, Y, W being RealNormSpace

for Z being set

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds

for b

( b

b

theorem LM400: :: NDIFF_7:41

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds

f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))

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

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds

f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))

proof end;

theorem LM401: :: NDIFF_7:42

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds

f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))

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

for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds

f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))

proof end;

theorem NDIFF5241: :: NDIFF_7:43

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W st Z is open holds

( f is_partial_differentiable_on`1 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds

f is_partial_differentiable_in`1 x ) ) )

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

for f being PartFunc of [:X,Y:],W st Z is open holds

( f is_partial_differentiable_on`1 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds

f is_partial_differentiable_in`1 x ) ) )

proof end;

theorem NDIFF5242: :: NDIFF_7:44

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W st Z is open holds

( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds

f is_partial_differentiable_in`2 x ) ) )

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

for f being PartFunc of [:X,Y:],W st Z is open holds

( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds

f is_partial_differentiable_in`2 x ) ) )

proof end;

theorem :: NDIFF_7:45

for X, Y, W being RealNormSpace

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds

( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) )

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds

( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) )

proof end;

theorem :: NDIFF_7:46

for X, Y, W being RealNormSpace

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds

( f - g is_partial_differentiable_on`1 Z & (f - g) `partial`1| Z = (f `partial`1| Z) - (g `partial`1| Z) )

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds

( f - g is_partial_differentiable_on`1 Z & (f - g) `partial`1| Z = (f `partial`1| Z) - (g `partial`1| Z) )

proof end;

theorem :: NDIFF_7:47

for X, Y, W being RealNormSpace

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds

( f + g is_partial_differentiable_on`2 Z & (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z) )

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds

( f + g is_partial_differentiable_on`2 Z & (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z) )

proof end;

theorem :: NDIFF_7:48

for X, Y, W being RealNormSpace

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds

( f - g is_partial_differentiable_on`2 Z & (f - g) `partial`2| Z = (f `partial`2| Z) - (g `partial`2| Z) )

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

for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds

( f - g is_partial_differentiable_on`2 Z & (f - g) `partial`2| Z = (f `partial`2| Z) - (g `partial`2| Z) )

proof end;

theorem :: NDIFF_7:49

for X, Y, W being RealNormSpace

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

for r being Real

for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z holds

( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) )

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

for r being Real

for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z holds

( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) )

proof end;

theorem :: NDIFF_7:50

for X, Y, W being RealNormSpace

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

for r being Real

for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z holds

( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )

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

for r being Real

for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z holds

( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )

proof end;

theorem LMX1: :: NDIFF_7:51

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W st f is_differentiable_on Z holds

( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )

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

for f being PartFunc of [:X,Y:],W st f is_differentiable_on Z holds

( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )

proof end;

theorem :: NDIFF_7:52

for X, Y, W being RealNormSpace

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

for f being PartFunc of [:X,Y:],W st Z is open holds

( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z iff ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) )

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

for f being PartFunc of [:X,Y:],W st Z is open holds

( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z iff ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) )

proof end;