:: Higher Order Partial Differentiation
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 20, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

theorem LM01CPre2: :: PDIFF_9:1
for S, T being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,T))
for r being Real st 0 <= r &amp; ( for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r * ||.x.|| ) holds
||.f.|| <= r
proofend;

theorem NFCONT125: :: PDIFF_9:2
for Z being set
for S being RealNormSpace
for f being PartFunc of S,REAL holds
( f is_continuous_on Z iff ( Z c= dom f &amp; ( for s1 being sequence of S st rng s1 c= Z &amp; s1 is convergent &amp; lim s1 in Z holds
( f /* s1 is convergent &amp; f /. (lim s1) = lim (f /* s1) ) ) ) )
proofend;

theorem LMXTh0: :: PDIFF_9:3
for i being Element of NAT
for f being PartFunc of (REAL i),REAL holds dom (<>* f) = dom f
proofend;

theorem :: PDIFF_9:4
for i being Element of NAT
for Z being set
for f being PartFunc of (REAL i),REAL st Z c= dom f holds
dom ((<>* f) | Z) = Z
proofend;

theorem LMXTh1: :: PDIFF_9:5
for i being Element of NAT
for Z being set
for f being PartFunc of (REAL i),REAL holds <>* (f | Z) = (<>* f) | Z
proofend;

theorem XTh30: :: PDIFF_9:6
for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for x being Element of REAL i st x in dom f holds
( (<>* f) . x = <*(f . x)*> &amp; (<>* f) /. x = <*(f /. x)*> )
proofend;

theorem LMXTh10: :: PDIFF_9:7
for i being Element of NAT
for f, g being PartFunc of (REAL i),REAL holds
( <>* (f + g) = (<>* f) + (<>* g) &amp; <>* (f - g) = (<>* f) - (<>* g) )
proofend;

theorem LMXTh11: :: PDIFF_9:8
for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for r being real number holds <>* (r (#) f) = r (#) (<>* f)
proofend;

XTh30D:  for x being Real
for y being Element of REAL 1 st <*x*> = y holds
|.x.| = |.y.|
proofend;

theorem LMXTh13: :: PDIFF_9:9
for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for g being PartFunc of (REAL i),(REAL 1) st <>* f = g holds
|.f.| = |.g.|
proofend;

theorem OPEN: :: PDIFF_9:10
for m being non empty Element of NAT
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X = Y holds
( X is open iff Y is open )
proofend;

theorem PDIFF75: :: PDIFF_9:11
for i, j being Element of NAT
for q being Element of REAL st 1 <= i &amp; i <= j holds
|.((reproj (i,(0* j))) . q).| = |.q.|
proofend;

Lm5:  for m being non empty Element of NAT
for i being Element of NAT
for x being Element of REAL m
for Z being Subset of (REAL m) st Z is open &amp; x in Z &amp; 1 <= i &amp; i <= m holds
ex N being Neighbourhood of (proj (i,m)) . x st
for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z
proofend;

theorem LMMMTh6: :: PDIFF_9:12
for j, i being Element of NAT
for x being Element of REAL j holds x = (reproj (i,x)) . ((proj (i,j)) . x)
proofend;

begin

theorem MPDIFF633: :: PDIFF_9:13
for m, n being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is open
proofend;

theorem MPDIFF632: :: PDIFF_9:14
for m, n being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n) st X is open holds
( f is_differentiable_on X iff ( X c= dom f &amp; ( for x being Element of REAL m st x in X holds
f is_differentiable_in x ) ) )
proofend;

definition
let m, n be non empty Element of NAT ;
let Z be set ;
let f be PartFunc of (REAL m),(REAL n);
assume A1: Z c= dom f ;
funcf `| Z ->  PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) means :Def1: :: PDIFF_9:def 1
( dom it = Z &amp; ( for x being Element of REAL m st x in Z holds
it /. x = diff (f,x) ) );
existence
 ex b1 being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) st
( dom b1 = Z &amp; ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) st dom b1 = Z &amp; ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) &amp; dom b2 = Z &amp; ( for x being Element of REAL m st x in Z holds
b2 /. x = diff (f,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines `| PDIFF_9:def_1_:_
 for m, n being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),(REAL n) st Z c= dom f holds
for b5 being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) holds
( b5 = f `| Z iff ( dom b5 = Z &amp; ( for x being Element of REAL m st x in Z holds
b5 /. x = diff (f,x) ) ) );

theorem :: PDIFF_9:15
for m, n being non empty Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X &amp; g is_differentiable_on X holds
( f + g is_differentiable_on X &amp; ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) ) )
proofend;

theorem :: PDIFF_9:16
for m, n being non empty Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X &amp; g is_differentiable_on X holds
( f - g is_differentiable_on X &amp; ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = (diff (f,x)) - (diff (g,x)) ) )
proofend;

theorem :: PDIFF_9:17
for m, n being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n)
for r being Real st f is_differentiable_on X holds
( r (#) f is_differentiable_on X &amp; ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) (diff (f,x)) ) )
proofend;

theorem LM01A: :: PDIFF_9:18
for j being Element of NAT
for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS j))) ex p being Point of (REAL-NS j) st
( p = f . <*1*> &amp; ( for r being Real
for x being Point of (REAL-NS 1) st x = <*r*> holds
f . x = r * p ) &amp; ( for x being Point of (REAL-NS 1) holds ||.(f . x).|| = ||.p.|| * ||.x.|| ) )
proofend;

theorem LM01C: :: PDIFF_9:19
for j being Element of NAT
for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS j))) ex p being Point of (REAL-NS j) st
( p = f . <*1*> &amp; ||.p.|| = ||.f.|| )
proofend;

theorem LM01: :: PDIFF_9:20
for j being Element of NAT
for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS j)))
for x being Point of (REAL-NS 1) holds ||.(f . x).|| = ||.f.|| * ||.x.||
proofend;

theorem LM02: :: PDIFF_9:21
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 g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st 1 <= i &amp; i <= m &amp; X is open &amp; g = f &amp; X = Y &amp; f is_partial_differentiable_on X,i holds
for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X &amp; x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
proofend;

theorem LM03: :: PDIFF_9:22
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 g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st 1 <= i &amp; i <= m &amp; X is open &amp; g = f &amp; X = Y &amp; f is_partial_differentiable_on X,i holds
for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 &amp; x1 = y1 &amp; x0 in X &amp; x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
proofend;

theorem LM1Direct: :: PDIFF_9:23
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 g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st 1 <= i &amp; i <= m &amp; X is open &amp; g = f &amp; X = Y holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i &amp; g `partial| (Y,i) is_continuous_on Y ) )
proofend;

theorem ThGdiff: :: PDIFF_9:24
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X = Y &amp; X is open &amp; f = g holds
( ( for i being Element of NAT st 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) ) iff ( g is_differentiable_on Y &amp; g `| Y is_continuous_on Y ) )
proofend;

theorem LM2: :: PDIFF_9:25
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X is open &amp; X c= dom f &amp; g = f &amp; X = Y holds
( g is_differentiable_on Y &amp; g `| Y is_continuous_on Y iff ( f is_differentiable_on X &amp; ( for x0 being Element of REAL m
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Element of REAL m st x1 in X &amp; |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
proofend;

theorem CW01: :: PDIFF_9:26
for m, n being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n) st X is open &amp; X c= dom f holds
( ( for i being Element of NAT st 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X &amp; ( for x0 being Element of REAL m
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Element of REAL m st x1 in X &amp; |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
proofend;

theorem :: PDIFF_9:27
for m, n being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g &amp; f is_differentiable_on Z holds
f `| Z = g `| Z
proofend;

theorem :: PDIFF_9:28
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X = Y &amp; X is open &amp; f = g holds
( ( for i being Element of NAT st 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X &amp; g `| Y is_continuous_on Y ) )
proofend;

theorem XTh350: :: PDIFF_9:29
for m, n being non empty Element of NAT
for f, g being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_continuous_in x &amp; g is_continuous_in x holds
( f + g is_continuous_in x &amp; f - g is_continuous_in x )
proofend;

theorem XTh351: :: PDIFF_9:30
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
for r being Real st f is_continuous_in x holds
r (#) f is_continuous_in x
proofend;

theorem :: PDIFF_9:31
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_continuous_in x holds
- f is_continuous_in x
proofend;

theorem YTh354: :: PDIFF_9:32
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_continuous_in x holds
|.f.| is_continuous_in x
proofend;

theorem XTh350X: :: PDIFF_9:33
for m, n being non empty Element of NAT
for Z being set
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z &amp; g is_continuous_on Z holds
( f + g is_continuous_on Z &amp; f - g is_continuous_on Z )
proofend;

theorem XTh351X: :: PDIFF_9:34
for m, n being non empty Element of NAT
for Z being set
for r being Real
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
r (#) f is_continuous_on Z
proofend;

theorem :: PDIFF_9:35
for m, n being non empty Element of NAT
for Z being set
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
- f is_continuous_on Z
proofend;

theorem XDef60: :: PDIFF_9:36
for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for x0 being Element of REAL i holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x being Element of REAL i st x in dom f &amp; |.(x - x0).| < s holds
|.((f /. x) - (f /. x0)).| < r ) ) ) ) )
proofend;

theorem XTh35: :: PDIFF_9:37
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff <>* f is_continuous_in x0 )
proofend;

theorem :: PDIFF_9:38
for m being non empty Element of NAT
for f, g being PartFunc of (REAL m),REAL
for x0 being Element of REAL m st f is_continuous_in x0 &amp; g is_continuous_in x0 holds
( f + g is_continuous_in x0 &amp; f - g is_continuous_in x0 )
proofend;

theorem :: PDIFF_9:39
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for x0 being Element of REAL m
for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
proofend;

theorem :: PDIFF_9:40
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for x0 being Element of REAL m st f is_continuous_in x0 holds
|.f.| is_continuous_in x0
proofend;

XTh360:  for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for g being PartFunc of (REAL-NS i),REAL
for x being Element of REAL i
for y being Point of (REAL-NS i) st f = g &amp; x = y holds
( f is_continuous_in x iff ( y in dom g &amp; ( for s being sequence of (REAL-NS i) st rng s c= dom g &amp; s is convergent &amp; lim s = y holds
( g /* s is convergent &amp; g /. y = lim (g /* s) ) ) ) )
proofend;

theorem :: PDIFF_9:41
for i being Element of NAT
for f, g being PartFunc of (REAL i),REAL
for x being Element of REAL i st f is_continuous_in x &amp; g is_continuous_in x holds
f (#) g is_continuous_in x
proofend;

definition
let m be non empty Element of NAT ;
let Z be set ;
let f be PartFunc of (REAL m),REAL;
predf is_continuous_on Z means :XDef7: :: PDIFF_9:def 2
 for x0 being Element of REAL m st x0 in Z holds
f | Z is_continuous_in x0;
end;

:: deftheorem XDef7 defines is_continuous_on PDIFF_9:def_2_:_
 for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL holds
( f is_continuous_on Z iff for x0 being Element of REAL m st x0 in Z holds
f | Z is_continuous_in x0 );

theorem XTh360B: :: PDIFF_9:42
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL-NS m),REAL st f = g holds
( ( Z c= dom f &amp; f is_continuous_on Z ) iff g is_continuous_on Z )
proofend;

theorem XTh360C: :: PDIFF_9:43
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL-NS m),REAL st f = g &amp; Z c= dom f holds
( f is_continuous_on Z iff for s being sequence of (REAL-NS m) st rng s c= Z &amp; s is convergent &amp; lim s in Z holds
( g /* s is convergent &amp; g /. (lim s) = lim (g /* s) ) )
proofend;

theorem XTh37: :: PDIFF_9:44
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g holds
( ( Z c= dom f &amp; f is_continuous_on Z ) iff g is_continuous_on Z )
proofend;

theorem XTh38: :: PDIFF_9:45
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL st Z c= dom f holds
( f is_continuous_on Z iff for x0 being Element of REAL m
for r being Real st x0 in Z &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Element of REAL m st x1 in Z &amp; |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
proofend;

theorem :: PDIFF_9:46
for m being non empty Element of NAT
for Z being set
for f, g being PartFunc of (REAL m),REAL st f is_continuous_on Z &amp; g is_continuous_on Z &amp; Z c= dom f &amp; Z c= dom g holds
( f + g is_continuous_on Z &amp; f - g is_continuous_on Z )
proofend;

theorem :: PDIFF_9:47
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for r being Real st Z c= dom f &amp; f is_continuous_on Z holds
r (#) f is_continuous_on Z
proofend;

theorem :: PDIFF_9:48
for m being non empty Element of NAT
for Z being set
for f, g being PartFunc of (REAL m),REAL st f is_continuous_on Z &amp; g is_continuous_on Z &amp; Z c= dom f &amp; Z c= dom g holds
f (#) g is_continuous_on Z
proofend;

theorem PDIFF736X: :: PDIFF_9:49
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL-NS m),REAL st f = g holds
( ( Z c= dom f &amp; f is_continuous_on Z ) iff g is_continuous_on Z )
proofend;

theorem :: PDIFF_9:50
for m, n being non empty Element of NAT
for Z being set
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
|.f.| is_continuous_on Z
proofend;

theorem PDIFF620X: :: PDIFF_9:51
for m being non empty Element of NAT
for f, g being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x &amp; g is_differentiable_in x holds
( f + g is_differentiable_in x &amp; diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) &amp; f - g is_differentiable_in x &amp; diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )
proofend;

theorem PDIFF622X: :: PDIFF_9:52
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for r being Real
for x being Element of REAL m st f is_differentiable_in x holds
( r (#) f is_differentiable_in x &amp; diff ((r (#) f),x) = r (#) (diff (f,x)) )
proofend;

definition
let Z be set ;
let m be non empty Element of NAT ;
let f be PartFunc of (REAL m),REAL;
predf is_differentiable_on Z means :XDef4: :: PDIFF_9:def 3
 for x being Element of REAL m st x in Z holds
f | Z is_differentiable_in x;
end;

:: deftheorem XDef4 defines is_differentiable_on PDIFF_9:def_3_:_
 for Z being set
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL holds
( f is_differentiable_on Z iff for x being Element of REAL m st x in Z holds
f | Z is_differentiable_in x );

theorem YTh30: :: PDIFF_9:53
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g holds
( ( Z c= dom f &amp; f is_differentiable_on Z ) iff g is_differentiable_on Z )
proofend;

theorem YTh32: :: PDIFF_9:54
for m being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X c= dom f &amp; X is open holds
( f is_differentiable_on X iff for x being Element of REAL m st x in X holds
f is_differentiable_in x )
proofend;

theorem YTh33: :: PDIFF_9:55
for m being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X c= dom f &amp; f is_differentiable_on X holds
X is open
proofend;

definition
let m be non empty Element of NAT ;
let Z be set ;
let f be PartFunc of (REAL m),REAL;
assume AK: Z c= dom f ;
funcf `| Z ->  PartFunc of (REAL m),(Funcs ((REAL m),REAL)) means :XDef1: :: PDIFF_9:def 4
( dom it = Z &amp; ( for x being Element of REAL m st x in Z holds
it /. x = diff (f,x) ) );
existence
 ex b1 being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) st
( dom b1 = Z &amp; ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) st dom b1 = Z &amp; ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) &amp; dom b2 = Z &amp; ( for x being Element of REAL m st x in Z holds
b2 /. x = diff (f,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem XDef1 defines `| PDIFF_9:def_4_:_
 for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL st Z c= dom f holds
for b4 being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) holds
( b4 = f `| Z iff ( dom b4 = Z &amp; ( for x being Element of REAL m st x in Z holds
b4 /. x = diff (f,x) ) ) );

theorem :: PDIFF_9:56
for m being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g &amp; X c= dom f &amp; f is_differentiable_on X holds
( g is_differentiable_on X &amp; ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) )
proofend;

theorem :: PDIFF_9:57
for m being non empty Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X c= dom f &amp; X c= dom g &amp; f is_differentiable_on X &amp; g is_differentiable_on X holds
( f + g is_differentiable_on X &amp; ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = ((f `| X) /. x) + ((g `| X) /. x) ) )
proofend;

theorem :: PDIFF_9:58
for m being non empty Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X c= dom f &amp; X c= dom g &amp; f is_differentiable_on X &amp; g is_differentiable_on X holds
( f - g is_differentiable_on X &amp; ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = ((f `| X) /. x) - ((g `| X) /. x) ) )
proofend;

theorem :: PDIFF_9:59
for m being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for r being Real st X c= dom f &amp; f is_differentiable_on X holds
( r (#) f is_differentiable_on X &amp; ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) )
proofend;

definition
let m be non empty Element of NAT ;
let Z be set ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),REAL;
predf is_partial_differentiable_on Z,i means :CWDef19: :: PDIFF_9:def 5
( Z c= dom f &amp; ( for x being Element of REAL m st x in Z holds
f | Z is_partial_differentiable_in x,i ) );
end;

:: deftheorem CWDef19 defines is_partial_differentiable_on PDIFF_9:def_5_:_
 for m being non empty Element of NAT
for Z being set
for i being Element of NAT
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f &amp; ( for x being Element of REAL m st x in Z holds
f | Z is_partial_differentiable_in x,i ) ) );

definition
let m be non empty Element of NAT ;
let Z be set ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),REAL;
assume A1: f is_partial_differentiable_on Z,i ;
funcf `partial| (Z,i) ->  PartFunc of (REAL m),REAL means :DefPDX: :: PDIFF_9:def 6
( dom it = Z &amp; ( for x being Element of REAL m st x in Z holds
it /. x = partdiff (f,x,i) ) );
existence
 ex b1 being PartFunc of (REAL m),REAL st
( dom b1 = Z &amp; ( for x being Element of REAL m st x in Z holds
b1 /. x = partdiff (f,x,i) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL m),REAL st dom b1 = Z &amp; ( for x being Element of REAL m st x in Z holds
b1 /. x = partdiff (f,x,i) ) &amp; dom b2 = Z &amp; ( for x being Element of REAL m st x in Z holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
proofend;
end;

:: deftheorem DefPDX defines `partial| PDIFF_9:def_6_:_
 for m being non empty Element of NAT
for Z being set
for i being Element of NAT
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,i holds
for b5 being PartFunc of (REAL m),REAL holds
( b5 = f `partial| (Z,i) iff ( dom b5 = Z &amp; ( for x being Element of REAL m st x in Z holds
b5 /. x = partdiff (f,x,i) ) ) );

theorem PDIFF734: :: PDIFF_9:60
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open &amp; 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f &amp; ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
proofend;

theorem CW020: :: PDIFF_9:61
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g &amp; X is open &amp; 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i )
proofend;

theorem CW021: :: PDIFF_9:62
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g &amp; X is open &amp; 1 <= i &amp; i <= m &amp; f is_partial_differentiable_on X,i holds
( f `partial| (X,i) is_continuous_on X iff g `partial| (X,i) is_continuous_on X )
proofend;

CW022:  for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1)
for x1, x0, v being Element of REAL m st <>* f = g holds
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).|
proofend;

theorem :: PDIFF_9:63
for m being non empty Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open &amp; X c= dom f holds
( ( for i being Element of NAT st 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X &amp; ( for x0 being Element of REAL m
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Element of REAL m st x1 in X &amp; |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
proofend;

LM1291:  for i, k being Element of NAT
for f, g being PartFunc of (REAL i),REAL
for x being Element of REAL i holds (f * (reproj (k,x))) (#) (g * (reproj (k,x))) = (f (#) g) * (reproj (k,x))
proofend;

theorem MPDIFF129: :: PDIFF_9:64
for m being non empty Element of NAT
for i being Element of NAT
for f, g being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_partial_differentiable_in x,i &amp; g is_partial_differentiable_in x,i holds
( f (#) g is_partial_differentiable_in x,i &amp; partdiff ((f (#) g),x,i) = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) )
proofend;

theorem XXX1: :: PDIFF_9:65
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open &amp; 1 <= i &amp; i <= m &amp; f is_partial_differentiable_on X,i &amp; g is_partial_differentiable_on X,i holds
( f + g is_partial_differentiable_on X,i &amp; (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) &amp; ( for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) )
proofend;

theorem XXX2: :: PDIFF_9:66
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open &amp; 1 <= i &amp; i <= m &amp; f is_partial_differentiable_on X,i &amp; g is_partial_differentiable_on X,i holds
( f - g is_partial_differentiable_on X,i &amp; (f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i)) &amp; ( for x being Element of REAL m st x in X holds
((f - g) `partial| (X,i)) /. x = (partdiff (f,x,i)) - (partdiff (g,x,i)) ) )
proofend;

theorem XXX3: :: PDIFF_9:67
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for r being Real
for f being PartFunc of (REAL m),REAL st X is open &amp; 1 <= i &amp; i <= m &amp; f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i &amp; (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) &amp; ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )
proofend;

theorem XXX4: :: PDIFF_9:68
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open &amp; 1 <= i &amp; i <= m &amp; f is_partial_differentiable_on X,i &amp; g is_partial_differentiable_on X,i holds
( f (#) g is_partial_differentiable_on X,i &amp; (f (#) g) `partial| (X,i) = ((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i))) &amp; ( for x being Element of REAL m st x in X holds
((f (#) g) `partial| (X,i)) /. x = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) ) )
proofend;

begin

definition
let m be non empty Element of NAT ;
let Z be set ;
let I be FinSequence of NAT ;
let f be PartFunc of (REAL m),REAL;
func PartDiffSeq (f,Z,I) ->  Functional_Sequence of (REAL m),REAL means :TDef5: :: PDIFF_9:def 7
( it . 0 = f &amp; ( for i being natural number holds it . (i + 1) = (it . i) `partial| (Z,(I /. (i + 1))) ) );
existence
 ex b1 being Functional_Sequence of (REAL m),REAL st
( b1 . 0 = f &amp; ( for i being natural number holds b1 . (i + 1) = (b1 . i) `partial| (Z,(I /. (i + 1))) ) )
proofend;
uniqueness
 for b1, b2 being Functional_Sequence of (REAL m),REAL st b1 . 0 = f &amp; ( for i being natural number holds b1 . (i + 1) = (b1 . i) `partial| (Z,(I /. (i + 1))) ) &amp; b2 . 0 = f &amp; ( for i being natural number holds b2 . (i + 1) = (b2 . i) `partial| (Z,(I /. (i + 1))) ) holds
b1 = b2
proofend;
end;

:: deftheorem TDef5 defines PartDiffSeq PDIFF_9:def_7_:_
 for m being non empty Element of NAT
for Z being set
for I being FinSequence of NAT
for f being PartFunc of (REAL m),REAL
for b5 being Functional_Sequence of (REAL m),REAL holds
( b5 = PartDiffSeq (f,Z,I) iff ( b5 . 0 = f &amp; ( for i being natural number holds b5 . (i + 1) = (b5 . i) `partial| (Z,(I /. (i + 1))) ) ) );

definition
let m be non empty Element of NAT ;
let Z be set ;
let I be FinSequence of NAT ;
let f be PartFunc of (REAL m),REAL;
predf is_partial_differentiable_on Z,I means :TDef6: :: PDIFF_9:def 8
 for i being Element of NAT st i <= (len I) - 1 holds
(PartDiffSeq (f,Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1);
end;

:: deftheorem TDef6 defines is_partial_differentiable_on PDIFF_9:def_8_:_
 for m being non empty Element of NAT
for Z being set
for I being FinSequence of NAT
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,I iff for i being Element of NAT st i <= (len I) - 1 holds
(PartDiffSeq (f,Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) );

definition
let m be non empty Element of NAT ;
let Z be set ;
let I be FinSequence of NAT ;
let f be PartFunc of (REAL m),REAL;
funcf `partial| (Z,I) ->  PartFunc of (REAL m),REAL equals :: PDIFF_9:def 9
(PartDiffSeq (f,Z,I)) . (len I);
correctness
coherence
(PartDiffSeq (f,Z,I)) . (len I) is PartFunc of (REAL m),REAL;
;
end;

:: deftheorem  defines `partial| PDIFF_9:def_9_:_
 for m being non empty Element of NAT
for Z being set
for I being FinSequence of NAT
for f being PartFunc of (REAL m),REAL holds f `partial| (Z,I) = (PartDiffSeq (f,Z,I)) . (len I);

XCWLM1:  for i being Element of NAT
for I being non empty FinSequence of NAT
for X being set st 1 <= i &amp; i <= len I &amp; rng I c= X holds
I /. i in X
proofend;

theorem XCW010: :: PDIFF_9:69
for m being non empty Element of NAT
for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open &amp; rng I c= Seg m &amp; f is_partial_differentiable_on X,I &amp; g is_partial_differentiable_on X,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f + g),X,I)) . i is_partial_differentiable_on X,I /. (i + 1) &amp; (PartDiffSeq ((f + g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) + ((PartDiffSeq (g,X,I)) . i) )
proofend;

theorem XCW011: :: PDIFF_9:70
for m being non empty Element of NAT
for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open &amp; rng I c= Seg m &amp; f is_partial_differentiable_on X,I &amp; g is_partial_differentiable_on X,I holds
( f + g is_partial_differentiable_on X,I &amp; (f + g) `partial| (X,I) = (f `partial| (X,I)) + (g `partial| (X,I)) )
proofend;

theorem XCW020: :: PDIFF_9:71
for m being non empty Element of NAT
for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open &amp; rng I c= Seg m &amp; f is_partial_differentiable_on X,I &amp; g is_partial_differentiable_on X,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f - g),X,I)) . i is_partial_differentiable_on X,I /. (i + 1) &amp; (PartDiffSeq ((f - g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) - ((PartDiffSeq (g,X,I)) . i) )
proofend;

theorem XCW021: :: PDIFF_9:72
for m being non empty Element of NAT
for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open &amp; rng I c= Seg m &amp; f is_partial_differentiable_on X,I &amp; g is_partial_differentiable_on X,I holds
( f - g is_partial_differentiable_on X,I &amp; (f - g) `partial| (X,I) = (f `partial| (X,I)) - (g `partial| (X,I)) )
proofend;

theorem XCW030: :: PDIFF_9:73
for m being non empty Element of NAT
for X being Subset of (REAL m)
for r being Real
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st X is open &amp; rng I c= Seg m &amp; f is_partial_differentiable_on X,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),X,I)) . i is_partial_differentiable_on X,I /. (i + 1) &amp; (PartDiffSeq ((r (#) f),X,I)) . i = r (#) ((PartDiffSeq (f,X,I)) . i) )
proofend;

theorem XCW031: :: PDIFF_9:74
for m being non empty Element of NAT
for X being Subset of (REAL m)
for r being Real
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st X is open &amp; rng I c= Seg m &amp; f is_partial_differentiable_on X,I holds
( r (#) f is_partial_differentiable_on X,I &amp; (r (#) f) `partial| (X,I) = r (#) (f `partial| (X,I)) )
proofend;

definition
let m be non empty Element of NAT ;
let f be PartFunc of (REAL m),REAL;
let k be Element of NAT ;
let Z be set ;
predf is_partial_differentiable_up_to_order k,Z means :TDef9: :: PDIFF_9:def 10
 for I being non empty FinSequence of NAT st len I <= k &amp; rng I c= Seg m holds
f is_partial_differentiable_on Z,I;
end;

:: deftheorem TDef9 defines is_partial_differentiable_up_to_order PDIFF_9:def_10_:_
 for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for k being Element of NAT
for Z being set holds
( f is_partial_differentiable_up_to_order k,Z iff for I being non empty FinSequence of NAT st len I <= k &amp; rng I c= Seg m holds
f is_partial_differentiable_on Z,I );

theorem XCW040: :: PDIFF_9:75
for m being non empty Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT holds
( f is_partial_differentiable_on Z,G ^ I iff ( f is_partial_differentiable_on Z,G &amp; f `partial| (Z,G) is_partial_differentiable_on Z,I ) )
proofend;

set Z0 = 0 ;

theorem XCW041: :: PDIFF_9:76
for m being non empty Element of NAT
for i being Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,<*i*> iff f is_partial_differentiable_on Z,i )
proofend;

theorem XCW042: :: PDIFF_9:77
for m being non empty Element of NAT
for i being Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL holds f `partial| (Z,<*i*>) = f `partial| (Z,i)
proofend;

theorem XCW0400: :: PDIFF_9:78
for m being non empty Element of NAT
for i, j being Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for I being non empty FinSequence of NAT st f is_partial_differentiable_up_to_order i + j,Z &amp; rng I c= Seg m &amp; len I = j holds
f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z
proofend;

theorem XCW0410: :: PDIFF_9:79
for m being non empty Element of NAT
for i, j being Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,Z &amp; j <= i holds
f is_partial_differentiable_up_to_order j,Z
proofend;

theorem :: PDIFF_9:80
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open &amp; f is_partial_differentiable_up_to_order i,X &amp; g is_partial_differentiable_up_to_order i,X holds
( f + g is_partial_differentiable_up_to_order i,X &amp; f - g is_partial_differentiable_up_to_order i,X )
proofend;

theorem :: PDIFF_9:81
for m being non empty Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for r being Real st X is open &amp; f is_partial_differentiable_up_to_order i,X holds
r (#) f is_partial_differentiable_up_to_order i,X
proofend;

theorem :: PDIFF_9:82
for m being non empty Element of NAT
for X being Subset of (REAL m) st X is open holds
for i being Element of NAT
for f, g being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,X &amp; g is_partial_differentiable_up_to_order i,X holds
f (#) g is_partial_differentiable_up_to_order i,X
proofend;