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


begin

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
proofend;
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
proofend;
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 Element of REAL holds
( (proj (1,1)) . <*x*> = x &amp; ((proj (1,1)) ") . x = <*x*> ) ) )
proofend;

Lm2:  for i, n being Element of NAT st i in Seg n holds
proj (i,n) is onto
proofend;

theorem :: PDIFF_1:1
( ( for i, n being Element of NAT st i in Seg n holds
( dom (proj (i,n)) = REAL n &amp; rng (proj (i,n)) = REAL ) ) &amp; ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x &amp; ((proj (1,1)) ") . x = <*x*> ) ) )
proofend;

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

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)
proofend;
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);
proofend;
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)*>
proofend;
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)*> ) &amp; ( for x being Point of (REAL-NS n) holds b2 . x = <*((proj (i,n)) . x)*> ) holds
b1 = b2
proofend;
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 Element of NAT ;
let x be FinSequence of REAL ;
func reproj (i,x) ->  Function means :Def5: :: PDIFF_1:def 5
( dom it = REAL &amp; ( for r being Element of REAL holds it . r = Replace (x,i,r) ) );
existence
 ex b1 being Function st
( dom b1 = REAL &amp; ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = REAL &amp; ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) &amp; dom b2 = REAL &amp; ( for r being Element of REAL holds b2 . r = Replace (x,i,r) ) holds
b1 = b2
proofend;
end;

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

definition
let n, i be Element of 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);
proofend;
end;

definition
let n, i be Element of 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*> &amp; y = x &amp; 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*> &amp; y = x &amp; b1 . r = (reproj (i,y)) . q )
proofend;
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*> &amp; y = x &amp; b1 . r = (reproj (i,y)) . q ) ) &amp; ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> &amp; y = x &amp; b2 . r = (reproj (i,y)) . q ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines reproj PDIFF_1:def_6_:_
 for n, i being Element of 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*> &amp; y = x &amp; b4 . r = (reproj (i,y)) . q ) );

definition
let m, n be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
predf is_differentiable_in x means :Def7: :: 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 &amp; x = y &amp; g is_differentiable_in y );
end;

:: deftheorem Def7 defines is_differentiable_in PDIFF_1:def_7_:_
 for m, n being non empty Element of 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 &amp; x = y &amp; g is_differentiable_in y ) );

definition
let m, n be non empty Element of 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 &amp; x = y &amp; 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 &amp; x = y &amp; 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 &amp; x = y &amp; b1 = diff (g,y) ) &amp; ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g &amp; x = y &amp; b2 = diff (g,y) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def8 defines diff PDIFF_1:def_8_:_
 for m, n being non empty Element of 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 &amp; x = y &amp; 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 Element of REAL st x = I . y holds
||.x.|| = abs y ) &amp; ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a &amp; y = I . b holds
x + y = I . (a + b) ) &amp; ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) &amp; ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) &amp; ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a &amp; y = I . b holds
x - y = I . (a - b) ) )
proofend;

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 Element of REAL st J . x = y holds
||.x.|| = abs y ) &amp; ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a &amp; J . y = b holds
J . (x + y) = a + b ) &amp; ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) &amp; ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) &amp; ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a &amp; J . y = b holds
J . (x - y) = a - b ) )
proofend;

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)) " &amp; J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) &amp; ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
proofend;

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)) " &amp; J = proj (1,1) holds
( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) &amp; ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )
proofend;

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 Element of REAL st f = <>* g &amp; x = <*y*> &amp; f is_differentiable_in x holds
( g is_differentiable_in y &amp; diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
proofend;

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 Element of REAL st f = <>* g &amp; x = <*y*> &amp; g is_differentiable_in y holds
( f is_differentiable_in x &amp; (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
proofend;

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 Element of REAL st f = <>* g &amp; 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 Element of REAL st f = <>* g &amp; x = <*y*> &amp; f is_differentiable_in x holds
(diff (f,x)) . <*1*> = <*(diff (g,y))*>
proofend;

begin

definition
let n, m be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
predf is_partial_differentiable_in x,i means :Def9: :: PDIFF_1:def 9
f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;
end;

:: deftheorem Def9 defines is_partial_differentiable_in PDIFF_1:def_9_:_
 for n, m being non empty Element of NAT
for i being Element of 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 empty Element of NAT ;
let i be Element of 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 empty Element of NAT
for i being Element of 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 empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
predf is_partial_differentiable_in x,i means :Def11: :: PDIFF_1:def 11
f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x;
end;

:: deftheorem Def11 defines is_partial_differentiable_in PDIFF_1:def_11_:_
 for n being non empty Element of NAT
for i being Element of 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 empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
func partdiff (f,x,i) ->  real number  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 number ;
end;

:: deftheorem  defines partdiff PDIFF_1:def_12_:_
 for n being non empty Element of NAT
for i being Element of 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));

definition
let n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
:: original:partdiff
redefine func partdiff (f,x,i) ->  Real;
coherence
 partdiff (f,x,i) is Real ;
end;

theorem Th11: :: PDIFF_1:11
for n being non empty Element of NAT
for i being Element of NAT holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n))
proofend;

theorem Th12: :: PDIFF_1:12
for n being non empty Element of NAT
for i being Element of 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)
proofend;

theorem Th13: :: PDIFF_1:13
for n being non empty Element of NAT
for i being Element of 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 &amp; x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
proofend;

theorem Th14: :: PDIFF_1:14
for n being non empty Element of NAT
for i being Element of 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 &amp; x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
proofend;

theorem Th15: :: PDIFF_1:15
for n being non empty Element of NAT
for i being Element of 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 &amp; x = y &amp; f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
proofend;

definition
let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
predf is_partial_differentiable_in x,i means :Def13: :: 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 &amp; x = y &amp; g is_partial_differentiable_in y,i );
end;

:: deftheorem Def13 defines is_partial_differentiable_in PDIFF_1:def_13_:_
 for m, n being non empty Element of NAT
for i being Element of 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 &amp; x = y &amp; g is_partial_differentiable_in y,i ) );

definition
let m, n be non empty Element of NAT ;
let i be Element of 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 &amp; x = y &amp; 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 &amp; x = y &amp; 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 &amp; x = y &amp; b1 = (partdiff (g,y,i)) . <*1*> ) &amp; ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g &amp; x = y &amp; b2 = (partdiff (g,y,i)) . <*1*> ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def14 defines partdiff PDIFF_1:def_14_:_
 for m, n being non empty Element of NAT
for i being Element of 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 &amp; x = y &amp; b6 = (partdiff (g,y,i)) . <*1*> ) );

theorem Th16: :: PDIFF_1:16
for i being Element of NAT
for m, n being non empty Element of 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 &amp; x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
proofend;

theorem Th17: :: PDIFF_1:17
for i being Element of NAT
for m, n being non empty Element of 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 &amp; x = y &amp; F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
proofend;

theorem :: PDIFF_1:18
for n being non empty Element of NAT
for i being Element of 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 )
proofend;

theorem :: PDIFF_1:19
for n being non empty Element of NAT
for i being Element of 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 &amp; g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
proofend;

begin

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

:: deftheorem Def15 defines is_partial_differentiable_in PDIFF_1:def_15_:_
 for m, n being non empty Element of NAT
for i, j being Element of 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 empty Element of NAT ;
let i, j be Element of 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 empty Element of NAT
for i, j being Element of 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 empty Element of NAT ;
let i, j be Element of NAT ;
let h be PartFunc of (REAL m),(REAL n);
let z be Element of REAL m;
predh is_partial_differentiable_in z,i,j means :Def17: :: PDIFF_1:def 17
((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z;
end;

:: deftheorem Def17 defines is_partial_differentiable_in PDIFF_1:def_17_:_
 for m, n being non empty Element of NAT
for i, j being Element of 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 empty Element of NAT ;
let i, j be Element of NAT ;
let h be PartFunc of (REAL m),(REAL n);
let z be Element of REAL m;
func partdiff (h,z,i,j) ->  real number  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 number ;
;
end;

:: deftheorem  defines partdiff PDIFF_1:def_18_:_
 for m, n being non empty Element of NAT
for i, j being Element of 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 Th20: :: PDIFF_1:20
for m, n being non empty Element of 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 &amp; x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
proofend;

theorem :: PDIFF_1:21
for m, n being non empty Element of 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 &amp; x = y &amp; F is_differentiable_in x holds
diff (F,x) = diff (G,y)
proofend;

theorem Th22: :: PDIFF_1:22
for m, n being non empty Element of NAT
for j, i being Element of 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 &amp; x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
proofend;

theorem :: PDIFF_1:23
for n, m being non empty Element of NAT
for i, j being Element of 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 &amp; x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
proofend;

theorem :: PDIFF_1:24
for n, m being non empty Element of NAT
for i, j being Element of 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 &amp; x = z &amp; f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
proofend;

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

:: deftheorem Def19 defines is_partial_differentiable_on PDIFF_1:def_19_:_
 for m, n being non empty Element of NAT
for i being Element of 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 &amp; ( 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 n, m being non empty Element of NAT
for i being Element of 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)
proofend;

definition
let m, n be non empty Element of NAT ;
let i be Element of 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 ;
funcf `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 &amp; ( 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 &amp; ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st dom b1 = X &amp; ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) &amp; dom b2 = X &amp; ( for x being Point of (REAL-NS m) st x in X holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines `partial| PDIFF_1:def_20_:_
 for m, n being non empty Element of NAT
for i being Element of 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 &amp; ( 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 n, m being non empty Element of NAT
for i being Element of 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))) &amp; (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )
proofend;

theorem Th27: :: PDIFF_1:27
for n, m being non empty Element of NAT
for i being Element of 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))
proofend;

theorem Th28: :: PDIFF_1:28
for n, m being non empty Element of NAT
for i being Element of 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 &amp; f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i &amp; partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
proofend;

theorem :: PDIFF_1:29
for n being non empty Element of NAT
for i being Element of 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 &amp; g2 is_partial_differentiable_in y,i holds
( g1 + g2 is_partial_differentiable_in y,i &amp; partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
proofend;

theorem Th30: :: PDIFF_1:30
for n, m being non empty Element of NAT
for i being Element of 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 &amp; f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i &amp; partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )
proofend;

theorem :: PDIFF_1:31
for n being non empty Element of NAT
for i being Element of 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 &amp; g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i &amp; partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
proofend;

theorem Th32: :: PDIFF_1:32
for n, m being non empty Element of NAT
for i being Element of 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 &amp; partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
proofend;

theorem :: PDIFF_1:33
for n being non empty Element of NAT
for i being Element of 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 &amp; partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
proofend;