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


theorem Th1: :: 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 & ( for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r * ||.x.|| ) holds
||.f.|| <= r
proof end;

theorem Th2: :: 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 & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
proof end;

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

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

theorem Th5: :: 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
proof end;

theorem Th6: :: 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)*> & (<>* f) /. x = <*(f /. x)*> )
proof end;

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

theorem Th8: :: PDIFF_9:8
for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for r being Real holds <>* (r (#) f) = r (#) (<>* f)
proof end;

Lm1: for x being Real
for y being Element of REAL 1 st <*x*> = y holds
|.x.| = |.y.|
proof end;

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

theorem :: PDIFF_9:10
for m being non zero 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 ) ;

theorem Th11: :: PDIFF_9:11
for j being Element of NAT
for q being Real
for i being Nat st 1 <= i & i <= j holds
|.((reproj (i,(0* j))) . q).| = |.q.|
proof end;

Lm2: for m being non zero Element of NAT
for x being Element of REAL m
for Z being Subset of (REAL m)
for i being Nat st Z is open & x in Z & 1 <= i & 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
proof end;

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

theorem Th13: :: PDIFF_9:13
for m, n being non zero 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 by PDIFF_6:33;

theorem Th14: :: PDIFF_9:14
for m, n being non zero 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 & ( for x being Element of REAL m st x in X holds
f is_differentiable_in x ) ) ) by PDIFF_6:32;

definition
let m, n be non zero Element of NAT ;
let Z be set ;
let f be PartFunc of (REAL m),(REAL n);
assume A1: Z c= dom f ;
func f `| Z -> PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) means :Def1: :: PDIFF_9:def 1
( dom it = Z & ( 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 & ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) st dom b1 = Z & ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) & dom b2 = Z & ( for x being Element of REAL m st x in Z holds
b2 /. x = diff (f,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines `| PDIFF_9:def 1 :
for m, n being non zero 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 & ( 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 zero 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 & g is_differentiable_on X holds
( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) ) )
proof end;

theorem :: PDIFF_9:16
for m, n being non zero 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 & g is_differentiable_on X holds
( f - g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f - g) `| X) /. x = (diff (f,x)) - (diff (g,x)) ) )
proof end;

theorem :: PDIFF_9:17
for m, n being non zero 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 & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) (diff (f,x)) ) )
proof end;

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

theorem Th18: :: 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*> & ( for r being Real
for x being Point of (REAL-NS 1) st x = <*r*> holds
f . x = r * p ) & ( for x being Point of (REAL-NS 1) holds ||.(f . x).|| = ||.p.|| * ||.x.|| ) )
proof end;

theorem Th19: :: 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*> & ||.p.|| = ||.f.|| )
proof end;

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

theorem Th21: :: PDIFF_9:21
for m, n being non zero 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)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & 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 & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
proof end;

theorem Th22: :: PDIFF_9:22
for m, n being non zero 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)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & 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 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
proof end;

theorem Th23: :: PDIFF_9:23
for m, n being non zero 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)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
proof end;

theorem Th24: :: PDIFF_9:24
for m, n being non zero 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 & X is open & f = g holds
( ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )
proof end;

theorem Th25: :: PDIFF_9:25
for m, n being non zero 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 & X c= dom f & g = f & X = Y holds
( g is_differentiable_on Y & g `| Y is_continuous_on Y iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
proof end;

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

theorem :: PDIFF_9:27
for m, n being non zero 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 & f is_differentiable_on Z holds
f `| Z = g `| Z
proof end;

theorem :: PDIFF_9:28
for m, n being non zero 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 & X is open & f = g holds
( ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & g `| Y is_continuous_on Y ) )
proof end;

theorem Th29: :: PDIFF_9:29
for m, n being non zero 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 & g is_continuous_in x holds
( f + g is_continuous_in x & f - g is_continuous_in x )
proof end;

theorem Th30: :: PDIFF_9:30
for m, n being non zero 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
proof end;

theorem :: PDIFF_9:31
for m, n being non zero 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
proof end;

theorem Th32: :: PDIFF_9:32
for m, n being non zero 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
proof end;

theorem Th33: :: PDIFF_9:33
for m, n being non zero Element of NAT
for Z being set
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z & g is_continuous_on Z holds
( f + g is_continuous_on Z & f - g is_continuous_on Z )
proof end;

theorem Th34: :: PDIFF_9:34
for m, n being non zero 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
proof end;

theorem :: PDIFF_9:35
for m, n being non zero 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
proof end;

theorem Th36: :: 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 & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Element of REAL i st x in dom f & |.(x - x0).| < s holds
|.((f /. x) - (f /. x0)).| < r ) ) ) ) )
proof end;

theorem Th37: :: PDIFF_9:37
for m being non zero 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 )
proof end;

theorem :: PDIFF_9:38
for m being non zero 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 & g is_continuous_in x0 holds
( f + g is_continuous_in x0 & f - g is_continuous_in x0 )
proof end;

theorem :: PDIFF_9:39
for m being non zero 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
proof end;

theorem :: PDIFF_9:40
for m being non zero 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
proof end;

Lm3: 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 & x = y holds
( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) )
proof end;

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 & g is_continuous_in x holds
f (#) g is_continuous_in x
proof end;

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

:: deftheorem defines is_continuous_on PDIFF_9:def 2 :
for m being non zero 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 Th42: :: PDIFF_9:42
for m being non zero 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 & f is_continuous_on Z ) iff g is_continuous_on Z )
proof end;

theorem Th43: :: PDIFF_9:43
for m being non zero 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 & Z c= dom f holds
( f is_continuous_on Z iff for s being sequence of (REAL-NS m) st rng s c= Z & s is convergent & lim s in Z holds
( g /* s is convergent & g /. (lim s) = lim (g /* s) ) )
proof end;

theorem Th44: :: PDIFF_9:44
for m being non zero 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 & f is_continuous_on Z ) iff g is_continuous_on Z )
proof end;

theorem Th45: :: PDIFF_9:45
for m being non zero 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 & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
proof end;

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

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

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

theorem Th49: :: PDIFF_9:49
for m being non zero 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 & f is_continuous_on Z ) iff g is_continuous_on Z )
proof end;

theorem :: PDIFF_9:50
for m, n being non zero 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
proof end;

theorem Th51: :: PDIFF_9:51
for m being non zero 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 & g is_differentiable_in x holds
( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) & f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )
proof end;

theorem Th52: :: PDIFF_9:52
for m being non zero 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 & diff ((r (#) f),x) = r (#) (diff (f,x)) )
proof end;

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

:: deftheorem defines is_differentiable_on PDIFF_9:def 3 :
for Z being set
for m being non zero 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 Th53: :: PDIFF_9:53
for m being non zero 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 & f is_differentiable_on Z ) iff g is_differentiable_on Z )
proof end;

theorem Th54: :: PDIFF_9:54
for m being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X c= dom f & 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 )
proof end;

theorem Th55: :: PDIFF_9:55
for m being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X c= dom f & f is_differentiable_on X holds
X is open
proof end;

definition
let m be non zero Element of NAT ;
let Z be set ;
let f be PartFunc of (REAL m),REAL;
assume A1: Z c= dom f ;
func f `| Z -> PartFunc of (REAL m),(Funcs ((REAL m),REAL)) means :Def4: :: PDIFF_9:def 4
( dom it = Z & ( 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 & ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) st dom b1 = Z & ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) & dom b2 = Z & ( for x being Element of REAL m st x in Z holds
b2 /. x = diff (f,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines `| PDIFF_9:def 4 :
for m being non zero 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 & ( 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 zero 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 & X c= dom f & f is_differentiable_on X holds
( g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) )
proof end;

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

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

theorem :: PDIFF_9:59
for m being non zero 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 & f is_differentiable_on X holds
( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) )
proof end;

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

:: deftheorem defines is_partial_differentiable_on PDIFF_9:def 5 :
for m being non zero Element of NAT
for Z being set
for i being Nat
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( 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 zero Element of NAT ;
let Z be set ;
let i be Nat;
let f be PartFunc of (REAL m),REAL;
assume A1: f is_partial_differentiable_on Z,i ;
func f `partial| (Z,i) -> PartFunc of (REAL m),REAL means :Def6: :: PDIFF_9:def 6
( dom it = Z & ( 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 & ( for x being Element of REAL m st x in Z holds
b1 /. x = partdiff (f,x,i) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (REAL m),REAL st dom b1 = Z & ( for x being Element of REAL m st x in Z holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = Z & ( for x being Element of REAL m st x in Z holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines `partial| PDIFF_9:def 6 :
for m being non zero Element of NAT
for Z being set
for i being 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 & ( for x being Element of REAL m st x in Z holds
b5 /. x = partdiff (f,x,i) ) ) );

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

theorem Th61: :: PDIFF_9:61
for m being non zero 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)
for i being Nat st <>* f = g & X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i )
proof end;

theorem Th62: :: PDIFF_9:62
for m being non zero 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)
for i being Nat st <>* f = g & X is open & 1 <= i & i <= m & 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 )
proof end;

Lm4: for m being non zero 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)).|
proof end;

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

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

theorem Th64: :: PDIFF_9:64
for m being non zero 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 & g is_partial_differentiable_in x,i holds
( f (#) g is_partial_differentiable_in x,i & partdiff ((f (#) g),x,i) = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) )
proof end;

theorem Th65: :: PDIFF_9:65
for m being non zero 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 & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) & ( for 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)) ) )
proof end;

theorem Th66: :: PDIFF_9:66
for m being non zero 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 & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f - g is_partial_differentiable_on X,i & (f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i)) & ( for 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)) ) )
proof end;

theorem Th67: :: PDIFF_9:67
for m being non zero 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 & 1 <= i & i <= m & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )
proof end;

theorem Th68: :: PDIFF_9:68
for m being non zero 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 & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f (#) g is_partial_differentiable_on X,i & (f (#) g) `partial| (X,i) = ((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i))) & ( 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))) ) )
proof end;

definition
let m be non zero 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 :Def7: :: PDIFF_9:def 7
( it . 0 = f | Z & ( for i being Nat 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 | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `partial| (Z,(I /. (i + 1))) ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of (REAL m),REAL st b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `partial| (Z,(I /. (i + 1))) ) & b2 . 0 = f | Z & ( for i being Nat holds b2 . (i + 1) = (b2 . i) `partial| (Z,(I /. (i + 1))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines PartDiffSeq PDIFF_9:def 7 :
for m being non zero 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 | Z & ( for i being Nat holds b5 . (i + 1) = (b5 . i) `partial| (Z,(I /. (i + 1))) ) ) );

definition
let m be non zero Element of NAT ;
let Z be set ;
let I be FinSequence of NAT ;
let f be PartFunc of (REAL m),REAL;
pred f is_partial_differentiable_on Z,I means :: 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 defines is_partial_differentiable_on PDIFF_9:def 8 :
for m being non zero 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 zero Element of NAT ;
let Z be set ;
let I be FinSequence of NAT ;
let f be PartFunc of (REAL m),REAL;
func f `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 zero 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);

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

theorem Th69: :: PDIFF_9:69
for m being non zero Element of NAT
for Z being Subset of (REAL m)
for i being Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st Z is open & Z c= dom f & 1 <= i & i <= m & x in Z & f is_partial_differentiable_in x,i holds
( f | Z is_partial_differentiable_in x,i & partdiff (f,x,i) = partdiff ((f | Z),x,i) )
proof end;

theorem Th70: :: PDIFF_9:70
for m being non zero Element of NAT
for Z being set
for i being Nat
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i )
proof end;

definition
let m be non zero Element of NAT ;
let Z be set ;
let i be Nat;
let f be PartFunc of (REAL m),REAL;
redefine pred f is_partial_differentiable_on Z,i means :: PDIFF_9:def 10
f | Z is_partial_differentiable_on Z,i;
compatibility
( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i ) by Th70;
end;

:: deftheorem defines is_partial_differentiable_on PDIFF_9:def 10 :
for m being non zero Element of NAT
for Z being set
for i being Nat
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i );

theorem Th71: :: PDIFF_9:71
for m being non zero Element of NAT
for Z being Subset of (REAL m)
for i being Nat
for f being PartFunc of (REAL m),REAL st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,i) = (f | Z) `partial| (Z,i)
proof end;

theorem Th72: :: PDIFF_9:72
for m being non zero 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_on Z,I holds
(f `partial| (Z,I)) | Z = f `partial| (Z,I)
proof end;

theorem Th73: :: PDIFF_9:73
for m being non zero Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n)
proof end;

theorem Th74: :: PDIFF_9:74
for m being non zero 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 & rng I c= Seg m & f is_partial_differentiable_on X,I & 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) & (PartDiffSeq ((f + g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) + ((PartDiffSeq (g,X,I)) . i) )
proof end;

theorem Th75: :: PDIFF_9:75
for m being non zero 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 & rng I c= Seg m & f is_partial_differentiable_on X,I & g is_partial_differentiable_on X,I holds
( f + g is_partial_differentiable_on X,I & (f + g) `partial| (X,I) = (f `partial| (X,I)) + (g `partial| (X,I)) )
proof end;

theorem Th76: :: PDIFF_9:76
for m being non zero 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 & rng I c= Seg m & f is_partial_differentiable_on X,I & 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) & (PartDiffSeq ((f - g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) - ((PartDiffSeq (g,X,I)) . i) )
proof end;

theorem Th77: :: PDIFF_9:77
for m being non zero 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 & rng I c= Seg m & f is_partial_differentiable_on X,I & g is_partial_differentiable_on X,I holds
( f - g is_partial_differentiable_on X,I & (f - g) `partial| (X,I) = (f `partial| (X,I)) - (g `partial| (X,I)) )
proof end;

theorem Th78: :: PDIFF_9:78
for m being non zero 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 & rng I c= Seg m & 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) & (PartDiffSeq ((r (#) f),X,I)) . i = r (#) ((PartDiffSeq (f,X,I)) . i) )
proof end;

theorem Th79: :: PDIFF_9:79
for m being non zero 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 & rng I c= Seg m & f is_partial_differentiable_on X,I holds
( r (#) f is_partial_differentiable_on X,I & (r (#) f) `partial| (X,I) = r (#) (f `partial| (X,I)) )
proof end;

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

:: deftheorem defines is_partial_differentiable_up_to_order PDIFF_9:def 11 :
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for k being 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 & rng I c= Seg m holds
f is_partial_differentiable_on Z,I );

theorem Th80: :: PDIFF_9:80
for m being non zero 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 & f `partial| (Z,G) is_partial_differentiable_on Z,I ) )
proof end;

set Z0 = 0 ;

theorem Th81: :: PDIFF_9:81
for m being non zero 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 )
proof end;

definition
let m be non zero Element of NAT ;
let Z be set ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),REAL;
redefine pred f is_partial_differentiable_on Z,i means :: PDIFF_9:def 12
f is_partial_differentiable_on Z,<*i*>;
compatibility
( f is_partial_differentiable_on Z,i iff f is_partial_differentiable_on Z,<*i*> ) by Th81;
end;

:: deftheorem defines is_partial_differentiable_on PDIFF_9:def 12 :
for m being non zero 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 f is_partial_differentiable_on Z,<*i*> );

theorem Th82: :: PDIFF_9:82
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for Z being Subset of (REAL m)
for i being Element of NAT st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,<*i*>) = f `partial| (Z,i)
proof end;

theorem Th83: :: PDIFF_9:83
for m being non zero Element of NAT
for Z being set
for i, j being Nat
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 & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z
proof end;

theorem Th84: :: PDIFF_9:84
for m being non zero Element of NAT
for Z being set
for i, j being Nat
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,Z & j <= i holds
f is_partial_differentiable_up_to_order j,Z by XXREAL_0:2;

theorem :: PDIFF_9:85
for m being non zero 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 & f is_partial_differentiable_up_to_order i,X & g is_partial_differentiable_up_to_order i,X holds
( f + g is_partial_differentiable_up_to_order i,X & f - g is_partial_differentiable_up_to_order i,X )
proof end;

theorem :: PDIFF_9:86
for m being non zero 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 & f is_partial_differentiable_up_to_order i,X holds
r (#) f is_partial_differentiable_up_to_order i,X
proof end;

theorem :: PDIFF_9:87
for m being non zero 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 & g is_partial_differentiable_up_to_order i,X holds
f (#) g is_partial_differentiable_up_to_order i,X
proof end;

theorem :: PDIFF_9:88
for m being non zero Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
(f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I))
proof end;