:: Isometric Differentiable Functions on Real Normed Space
:: by Yuichi Futa , Noboru Endou and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


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

theorem FX1: :: NDIFF_7:1
for X being set
for I, f being Function holds (f | X) * I = (f * I) | (I " X)
proof end;

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)
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) )
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
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
proof end;

definition
let X, Y be RealNormSpace;
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
ex b1 being Function of X,[:X,Y:] st
for r being Element of X holds b1 . r = [r,(x `2)]
proof end;
uniqueness
for b1, b2 being Function of X,[:X,Y:] st ( for r being Element of X holds b1 . r = [r,(x `2)] ) & ( for r being Element of X holds b2 . r = [r,(x `2)] ) holds
b1 = b2
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
ex b1 being Function of Y,[:X,Y:] st
for r being Element of Y holds b1 . r = [(x `1),r]
proof end;
uniqueness
for b1, b2 being Function of Y,[:X,Y:] st ( for r being Element of Y holds b1 . r = [(x `1),r] ) & ( for r being Element of Y holds b2 . r = [(x `1),r] ) holds
b1 = b2
proof end;
end;

:: deftheorem Defrep1 defines reproj1 NDIFF_7:def 1 :
for X, Y being RealNormSpace
for x being Element of [:X,Y:]
for b4 being Function of X,[:X,Y:] holds
( b4 = reproj1 x iff for r being Element of X holds b4 . r = [r,(x `2)] );

:: deftheorem Defrep2 defines reproj2 NDIFF_7:def 2 :
for X, Y being RealNormSpace
for x being Element of [:X,Y:]
for b4 being Function of Y,[:X,Y:] holds
( b4 = reproj2 x iff for r being Element of Y holds b4 . r = [(x `1),r] );

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
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.|| )
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
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 )
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) )
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 )
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 )
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 )
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 )
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 )
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 )
proof end;

definition
let X, Y be RealNormSpace;
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
ex b1 being LinearOperator of [:X,Y:],(product <*X,Y*>) st
for x being Point of X
for y being Point of Y holds b1 . (x,y) = <*x,y*>
proof end;
uniqueness
for b1, b2 being LinearOperator of [:X,Y:],(product <*X,Y*>) st ( for x being Point of X
for y being Point of Y holds b1 . (x,y) = <*x,y*> ) & ( for x being Point of X
for y being Point of Y holds b2 . (x,y) = <*x,y*> ) holds
b1 = b2
proof end;
end;

:: deftheorem defISO defines IsoCPNrSP NDIFF_7:def 3 :
for X, Y being RealNormSpace
for b3 being LinearOperator of [:X,Y:],(product <*X,Y*>) holds
( b3 = IsoCPNrSP (X,Y) iff for x being Point of X
for y being Point of Y holds b3 . (x,y) = <*x,y*> );

theorem ZeZe: :: NDIFF_7:17
for X, Y being RealNormSpace holds 0. (product <*X,Y*>) = (IsoCPNrSP (X,Y)) . (0. [:X,Y:])
proof end;

registration
let X, Y be RealNormSpace;
cluster IsoCPNrSP (X,Y) -> one-to-one onto isometric ;
correctness
coherence
( IsoCPNrSP (X,Y) is one-to-one & IsoCPNrSP (X,Y) is onto & IsoCPNrSP (X,Y) is isometric )
;
proof end;
end;

registration
let X, Y be RealNormSpace;
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 Element of bool [: the carrier of [:X,Y:], the carrier of (product <*X,Y*>):];
correctness
existence
ex b1 being LinearOperator of [:X,Y:],(product <*X,Y*>) st
( b1 is one-to-one & b1 is onto & b1 is isometric )
;
proof end;
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:]
;
proof end;
end;

registration
let X, Y be RealNormSpace;
let f be one-to-one onto isometric LinearOperator of [:X,Y:],(product <*X,Y*>);
cluster f " -> one-to-one onto isometric for LinearOperator of (product <*X,Y*>),[:X,Y:];
correctness
coherence
for b1 being LinearOperator of (product <*X,Y*>),[:X,Y:] st b1 = f " holds
( b1 is one-to-one & b1 is onto & b1 is isometric )
;
proof end;
end;

registration
let X, Y be RealNormSpace;
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 Element of bool [: the carrier of (product <*X,Y*>), the carrier of [:X,Y:]:];
correctness
existence
ex b1 being LinearOperator of (product <*X,Y*>),[:X,Y:] st
( b1 is one-to-one & b1 is onto & b1 is isometric )
;
proof end;
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]
proof end;

theorem defISOA2: :: NDIFF_7:19
for X, Y being RealNormSpace holds ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) = 0. [: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;

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;

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.||
proof end;

registration
let S, T be RealNormSpace;
cluster Function-like quasi_total V152(S,T) V153(S,T) isometric -> Lipschitzian for Element of bool [: the carrier of S, the carrier of T:];
coherence
for b1 being LinearOperator of S,T st b1 is isometric holds
b1 is Lipschitzian
proof end;
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)) )
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)) )
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)) )
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 )
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 )
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 )
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 )
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)) ")
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)) ") ")
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))) )
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
;
proof end;
:: original: `2
redefine func z `2 -> Point of Y;
correctness
coherence
z `2 is Point of Y
;
proof end;
end;

definition
let X, Y, W be RealNormSpace;
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 ;
pred f is_partial_differentiable_in`2 z means :: NDIFF_7:def 5
f * (reproj2 z) is_differentiable_in z `2 ;
end;

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

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

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) )
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 ) )
proof end;

definition
let X, Y, W be RealNormSpace;
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)) 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)) is Point of (R_NormSpace_of_BoundedLinearOperators (Y,W))
;
end;

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

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

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) )
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)) )
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)) )
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)) )
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)) )
proof end;

definition
let X, Y, W be RealNormSpace;
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 ) );
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 ) );
end;

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

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

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 ) )
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 ;
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
ex b1 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st
( dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`1 (f,z) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`1 (f,z) ) & dom b2 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b2 /. z = partdiff`1 (f,z) ) holds
b1 = b2
proof end;
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 b6 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) holds
( b6 = f `partial`1| Z iff ( dom b6 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b6 /. z = partdiff`1 (f,z) ) ) );

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 ;
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
ex b1 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st
( dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`2 (f,z) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`2 (f,z) ) & dom b2 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b2 /. z = partdiff`2 (f,z) ) holds
b1 = b2
proof end;
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 b6 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) holds
( b6 = f `partial`2| Z iff ( dom b6 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b6 /. z = partdiff`2 (f,z) ) ) );

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))
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))
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 ) ) )
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 ) ) )
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) )
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) )
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) )
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) )
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) )
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) )
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 )
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 ) )
proof end;