:: Partial Differentiation on Normed Linear Spaces $ {\cal R}^n$
:: by Noboru Endou , Yasunari Shidama and Keiichi Miyajima
::
:: Received June 6, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users


definition
let i, n be Nat;
func proj (i,n) -> Function of (REAL n),REAL means :Def1: :: PDIFF_1:def 1
 for x being Element of REAL n holds it . x = x . i;
existence
ex b1 being Function of (REAL n),REAL st
for x being Element of REAL n holds b1 . x = x . i
proof end;
uniqueness
for b1, b2 being Function of (REAL n),REAL st ( for x being Element of REAL n holds b1 . x = x . i ) & ( for x being Element of REAL n holds b2 . x = x . i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines proj PDIFF_1:def 1 :
for i, n being Nat
for b3 being Function of (REAL n),REAL holds
( b3 = proj (i,n) iff for x being Element of REAL n holds b3 . x = x . i );

set W = (proj (1,1)) " ;

Lm1: ( proj (1,1) is bijective & dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
proof end;

Lm2: for i, n being Nat st i in Seg n holds
proj (i,n) is onto
proof end;

theorem :: PDIFF_1:1
( ( for i, n being Nat st i in Seg n holds
( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
proof end;

theorem Th2: :: PDIFF_1:2
( (proj (1,1)) " is Function of REAL,(REAL 1) & (proj (1,1)) " is one-to-one & dom ((proj (1,1)) ") = REAL & rng ((proj (1,1)) ") = REAL 1 & ex g being Function of REAL,(REAL 1) st
( g is bijective & (proj (1,1)) " = g ) )
proof end;

registration
cluster proj (1,1) -> bijective ;
coherence
proj (1,1) is bijective by Lm1;
end;

definition
let g be PartFunc of REAL,REAL;
func <>* g -> PartFunc of (REAL 1),(REAL 1) equals :: PDIFF_1:def 2
(((proj (1,1)) ") * g) * (proj (1,1));
coherence
(((proj (1,1)) ") * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1)
proof end;
end;

:: deftheorem defines <>* PDIFF_1:def 2 :
for g being PartFunc of REAL,REAL holds <>* g = (((proj (1,1)) ") * g) * (proj (1,1));

definition
let n be Nat;
let g be PartFunc of (REAL n),REAL;
func <>* g -> PartFunc of (REAL n),(REAL 1) equals :: PDIFF_1:def 3
((proj (1,1)) ") * g;
correctness
coherence
((proj (1,1)) ") * g is PartFunc of (REAL n),(REAL 1);
proof end;
end;

:: deftheorem defines <>* PDIFF_1:def 3 :
for n being Nat
for g being PartFunc of (REAL n),REAL holds <>* g = ((proj (1,1)) ") * g;

definition
let i, n be Nat;
func Proj (i,n) -> Function of (REAL-NS n),(REAL-NS 1) means :Def4: :: PDIFF_1:def 4
 for x being Point of (REAL-NS n) holds it . x = <*((proj (i,n)) . x)*>;
existence
ex b1 being Function of (REAL-NS n),(REAL-NS 1) st
for x being Point of (REAL-NS n) holds b1 . x = <*((proj (i,n)) . x)*>
proof end;
uniqueness
for b1, b2 being Function of (REAL-NS n),(REAL-NS 1) st ( for x being Point of (REAL-NS n) holds b1 . x = <*((proj (i,n)) . x)*> ) & ( for x being Point of (REAL-NS n) holds b2 . x = <*((proj (i,n)) . x)*> ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Proj PDIFF_1:def 4 :
for i, n being Nat
for b3 being Function of (REAL-NS n),(REAL-NS 1) holds
( b3 = Proj (i,n) iff for x being Point of (REAL-NS n) holds b3 . x = <*((proj (i,n)) . x)*> );

definition
let i be Nat;
let x be FinSequence of REAL ;
func reproj (i,x) -> Function means :Def5: :: PDIFF_1:def 5
( dom it = REAL & ( for r being Element of REAL holds it . r = Replace (x,i,r) ) );
existence
ex b1 being Function st
( dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) & dom b2 = REAL & ( for r being Element of REAL holds b2 . r = Replace (x,i,r) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines reproj PDIFF_1:def 5 :
for i being Nat
for x being FinSequence of REAL
for b3 being Function holds
( b3 = reproj (i,x) iff ( dom b3 = REAL & ( for r being Element of REAL holds b3 . r = Replace (x,i,r) ) ) );

definition
let n, i be Nat;
let x be Element of REAL n;
:: original: reproj
redefine func reproj (i,x) -> Function of REAL,(REAL n);
correctness
coherence
reproj (i,x) is Function of REAL,(REAL n);
proof end;
end;

definition
let n, i be Nat;
let x be Point of (REAL-NS n);
func reproj (i,x) -> Function of (REAL-NS 1),(REAL-NS n) means :Def6: :: PDIFF_1:def 6
 for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & it . r = (reproj (i,y)) . q );
existence
ex b1 being Function of (REAL-NS 1),(REAL-NS n) st
for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b1 . r = (reproj (i,y)) . q )
proof end;
uniqueness
for b1, b2 being Function of (REAL-NS 1),(REAL-NS n) st ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b1 . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b2 . r = (reproj (i,y)) . q ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines reproj PDIFF_1:def 6 :
for n, i being Nat
for x being Point of (REAL-NS n)
for b4 being Function of (REAL-NS 1),(REAL-NS n) holds
( b4 = reproj (i,x) iff for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b4 . r = (reproj (i,y)) . q ) );

definition
let m, n be non zero Nat;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
pred f is_differentiable_in x means :: PDIFF_1:def 7
 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_differentiable_in y );
end;

:: deftheorem defines is_differentiable_in PDIFF_1:def 7 :
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_differentiable_in x iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_differentiable_in y ) );

definition
let m, n be non zero Nat;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
assume A1: f is_differentiable_in x ;
func diff (f,x) -> Function of (REAL m),(REAL n) means :Def8: :: PDIFF_1:def 8
 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & it = diff (g,y) );
correctness
existence
ex b1 being Function of (REAL m),(REAL n) ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) );
uniqueness
for b1, b2 being Function of (REAL m),(REAL n) st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = diff (g,y) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def8 defines diff PDIFF_1:def 8 :
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
for b5 being Function of (REAL m),(REAL n) holds
( b5 = diff (f,x) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b5 = diff (g,y) ) );

theorem Th3: :: PDIFF_1:3
for I being Function of REAL,(REAL 1) st I = (proj (1,1)) " holds
( ( for x being VECTOR of (REAL-NS 1)
for y being Real st x = I . y holds
||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y, a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Real st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st x = I . a & y = I . b holds
x - y = I . (a - b) ) )
proof end;

reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;

theorem Th4: :: PDIFF_1:4
for J being Function of (REAL 1),REAL st J = proj (1,1) holds
( ( for x being VECTOR of (REAL-NS 1)
for y being Real st J . x = y holds
||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y, a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Real st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st J . x = a & J . y = b holds
J . (x - y) = a - b ) )
proof end;

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

theorem Th5: :: PDIFF_1:5
for I being Function of REAL,(REAL 1)
for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
proof end;

theorem Th6: :: PDIFF_1:6
for I being Function of REAL,(REAL 1)
for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )
proof end;

theorem Th7: :: PDIFF_1:7
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Real st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
proof end;

theorem Th8: :: PDIFF_1:8
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
proof end;

theorem :: PDIFF_1:9
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Real st f = <>* g & x = <*y*> holds
( f is_differentiable_in x iff g is_differentiable_in y ) by Th7, Th8;

theorem Th10: :: PDIFF_1:10
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Real st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff (f,x)) . <*1*> = <*(diff (g,y))*>
proof end;

definition
let n, m be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
pred f is_partial_differentiable_in x,i means :: PDIFF_1:def 9
f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;
end;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 9 :
for n, m being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );

definition
let m, n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
func partdiff (f,x,i) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) equals :: PDIFF_1:def 10
 diff ((f * (reproj (i,x))),((Proj (i,m)) . x));
coherence
diff ((f * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ;
end;

:: deftheorem defines partdiff PDIFF_1:def 10 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((Proj (i,m)) . x));

definition
let n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
pred f is_partial_differentiable_in x,i means :: PDIFF_1:def 11
f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x;
end;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 11 :
for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds
( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x );

definition
let n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
func partdiff (f,x,i) -> Real equals :: PDIFF_1:def 12
 diff ((f * (reproj (i,x))),((proj (i,n)) . x));
coherence
diff ((f * (reproj (i,x))),((proj (i,n)) . x)) is Real ;
end;

:: deftheorem defines partdiff PDIFF_1:def 12 :
for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((proj (i,n)) . x));

theorem Th11: :: PDIFF_1:11
for n being non zero Nat
for i being Nat holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n))
proof end;

theorem Th12: :: PDIFF_1:12
for n being non zero Nat
for i being Nat
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
(reproj (i,y)) * (proj (1,1)) = reproj (i,x)
proof end;

theorem Th13: :: PDIFF_1:13
for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
proof end;

theorem Th14: :: PDIFF_1:14
for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
proof end;

theorem Th15: :: PDIFF_1:15
for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
proof end;

definition
let m, n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
pred f is_partial_differentiable_in x,i means :: PDIFF_1:def 13
 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_partial_differentiable_in y,i );
end;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 13 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_partial_differentiable_in x,i iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_partial_differentiable_in y,i ) );

definition
let m, n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
assume A1: f is_partial_differentiable_in x,i ;
func partdiff (f,x,i) -> Element of REAL n means :Def14: :: PDIFF_1:def 14
 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & it = (partdiff (g,y,i)) . <*1*> );
correctness
existence
ex b1 being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> );
uniqueness
for b1, b2 being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = (partdiff (g,y,i)) . <*1*> ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def14 defines partdiff PDIFF_1:def 14 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_partial_differentiable_in x,i holds
for b6 being Element of REAL n holds
( b6 = partdiff (f,x,i) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b6 = (partdiff (g,y,i)) . <*1*> ) );

theorem :: PDIFF_1:16
for i being Nat
for m, n being non zero Nat
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) ;

theorem Th17: :: PDIFF_1:17
for i being Nat
for m, n being non zero Nat
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
proof end;

theorem :: PDIFF_1:18
for n being non zero Nat
for i being Nat
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
proof end;

theorem :: PDIFF_1:19
for n being non zero Nat
for i being Nat
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
proof end;

definition
let m, n be non zero Nat;
let i, j be Nat;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
pred f is_partial_differentiable_in x,i,j means :: PDIFF_1:def 15
((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;
end;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 15 :
for m, n being non zero Nat
for i, j being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( f is_partial_differentiable_in x,i,j iff ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );

definition
let m, n be non zero Nat;
let i, j be Nat;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
func partdiff (f,x,i,j) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) equals :: PDIFF_1:def 16
 diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));
correctness
coherence
diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)));
;
end;

:: deftheorem defines partdiff PDIFF_1:def 16 :
for m, n being non zero Nat
for i, j being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds partdiff (f,x,i,j) = diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));

definition
let m, n be non zero Nat;
let i, j be Nat;
let h be PartFunc of (REAL m),(REAL n);
let z be Element of REAL m;
pred h is_partial_differentiable_in z,i,j means :: PDIFF_1:def 17
((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z;
end;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 17 :
for m, n being non zero Nat
for i, j being Nat
for h being PartFunc of (REAL m),(REAL n)
for z being Element of REAL m holds
( h is_partial_differentiable_in z,i,j iff ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z );

definition
let m, n be non zero Nat;
let i, j be Nat;
let h be PartFunc of (REAL m),(REAL n);
let z be Element of REAL m;
func partdiff (h,z,i,j) -> Real equals :: PDIFF_1:def 18
 diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));
correctness
coherence
diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z)) is Real;
;
end;

:: deftheorem defines partdiff PDIFF_1:def 18 :
for m, n being non zero Nat
for i, j being Nat
for h being PartFunc of (REAL m),(REAL n)
for z being Element of REAL m holds partdiff (h,z,i,j) = diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));

theorem :: PDIFF_1:20
for m, n being non zero Nat
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y ) ;

theorem :: PDIFF_1:21
for m, n being non zero Nat
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff (F,x) = diff (G,y)
proof end;

theorem Th22: :: PDIFF_1:22
for m, n being non zero Nat
for i, j being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
proof end;

theorem :: PDIFF_1:23
for m, n being non zero Nat
for i, j being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
proof end;

theorem :: PDIFF_1:24
for m, n being non zero Nat
for i, j being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
proof end;

definition
let m, n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let X be set ;
pred f is_partial_differentiable_on X,i means :: PDIFF_1:def 19
( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds
f | X is_partial_differentiable_in x,i ) );
end;

:: deftheorem defines is_partial_differentiable_on PDIFF_1:def 19 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds
f | X is_partial_differentiable_in x,i ) ) );

theorem Th25: :: PDIFF_1:25
for m, n being non zero Nat
for i being Nat
for X being set
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m) by XBOOLE_1:1;

definition
let m, n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let X be set ;
assume A1: f is_partial_differentiable_on X,i ;
func f `partial| (X,i) -> PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) means :: PDIFF_1:def 20
( dom it = X & ( for x being Point of (REAL-NS m) st x in X holds
it /. x = partdiff (f,x,i) ) );
existence
ex b1 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st
( dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = X & ( for x being Point of (REAL-NS m) st x in X holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines `partial| PDIFF_1:def 20 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set st f is_partial_differentiable_on X,i holds
for b6 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) holds
( b6 = f `partial| (X,i) iff ( dom b6 = X & ( for x being Point of (REAL-NS m) st x in X holds
b6 /. x = partdiff (f,x,i) ) ) );

theorem Th26: :: PDIFF_1:26
for m, n being non zero Nat
for i being Nat
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )
proof end;

theorem Th27: :: PDIFF_1:27
for m, n being non zero Nat
for i being Nat
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
proof end;

theorem Th28: :: PDIFF_1:28
for m, n being non zero Nat
for i being Nat
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
proof end;

theorem :: PDIFF_1:29
for n being non zero Nat
for i being Nat
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
proof end;

theorem Th30: :: PDIFF_1:30
for m, n being non zero Nat
for i being Nat
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )
proof end;

theorem :: PDIFF_1:31
for n being non zero Nat
for i being Nat
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
proof end;

theorem Th32: :: PDIFF_1:32
for m, n being non zero Nat
for i being Nat
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
proof end;

theorem :: PDIFF_1:33
for n being non zero Nat
for i being Nat
for r being Real
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
proof end;