:: Partial Differentiation of Vector-Valued Functions on $n$-Dimensional Real Normed Linear Spaces
:: by Takao Inou\'e , Adam Naumowicz , Noboru Endou and Yasunari Shidama
::
:: Received April 22, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

registration
let n be Nat;
let p, q be Element of (TOP-REAL n);
let f, g be real-valued FinSequence;
identifyp + q with f + g when p = f, q = g;
compatibility
 ( p = f & q = g implies p + q = f + g ) ;
end;

registration
let r, s be real number ;
let n be Nat;
let p be Element of (TOP-REAL n);
let f be real-valued FinSequence;
identifyr * p with s * f when r = s, p = f;
compatibility
 ( r = s & p = f implies r * p = s * f ) ;
end;

registration
let n be Nat;
let p be Element of (TOP-REAL n);
let f be real-valued FinSequence;
identify - p with  - f when p = f;
compatibility
 ( p = f implies - p = - f ) ;
end;

registration
let n be Nat;
let p, q be Element of (TOP-REAL n);
let f, g be real-valued FinSequence;
identifyp - q with f - g when p = f, q = g;
compatibility
 ( p = f & q = g implies p - q = f - g ) ;
end;

Lm1:  for S being RealNormSpace
for x being Point of S
for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x
proofend;

Lm2:  for i, j being Element of NAT st i <= j holds
i + (j -' i) = (i + j) -' i
proofend;

theorem Th1: :: PDIFF_7:1
for i, j being Element of NAT st i <= j holds
(0* j) | i = 0* i
proofend;

theorem Th2: :: PDIFF_7:2
for i, j being Element of NAT st i <= j holds
(0* j) | (i -' 1) = 0* (i -' 1)
proofend;

Lm3:  for i, j being Element of NAT st i <= j holds
(0* j) /^ i = 0* (j -' i)
proofend;

Lm4:  for i, j being Element of NAT st i > j holds
(0* j) /^ i = 0* (j -' i)
proofend;

theorem Th3: :: PDIFF_7:3
for j, i being Element of NAT holds (0* j) /^ i = 0* (j -' i)
proofend;

theorem :: PDIFF_7:4
for i, j being Element of NAT holds
( ( i <= j implies (0* j) | (i -' 1) = 0* (i -' 1) ) &amp; (0* j) /^ i = 0* (j -' i) ) by Th2, Th3;

theorem Th5: :: PDIFF_7:5
for i, j being Element of NAT
for xi being Element of (REAL-NS 1) st 1 <= i &amp; i <= j holds
||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = ||.xi.||
proofend;

theorem Th6: :: PDIFF_7:6
for m, i being Element of NAT
for x being Element of REAL m
for r being Real holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x)) &amp; x - ((reproj (i,x)) . r) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r) )
proofend;

theorem Th7: :: PDIFF_7:7
for m, i being Element of NAT
for x being Point of (REAL-NS m)
for p being Point of (REAL-NS 1) holds
( ((reproj (i,x)) . p) - x = (reproj (i,(0. (REAL-NS m)))) . (p - ((Proj (i,m)) . x)) &amp; x - ((reproj (i,x)) . p) = (reproj (i,(0. (REAL-NS m)))) . (((Proj (i,m)) . x) - p) )
proofend;

Lm5:  for m being Element of NAT
for nx being Point of (REAL-NS m)
for Z being Subset of (REAL-NS m)
for i being Element of NAT st Z is open &amp; nx in Z &amp; 1 <= i &amp; i <= m holds
ex N being Neighbourhood of (Proj (i,m)) . nx st
for z being Point of (REAL-NS 1) st z in N holds
(reproj (i,nx)) . z in Z
proofend;

theorem Th8: :: PDIFF_7:8
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being Subset of (REAL-NS m) st Z is open &amp; 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f &amp; ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
proofend;

Lm6:  for m being non empty Element of NAT
for v being Element of REAL m
for x being Element of REAL
for i being Element of NAT holds len (Replace (v,i,x)) = m
proofend;

Lm7:  for m being non empty Element of NAT
for x being Element of REAL
for i, j being Element of NAT st 1 <= j &amp; j <= m holds
( ( i = j implies (Replace ((0* m),i,x)) . j = x ) &amp; ( i <> j implies (Replace ((0* m),i,x)) . j = 0 ) )
proofend;

theorem Th9: :: PDIFF_7:9
for m being non empty Element of NAT
for x, y being Element of REAL
for i being Element of NAT st 1 <= i &amp; i <= m holds
Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))
proofend;

theorem Th10: :: PDIFF_7:10
for m being non empty Element of NAT
for x, a being Element of REAL
for i being Element of NAT st 1 <= i &amp; i <= m holds
Replace ((0* m),i,(a * x)) = a * (Replace ((0* m),i,x))
proofend;

theorem Th11: :: PDIFF_7:11
for m being non empty Element of NAT
for x being Element of REAL
for i being Element of NAT st 1 <= i &amp; i <= m &amp; x <> 0 holds
Replace ((0* m),i,x) <> 0* m
proofend;

theorem Th12: :: PDIFF_7:12
for m being non empty Element of NAT
for x, y being Element of REAL
for z being Element of REAL m
for i being Element of NAT st 1 <= i &amp; i <= m &amp; y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = Replace ((0* m),i,(x - y)) &amp; z - (Replace (z,i,x)) = Replace ((0* m),i,(y - x)) )
proofend;

theorem Th13: :: PDIFF_7:13
for m being non empty Element of NAT
for x, y being Element of REAL
for i being Element of NAT st 1 <= i &amp; i <= m holds
(reproj (i,(0* m))) . (x + y) = ((reproj (i,(0* m))) . x) + ((reproj (i,(0* m))) . y)
proofend;

theorem Th14: :: PDIFF_7:14
for m being non empty Element of NAT
for x, y being Point of (REAL-NS 1)
for i being Element of NAT st 1 <= i &amp; i <= m holds
(reproj (i,(0. (REAL-NS m)))) . (x + y) = ((reproj (i,(0. (REAL-NS m)))) . x) + ((reproj (i,(0. (REAL-NS m)))) . y)
proofend;

theorem Th15: :: PDIFF_7:15
for m being non empty Element of NAT
for x, a being Element of REAL
for i being Element of NAT st 1 <= i &amp; i <= m holds
(reproj (i,(0* m))) . (a * x) = a * ((reproj (i,(0* m))) . x)
proofend;

theorem Th16: :: PDIFF_7:16
for m being non empty Element of NAT
for x being Point of (REAL-NS 1)
for a being Element of REAL
for i being Element of NAT st 1 <= i &amp; i <= m holds
(reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)
proofend;

theorem Th17: :: PDIFF_7:17
for m being non empty Element of NAT
for x being Element of REAL
for i being Element of NAT st 1 <= i &amp; i <= m &amp; x <> 0 holds
(reproj (i,(0* m))) . x <> 0* m
proofend;

theorem Th18: :: PDIFF_7:18
for m being non empty Element of NAT
for x being Point of (REAL-NS 1)
for i being Element of NAT st 1 <= i &amp; i <= m &amp; x <> 0. (REAL-NS 1) holds
(reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m)
proofend;

theorem Th19: :: PDIFF_7:19
for m being non empty Element of NAT
for x, y being Element of REAL
for z being Element of REAL m
for i being Element of NAT st 1 <= i &amp; i <= m &amp; y = (proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0* m))) . (x - y) &amp; z - ((reproj (i,z)) . x) = (reproj (i,(0* m))) . (y - x) )
proofend;

theorem Th20: :: PDIFF_7:20
for m being non empty Element of NAT
for x, y being Point of (REAL-NS 1)
for i being Element of NAT
for z being Point of (REAL-NS m) st 1 <= i &amp; i <= m &amp; y = (Proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) &amp; z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) )
proofend;

theorem Th21: :: PDIFF_7:21
for n, m being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_differentiable_in x &amp; 1 <= i &amp; i <= m holds
( f is_partial_differentiable_in x,i &amp; partdiff (f,x,i) = (diff (f,x)) * (reproj (i,(0. (REAL-NS m)))) )
proofend;

theorem Th22: :: PDIFF_7:22
for n, m being non empty Element of NAT
for i being Element of NAT
for g being PartFunc of (REAL m),(REAL n)
for y being Element of REAL m st g is_differentiable_in y &amp; 1 <= i &amp; i <= m holds
( g is_partial_differentiable_in y,i &amp; partdiff (g,y,i) = ((diff (g,y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> )
proofend;

definition
let n be non empty Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
predf is_differentiable_in x means :Def1: :: PDIFF_7:def 1
 <>* f is_differentiable_in x;
end;

:: deftheorem Def1 defines is_differentiable_in PDIFF_7:def_1_:_
 for n being non empty Element of NAT
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds
( f is_differentiable_in x iff <>* f is_differentiable_in x );

definition
let n be non empty Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
func diff (f,x) ->  Function of (REAL n),REAL equals :: PDIFF_7:def 2
(proj (1,1)) * (diff ((<>* f),x));
coherence
 (proj (1,1)) * (diff ((<>* f),x)) is Function of (REAL n),REAL ;
end;

:: deftheorem  defines diff PDIFF_7:def_2_:_
 for n being non empty Element of NAT
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds diff (f,x) = (proj (1,1)) * (diff ((<>* f),x));

theorem :: PDIFF_7:23
for m being non empty Element of NAT
for i being Element of NAT
for h being PartFunc of (REAL m),REAL
for y being Element of REAL m st h is_differentiable_in y &amp; 1 <= i &amp; i <= m holds
( h is_partial_differentiable_in y,i &amp; partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) &amp; partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) )
proofend;

theorem Th24: :: PDIFF_7:24
for m being non empty Element of NAT
for v, w, u being FinSequence of REAL m st dom v = dom w &amp; u = v + w holds
Sum u = (Sum v) + (Sum w)
proofend;

theorem Th25: :: PDIFF_7:25
for m being non empty Element of NAT
for r being Real
for w, u being FinSequence of REAL m st u = r (#) w holds
Sum u = r * (Sum w)
proofend;

Lm8:  for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m ex L being Lipschitzian LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m &amp; ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) &amp; L . h = Sum w )
proofend;

theorem Th26: :: PDIFF_7:26
for n being non empty Element of NAT
for h, g being FinSequence of REAL n st len h = (len g) + 1 &amp; ( for i being Nat st i in dom g holds
g /. i = (h /. i) - (h /. (i + 1)) ) holds
(h /. 1) - (h /. (len h)) = Sum g
proofend;

theorem Th27: :: PDIFF_7:27
for n being non empty Element of NAT
for h, g, j being FinSequence of REAL n st len h = len j &amp; len g = len j &amp; ( for i being Nat st i in dom j holds
j /. i = (h /. i) - (g /. i) ) holds
Sum j = (Sum h) - (Sum g)
proofend;

theorem Th28: :: PDIFF_7:28
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x, y being Element of REAL m ex h being FinSequence of REAL m ex g being FinSequence of REAL n st
( len h = m + 1 &amp; len g = m &amp; ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) &amp; ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) &amp; ( for i being Nat
for hi being Element of REAL m st i in dom h &amp; h /. i = hi holds
|.hi.| <= |.y.| ) &amp; (f /. (x + y)) - (f /. x) = Sum g )
proofend;

theorem Th29: :: PDIFF_7:29
for m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL 1) ex f0 being PartFunc of (REAL m),REAL st f = <>* f0
proofend;

theorem Th30: :: PDIFF_7:30
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for f0 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for x0 being Element of (REAL-NS m) st x in dom f &amp; x = x0 &amp; f = f0 holds
f /. x = f0 /. x0
proofend;

definition
let m be non empty Element of NAT ;
let X be Subset of (REAL m);
attrX is open  means :Def3: :: PDIFF_7:def 3
 ex X0 being Subset of (REAL-NS m) st
( X0 = X &amp; X0 is open );
end;

:: deftheorem Def3 defines open PDIFF_7:def_3_:_
 for m being non empty Element of NAT
for X being Subset of (REAL m) holds
( X is open iff ex X0 being Subset of (REAL-NS m) st
( X0 = X &amp; X0 is open ) );

theorem Th31: :: PDIFF_7:31
for m being non empty Element of NAT
for X being Subset of (REAL m) holds
( X is open iff for x being Element of REAL m st x in X holds
ex r being Real st
( r > 0 &amp;  {  y where y is Element of REAL m : |.(y - x).| < r  }  c= X ) )
proofend;

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

:: deftheorem Def4 defines is_partial_differentiable_on PDIFF_7:def_4_:_
 for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f &amp; ( for x being Element of REAL m st x in X holds
f | X is_partial_differentiable_in x,i ) ) );

theorem Th32: :: PDIFF_7:32
for i being Element of NAT
for X being set
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL m)
proofend;

theorem Th33: :: PDIFF_7:33
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being set st f = g holds
( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i )
proofend;

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

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

:: deftheorem Def5 defines `partial| PDIFF_7:def_5_:_
 for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for X being set st f is_partial_differentiable_on X,i holds
for b6 being PartFunc of (REAL m),(REAL n) holds
( b6 = f `partial| (X,i) iff ( dom b6 = X &amp; ( for x being Element of REAL m st x in X holds
b6 /. x = partdiff (f,x,i) ) ) );

definition
let m, n be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x0 be Element of REAL m;
predf is_continuous_in x0 means :Def6: :: PDIFF_7:def 6
 ex y0 being Point of (REAL-NS m) ex g being PartFunc of (REAL-NS m),(REAL-NS n) st
( x0 = y0 &amp; f = g &amp; g is_continuous_in y0 );
end;

:: deftheorem Def6 defines is_continuous_in PDIFF_7:def_6_:_
 for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff ex y0 being Point of (REAL-NS m) ex g being PartFunc of (REAL-NS m),(REAL-NS n) st
( x0 = y0 &amp; f = g &amp; g is_continuous_in y0 ) );

theorem Th35: :: PDIFF_7:35
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g &amp; x = y holds
( f is_continuous_in x iff g is_continuous_in y )
proofend;

theorem :: PDIFF_7:36
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Element of REAL m st x1 in dom f &amp; |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proofend;

definition
let m, n be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let X be set ;
predf is_continuous_on X means :Def7: :: PDIFF_7:def 7
( X c= dom f &amp; ( for x0 being Element of REAL m st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def7 defines is_continuous_on PDIFF_7:def_7_:_
 for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for X being set holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Element of REAL m st x0 in X holds
f | X is_continuous_in x0 ) ) );

theorem Th37: :: PDIFF_7:37
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set st f = g holds
( f is_continuous_on X iff g is_continuous_on X )
proofend;

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

theorem Th39: :: PDIFF_7:39
for m being non empty Element of NAT
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i &amp; i <= m &amp; y = (reproj (i,x)) . xi holds
(proj (i,m)) . y = xi
proofend;

theorem Th40: :: PDIFF_7:40
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i &amp; i <= m &amp; y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
proofend;

theorem Th41: :: PDIFF_7:41
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for g being PartFunc of REAL,REAL
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i &amp; i <= m &amp; y = (reproj (i,x)) . xi &amp; g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,y,i)
proofend;

theorem Th42: :: PDIFF_7:42
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for p, q being Real
for x being Element of REAL m
for i being Element of NAT st 1 <= i &amp; i <= m &amp; p < q &amp; ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) &amp; ( for h being Real st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ &amp; y = (reproj (i,x)) . r &amp; (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
proofend;

theorem Th43: :: PDIFF_7:43
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for p, q being Real
for x being Element of REAL m
for i being Element of NAT st 1 <= i &amp; i <= m &amp; p <= q &amp; ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) &amp; ( for h being Real st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in [.p,q.] &amp; y = (reproj (i,x)) . r &amp; (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
proofend;

theorem Th44: :: PDIFF_7:44
for m being non empty Element of NAT
for x, y, z, w being Element of REAL m
for i being Element of NAT
for d, p, q, r being Real st 1 <= i &amp; i <= m &amp; |.(y - x).| < d &amp; |.(z - x).| < d &amp; p = (proj (i,m)) . y &amp; z = (reproj (i,y)) . q &amp; r in [.p,q.] &amp; w = (reproj (i,y)) . r holds
|.(w - x).| < d
proofend;

theorem Th45: :: PDIFF_7:45
for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for X being Subset of (REAL m)
for x, y, z being Element of REAL m
for i being Element of NAT
for d, p, q being Real st 1 <= i &amp; i <= m &amp; X is open &amp; x in X &amp; |.(y - x).| < d &amp; |.(z - x).| < d &amp; X c= dom f &amp; ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) &amp; 0 < d &amp; ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) &amp; z = (reproj (i,y)) . p &amp; q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d &amp; f is_partial_differentiable_in w,i &amp; (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
proofend;

theorem Th46: :: PDIFF_7:46
for m being non empty Element of NAT
for h being FinSequence of REAL m
for y, x being Element of REAL m
for j being Element of NAT st len h = m + 1 &amp; 1 <= j &amp; j <= m &amp; ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) holds
x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y))
proofend;

theorem Th47: :: PDIFF_7:47
for m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL 1)
for X being Subset of (REAL m)
for x being Element of REAL m st X is open &amp; x in X &amp; ( for i being Element of NAT st 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) ) holds
( f is_differentiable_in x &amp; ( for h being Element of REAL m ex w being FinSequence of REAL 1 st
( dom w = Seg m &amp; ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) &amp; (diff (f,x)) . h = Sum w ) ) )
proofend;

theorem Th48: :: PDIFF_7:48
for m being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS 1)
for X being Subset of (REAL-NS m)
for x being Point of (REAL-NS m) st X is open &amp; x in X &amp; ( for i being Element of NAT st 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) ) holds
( f is_differentiable_in x &amp; ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m &amp; ( for i being Element of NAT st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) &amp; (diff (f,x)) . h = Sum w ) ) )
proofend;

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