:: 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-2021 Association of Mizar Users


registration
let n be Nat;
let p, q be Element of (TOP-REAL n);
let f, g be real-valued FinSequence;
identify p + 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;
let n be Nat;
let p be Element of (TOP-REAL n);
let f be real-valued FinSequence;
identify r * 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;
identify p - 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
proof end;

Lm2: for i, j being Nat st i <= j holds
i + (j -' i) = (i + j) -' i
proof end;

theorem Th1: :: PDIFF_7:1
for i, j being Nat st i <= j holds
(0* j) | i = 0* i
proof end;

theorem Th2: :: PDIFF_7:2
for i, j being Nat st i <= j holds
(0* j) | (i -' 1) = 0* (i -' 1)
proof end;

Lm3: for i, j being Nat st i <= j holds
(0* j) /^ i = 0* (j -' i)
proof end;

Lm4: for i, j being Nat st i > j holds
(0* j) /^ i = 0* (j -' i)
proof end;

theorem Th3: :: PDIFF_7:3
for i, j being Nat holds (0* j) /^ i = 0* (j -' i)
proof end;

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

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

theorem Th6: :: PDIFF_7:6
for m, i being 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)) & x - ((reproj (i,x)) . r) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r) )
proof end;

theorem Th7: :: PDIFF_7:7
for m, i being 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)) & x - ((reproj (i,x)) . p) = (reproj (i,(0. (REAL-NS m)))) . (((Proj (i,m)) . x) - p) )
proof end;

Lm5: for m being Nat
for nx being Point of (REAL-NS m)
for Z being Subset of (REAL-NS m)
for i being Nat st Z is open & nx in Z & 1 <= i & 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
proof end;

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

Lm6: for m being non zero Nat
for v being Element of REAL m
for x being Real
for i being Nat holds len (Replace (v,i,x)) = m
proof end;

Lm7: for m being non zero Nat
for x being Real
for i, j being Nat st 1 <= j & j <= m holds
( ( i = j implies (Replace ((0* m),i,x)) . j = x ) & ( i <> j implies (Replace ((0* m),i,x)) . j = 0 ) )
proof end;

theorem Th9: :: PDIFF_7:9
for m being non zero Nat
for x, y being Element of REAL
for i being Nat st 1 <= i & i <= m holds
Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))
proof end;

registration
let f be real-valued FinSequence;
let i be Nat;
let p be Real;
cluster f +* (i,p) -> real-valued ;
coherence
Replace (f,i,p) is real-valued
proof end;
end;

theorem Th10: :: PDIFF_7:10
for m being non zero Nat
for x, a being Real
for i being Nat st 1 <= i & i <= m holds
(0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))
proof end;

theorem Th11: :: PDIFF_7:11
for m being non zero Nat
for x being Element of REAL
for i being Nat st 1 <= i & i <= m & x <> 0 holds
Replace ((0* m),i,x) <> 0* m
proof end;

theorem Th12: :: PDIFF_7:12
for m being non zero Nat
for x, y being Element of REAL
for z being Element of REAL m
for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
proof end;

theorem Th13: :: PDIFF_7:13
for m being non zero Nat
for x, y being Element of REAL
for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0* m))) . (x + y) = ((reproj (i,(0* m))) . x) + ((reproj (i,(0* m))) . y)
proof end;

theorem Th14: :: PDIFF_7:14
for m being non zero Nat
for x, y being Point of (REAL-NS 1)
for i being Nat st 1 <= i & 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)
proof end;

theorem Th15: :: PDIFF_7:15
for m being non zero Nat
for x, a being Real
for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0* m))) . (a * x) = a (#) ((reproj (i,(0* m))) . x)
proof end;

theorem Th16: :: PDIFF_7:16
for m being non zero Nat
for x being Point of (REAL-NS 1)
for a being Real
for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)
proof end;

theorem Th17: :: PDIFF_7:17
for m being non zero Nat
for x being Element of REAL
for i being Nat st 1 <= i & i <= m & x <> 0 holds
(reproj (i,(0* m))) . x <> 0* m
proof end;

theorem Th18: :: PDIFF_7:18
for m being non zero Nat
for x being Point of (REAL-NS 1)
for i being Nat st 1 <= i & i <= m & x <> 0. (REAL-NS 1) holds
(reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m)
proof end;

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

theorem Th20: :: PDIFF_7:20
for m being non zero Nat
for x, y being Point of (REAL-NS 1)
for i being Nat
for z being Point of (REAL-NS m) st 1 <= i & i <= m & y = (Proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) )
proof end;

theorem Th21: :: PDIFF_7:21
for n, m being non zero Nat
for i being 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 & 1 <= i & i <= m holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj (i,(0. (REAL-NS m)))) )
proof end;

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

definition
let n be non zero Nat;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
pred f is_differentiable_in x means :: PDIFF_7:def 1
 <>* f is_differentiable_in x;
end;

:: deftheorem defines is_differentiable_in PDIFF_7:def 1 :
for n being non zero 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 zero 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 zero 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));

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

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

theorem Th24: :: PDIFF_7:24
for m being non zero Nat
for v, w, u being FinSequence of REAL m st dom v = dom w & u = v + w holds
Sum u = (Sum v) + (Sum w)
proof end;

theorem Th25: :: PDIFF_7:25
for m being non zero Nat
for r being Real
for w, u being FinSequence of REAL m st u = r (#) w holds
Sum u = r * (Sum w)
proof end;

Lm8: for m, n being non zero 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 & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
proof end;

theorem Th26: :: PDIFF_7:26
for n being non zero Nat
for h, g being FinSequence of REAL n st len h = (len g) + 1 & ( 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
proof end;

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

theorem Th28: :: PDIFF_7:28
for m, n being non zero 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 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )
proof end;

theorem Th29: :: PDIFF_7:29
for m being non zero Nat
for f being PartFunc of (REAL m),(REAL 1) ex f0 being PartFunc of (REAL m),REAL st f = <>* f0
proof end;

theorem Th30: :: PDIFF_7:30
for m, n being non zero 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 & x = x0 & f = f0 holds
f /. x = f0 /. x0
proof end;

definition
let m be non zero Nat;
let X be Subset of (REAL m);
attr X is open means :: PDIFF_7:def 3
 ex X0 being Subset of (REAL-NS m) st
( X0 = X & X0 is open );
end;

:: deftheorem defines open PDIFF_7:def 3 :
for m being non zero Nat
for X being Subset of (REAL m) holds
( X is open iff ex X0 being Subset of (REAL-NS m) st
( X0 = X & X0 is open ) );

theorem Th31: :: PDIFF_7:31
for m being non zero 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 & { y where y is Element of REAL m : |.(y - x).| < r } c= X ) )
proof end;

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

:: deftheorem defines is_partial_differentiable_on PDIFF_7:def 4 :
for m, n being non zero Nat
for i being 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 & ( 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 Nat
for X being set
for m, n being non zero 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) by XBOOLE_1:1;

theorem Th33: :: PDIFF_7:33
for m, n being non zero Nat
for i being 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 )
proof end;

theorem Th34: :: PDIFF_7:34
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st Z is open & 1 <= i & i <= m 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 is_partial_differentiable_in x,i ) ) )
proof end;

definition
let m, n be non zero Nat;
let i be Nat;
let f be PartFunc of (REAL m),(REAL n);
let X be set ;
assume A1: f is_partial_differentiable_on X,i ;
func f `partial| (X,i) -> PartFunc of (REAL m),(REAL n) means :Def5: :: PDIFF_7:def 5
( dom it = X & ( 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 & ( for x being Element of REAL m st x in X holds
b1 /. x = partdiff (f,x,i) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (REAL m),(REAL n) st dom b1 = X & ( for x being Element of REAL m st x in X holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = X & ( for x being Element of REAL m st x in X holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines `partial| PDIFF_7:def 5 :
for m, n being non zero Nat
for i being 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 & ( for x being Element of REAL m st x in X holds
b6 /. x = partdiff (f,x,i) ) ) );

definition
let m, n be non zero Nat;
let f be PartFunc of (REAL m),(REAL n);
let x0 be Element of REAL m;
pred f is_continuous_in x0 means :: 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 & f = g & g is_continuous_in y0 );
end;

:: deftheorem defines is_continuous_in PDIFF_7:def 6 :
for m, n being non zero 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 & f = g & g is_continuous_in y0 ) );

theorem :: PDIFF_7:35
for m, n being non zero 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 & x = y holds
( f is_continuous_in x iff g is_continuous_in y ) ;

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

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

:: deftheorem defines is_continuous_on PDIFF_7:def 7 :
for m, n being non zero 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 & ( 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 zero 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 )
proof end;

theorem Th38: :: PDIFF_7:38
for m, n being non zero 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 & ( 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
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proof end;

theorem Th39: :: PDIFF_7:39
for m being non zero Nat
for x, y being Element of REAL m
for i being Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds
(proj (i,m)) . y = xi
proof end;

theorem Th40: :: PDIFF_7:40
for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x, y being Element of REAL m
for i being Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
proof end;

theorem Th41: :: PDIFF_7:41
for m being non zero 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 Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,y,i)
proof end;

theorem Th42: :: PDIFF_7:42
for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for p, q being Real
for x being Element of REAL m
for i being Nat st 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of 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.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
proof end;

theorem Th43: :: PDIFF_7:43
for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for p, q being Real
for x being Element of REAL m
for i being Nat st 1 <= i & i <= m & p <= q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of 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.] & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
proof end;

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

theorem Th45: :: PDIFF_7:45
for m being non zero 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 Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
proof end;

theorem Th46: :: PDIFF_7:46
for m being non zero Nat
for h being FinSequence of REAL m
for y, x being Element of REAL m
for j being Nat st len h = m + 1 & 1 <= j & j <= m & ( 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))
proof end;

theorem Th47: :: PDIFF_7:47
for m being non zero 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 & x in X & ( 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 ) ) holds
( f is_differentiable_in x & ( for h being Element of REAL m ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & (diff (f,x)) . h = Sum w ) ) )
proof end;

theorem Th48: :: PDIFF_7:48
for m being non zero 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 & x in X & ( 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 ) ) holds
( f is_differentiable_in x & ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) )
proof end;

theorem :: PDIFF_7:49
for m being non zero 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 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 & f `| X is_continuous_on X ) )
proof end;