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

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

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

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

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)*> )

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

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)

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.|

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

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.|

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)

for x being Element of REAL j holds x = (reproj (i,x)) . ((proj (i,j)) . x)

proof end;

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 ;

ex b_{1} being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) st

( dom b_{1} = Z & ( for x being Element of REAL m st x in Z holds

b_{1} /. x = diff (f,x) ) )

for b_{1}, b_{2} being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) st dom b_{1} = Z & ( for x being Element of REAL m st x in Z holds

b_{1} /. x = diff (f,x) ) & dom b_{2} = Z & ( for x being Element of REAL m st x in Z holds

b_{2} /. x = diff (f,x) ) holds

b_{1} = b_{2}

end;
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 ( dom it = Z & ( for x being Element of REAL m st x in Z holds

it /. x = diff (f,x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) holds

( b_{5} = f `| Z iff ( dom b_{5} = Z & ( for x being Element of REAL m st x in Z holds

b_{5} /. x = diff (f,x) ) ) );

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 b

( b

b

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

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

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

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.|| ) )

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.|| )

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.||

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*>

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)).||

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

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

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.| ) ) ) ) )

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.| ) ) ) ) )

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

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

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 )

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

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

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

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 )

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

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

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

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 )

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 )

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

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

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

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;

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

for x0 being Element of REAL m st x0 in Z holds

f | Z is_continuous_in x0;

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

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 )

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

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 )

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

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 )

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

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

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 )

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

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

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

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;

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

for x being Element of REAL m st x in Z holds

f | Z is_differentiable_in x;

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

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 )

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 )

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

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 ;

ex b_{1} being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) st

( dom b_{1} = Z & ( for x being Element of REAL m st x in Z holds

b_{1} /. x = diff (f,x) ) )

for b_{1}, b_{2} being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) st dom b_{1} = Z & ( for x being Element of REAL m st x in Z holds

b_{1} /. x = diff (f,x) ) & dom b_{2} = Z & ( for x being Element of REAL m st x in Z holds

b_{2} /. x = diff (f,x) ) holds

b_{1} = b_{2}

end;
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 ( dom it = Z & ( for x being Element of REAL m st x in Z holds

it /. x = diff (f,x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) holds

( b_{4} = f `| Z iff ( dom b_{4} = Z & ( for x being Element of REAL m st x in Z holds

b_{4} /. x = diff (f,x) ) ) );

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 b

( b

b

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

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

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

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

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;

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

( Z c= dom f & ( for x being Element of REAL m st x in Z holds

f | Z is_partial_differentiable_in x,i ) );

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

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 ;

ex b_{1} being PartFunc of (REAL m),REAL st

( dom b_{1} = Z & ( for x being Element of REAL m st x in Z holds

b_{1} /. x = partdiff (f,x,i) ) )

for b_{1}, b_{2} being PartFunc of (REAL m),REAL st dom b_{1} = Z & ( for x being Element of REAL m st x in Z holds

b_{1} /. x = partdiff (f,x,i) ) & dom b_{2} = Z & ( for x being Element of REAL m st x in Z holds

b_{2} /. x = partdiff (f,x,i) ) holds

b_{1} = b_{2}

end;
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 ( dom it = Z & ( for x being Element of REAL m st x in Z holds

it /. x = partdiff (f,x,i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being PartFunc of (REAL m),REAL holds

( b_{5} = f `partial| (Z,i) iff ( dom b_{5} = Z & ( for x being Element of REAL m st x in Z holds

b_{5} /. x = partdiff (f,x,i) ) ) );

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 b

( b

b

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

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 )

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 )

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.| ) ) ) ) )

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

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

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

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

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

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;

ex b_{1} being Functional_Sequence of (REAL m),REAL st

( b_{1} . 0 = f | Z & ( for i being Nat holds b_{1} . (i + 1) = (b_{1} . i) `partial| (Z,(I /. (i + 1))) ) )

for b_{1}, b_{2} being Functional_Sequence of (REAL m),REAL st b_{1} . 0 = f | Z & ( for i being Nat holds b_{1} . (i + 1) = (b_{1} . i) `partial| (Z,(I /. (i + 1))) ) & b_{2} . 0 = f | Z & ( for i being Nat holds b_{2} . (i + 1) = (b_{2} . i) `partial| (Z,(I /. (i + 1))) ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (it . i) `partial| (Z,(I /. (i + 1))) ) );

ex b

( b

proof end;

uniqueness for b

b

proof 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 b_{5} being Functional_Sequence of (REAL m),REAL holds

( b_{5} = PartDiffSeq (f,Z,I) iff ( b_{5} . 0 = f | Z & ( for i being Nat holds b_{5} . (i + 1) = (b_{5} . i) `partial| (Z,(I /. (i + 1))) ) ) );

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 b

( b

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;

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

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

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

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;

coherence

(PartDiffSeq (f,Z,I)) . (len I) is PartFunc of (REAL m),REAL;

;

end;
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 (PartDiffSeq (f,Z,I)) . (len I);

coherence

(PartDiffSeq (f,Z,I)) . (len I) is PartFunc of (REAL m),REAL;

;

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

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

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 )

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;

( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i ) by Th70;

end;
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 | Z is_partial_differentiable_on Z,i;

( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i ) by Th70;

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

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)

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)

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)

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

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

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

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

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

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

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 ;

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

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;

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

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

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 )

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;

( f is_partial_differentiable_on Z,i iff f is_partial_differentiable_on Z,<*i*> ) by Th81;

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

( f is_partial_differentiable_on Z,i iff f is_partial_differentiable_on Z,<*i*> ) by Th81;

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

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)

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

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;

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 )

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

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

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

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;