:: The Differentiable Functions from $\mathbbR$ into ${\mathbbR}^n$
:: by Keiko Narita , Artur Korni\l owicz and Yasunari Shidama
::
:: Received September 28, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:45;

set ZR = [#] REAL;

Lm1:  the carrier of (REAL-NS 1) = REAL 1
by REAL_NS1:def_4;

theorem Th1: :: NDIFF_4:1
for m being Element of NAT
for f1, f2 being PartFunc of REAL,(REAL m) holds f1 - f2 = f1 + (- f2)
proofend;

definition
let n be non empty Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let x be real number ;
predf is_differentiable_in x means :Def1: :: NDIFF_4:def 1
 ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_differentiable_in x );
end;

:: deftheorem Def1 defines is_differentiable_in NDIFF_4:def_1_:_
 for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for x being real number holds
( f is_differentiable_in x iff ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_differentiable_in x ) );

theorem Th2: :: NDIFF_4:2
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n)
for x being real number st h = f holds
( f is_differentiable_in x iff h is_differentiable_in x )
proofend;

definition
let n be non empty Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let x be real number ;
func diff (f,x) ->  Element of REAL n means :Def2: :: NDIFF_4:def 2
 ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & it = diff (g,x) );
existence
 ex b1 being Element of REAL n ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & b1 = diff (g,x) )
proofend;
uniqueness
 for b1, b2 being Element of REAL n st ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & b1 = diff (g,x) ) & ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & b2 = diff (g,x) ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines diff NDIFF_4:def_2_:_
 for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for x being real number
for b4 being Element of REAL n holds
( b4 = diff (f,x) iff ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & b4 = diff (g,x) ) );

theorem Th3: :: NDIFF_4:3
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n)
for x being real number st h = f holds
diff (f,x) = diff (h,x)
proofend;

definition
let n be non empty Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let X be set ;
predf is_differentiable_on X means :Def3: :: NDIFF_4:def 3
( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def3 defines is_differentiable_on NDIFF_4:def_3_:_
 for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) );

theorem Th4: :: NDIFF_4:4
for X being set
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds
X is Subset of REAL
proofend;

theorem Th5: :: NDIFF_4:5
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
proofend;

theorem Th6: :: NDIFF_4:6
for n being non empty Element of NAT
for Y being Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds
Y is open
proofend;

definition
let n be non empty Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X ->  PartFunc of REAL,(REAL n) means :Def4: :: NDIFF_4:def 4
( dom it = X & ( for x being Real st x in X holds
it . x = diff (f,x) ) );
existence
 ex b1 being PartFunc of REAL,(REAL n) st
( dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff (f,x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of REAL,(REAL n) st dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff (f,x) ) & dom b2 = X & ( for x being Real st x in X holds
b2 . x = diff (f,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines `| NDIFF_4:def_4_:_
 for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for X being set st f is_differentiable_on X holds
for b4 being PartFunc of REAL,(REAL n) holds
( b4 = f `| X iff ( dom b4 = X & ( for x being Real st x in X holds
b4 . x = diff (f,x) ) ) );

theorem :: NDIFF_4:7
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0* n ) )
proofend;

theorem :: NDIFF_4:8
for n being non empty Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n)
for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
proofend;

theorem Th9: :: NDIFF_4:9
for x0, r being Real
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
proofend;

theorem Th10: :: NDIFF_4:10
for x0 being Real
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds
( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) )
proofend;

theorem Th11: :: NDIFF_4:11
for x0 being Real
for n being non empty Element of NAT
for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
proofend;

theorem :: NDIFF_4:12
for x0 being Real
for n being non empty Element of NAT
for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
proofend;

theorem Th13: :: NDIFF_4:13
for r being Real
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
proofend;

theorem Th14: :: NDIFF_4:14
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds
( - f is_differentiable_on Z & ( for x being Real st x in Z holds
((- f) `| Z) . x = - (diff (f,x)) ) )
proofend;

theorem Th15: :: NDIFF_4:15
for n being non empty Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,(REAL n) st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )
proofend;

theorem :: NDIFF_4:16
for n being non empty Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,(REAL n) st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )
proofend;

theorem :: NDIFF_4:17
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st Z c= dom f & f | Z is constant holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0* n ) )
proofend;

theorem Th18: :: NDIFF_4:18
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
proofend;

theorem :: NDIFF_4:19
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
proofend;

theorem :: NDIFF_4:20
for X being set
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds
f | X is continuous
proofend;

theorem Th21: :: NDIFF_4:21
for X being set
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
proofend;

definition
let n be non empty Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is differentiable  means :Def5: :: NDIFF_4:def 5
f is_differentiable_on dom f;
end;

:: deftheorem Def5 defines differentiable NDIFF_4:def_5_:_
 for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is differentiable iff f is_differentiable_on dom f );

registration
let n be non empty Element of NAT ;
clusterREAL --> (0* n) ->  differentiable for Function of REAL,(REAL n);
coherence
 for b1 being Function of REAL,(REAL n) st b1 = REAL --> (0* n) holds
b1 is differentiable
proofend;
end;

registration
let n be non empty Element of NAT ;
cluster non empty Relation-like REAL -defined REAL n -valued Function-like total quasi_total V239() V240() V241() differentiable for Element of K6(K7(REAL,(REAL n)));
existence
 ex b1 being Function of REAL,(REAL n) st b1 is differentiable
proofend;
end;

theorem :: NDIFF_4:22
for n being non empty Element of NAT
for Z being open Subset of REAL
for f being differentiable PartFunc of REAL,(REAL n) st Z c= dom f holds
f is_differentiable_on Z
proofend;

theorem Th23: :: NDIFF_4:23
for n being non empty Element of NAT
for R being PartFunc of REAL,(REAL-NS n) st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 &amp; ( for z being Real st z <> 0 &amp; |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) )
proofend;

theorem Th24: :: NDIFF_4:24
for i being Element of NAT
for n being non empty Element of NAT
for g being PartFunc of REAL,(REAL-NS n)
for x0 being real number st 1 <= i &amp; i <= n &amp; g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 &amp; (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
proofend;

theorem Th25: :: NDIFF_4:25
for n being non empty Element of NAT
for g being PartFunc of REAL,(REAL-NS n)
for x0 being real number holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i &amp; i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
proofend;

theorem :: NDIFF_4:26
for i being Element of NAT
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being real number st 1 <= i &amp; i <= n &amp; f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 &amp; (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
proofend;

theorem :: NDIFF_4:27
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being real number holds
( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i &amp; i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 )
proofend;

theorem Th28: :: NDIFF_4:28
for X being set
for i being Element of NAT
for n being non empty Element of NAT
for g being PartFunc of REAL,(REAL-NS n) st 1 <= i &amp; i <= n &amp; g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X &amp; (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
proofend;

theorem Th29: :: NDIFF_4:29
for X being set
for i being Element of NAT
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st 1 <= i &amp; i <= n &amp; f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X &amp; (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
proofend;

theorem Th30: :: NDIFF_4:30
for X being set
for n being non empty Element of NAT
for g being PartFunc of REAL,(REAL-NS n) holds
( g is_differentiable_on X iff for i being Element of NAT st 1 <= i &amp; i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
proofend;

theorem :: NDIFF_4:31
for X being set
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is_differentiable_on X iff for i being Element of NAT st 1 <= i &amp; i <= n holds
(Proj (i,n)) * f is_differentiable_on X )
proofend;

theorem Th32: :: NDIFF_4:32
for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds
J is_continuous_in x0
proofend;

theorem Th33: :: NDIFF_4:33
for x0 being Real
for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
I is_continuous_in x0
proofend;

theorem Th34: :: NDIFF_4:34
for S, T being RealNormSpace
for f1 being PartFunc of S,REAL
for f2 being PartFunc of REAL,T
for x0 being Point of S st x0 in dom (f2 * f1) &amp; f1 is_continuous_in x0 &amp; f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proofend;

Lm2:  ( dom (proj (1,1)) = REAL 1 &amp; rng (proj (1,1)) = REAL &amp; ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x &amp; ((proj (1,1)) ") . x = <*x*> ) ) )
proofend;

theorem :: NDIFF_4:35
for n being non empty Element of NAT
for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) &amp; x0 in dom f &amp; y0 in dom g &amp; x0 = <*y0*> &amp; f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
proofend;

theorem :: NDIFF_4:36
for n being non empty Element of NAT
for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " &amp; x0 in dom f &amp; y0 in dom g &amp; x0 = <*y0*> &amp; f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
proofend;

theorem :: NDIFF_4:37
for x0 being Real
for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( I is_differentiable_in x0 &amp; diff (I,x0) = <*1*> )
proofend;

definition
let n be non empty Element of NAT ;
let f be PartFunc of (REAL-NS n),REAL;
let x be Point of (REAL-NS n);
predf is_differentiable_in x means :Def6: :: NDIFF_4:def 6
 ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g &amp; x = y &amp; g is_differentiable_in y );
end;

:: deftheorem Def6 defines is_differentiable_in NDIFF_4:def_6_:_
 for n being non empty Element of NAT
for f being PartFunc of (REAL-NS n),REAL
for x being Point of (REAL-NS n) holds
( f is_differentiable_in x iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g &amp; x = y &amp; g is_differentiable_in y ) );

definition
let n be non empty Element of NAT ;
let f be PartFunc of (REAL-NS n),REAL;
let x be Point of (REAL-NS n);
func diff (f,x) ->  Function of (REAL-NS n),REAL means :Def7: :: NDIFF_4:def 7
 ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g &amp; x = y &amp; it = diff (g,y) );
existence
 ex b1 being Function of (REAL-NS n),REAL ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g &amp; x = y &amp; b1 = diff (g,y) )
proofend;
uniqueness
 for b1, b2 being Function of (REAL-NS n),REAL st ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g &amp; x = y &amp; b1 = diff (g,y) ) &amp; ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g &amp; x = y &amp; b2 = diff (g,y) ) holds
b1 = b2 ;
end;

:: deftheorem Def7 defines diff NDIFF_4:def_7_:_
 for n being non empty Element of NAT
for f being PartFunc of (REAL-NS n),REAL
for x being Point of (REAL-NS n)
for b4 being Function of (REAL-NS n),REAL holds
( b4 = diff (f,x) iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g &amp; x = y &amp; b4 = diff (g,y) ) );

theorem Th38: :: NDIFF_4:38
for J being Function of (REAL 1),REAL
for x0 being Element of REAL 1 st J = proj (1,1) holds
( J is_differentiable_in x0 &amp; diff (J,x0) = J )
proofend;

theorem :: NDIFF_4:39
for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds
( J is_differentiable_in x0 &amp; diff (J,x0) = J )
proofend;

theorem Th40: :: NDIFF_4:40
for n being non empty Element of NAT
for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) &amp; ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )
proofend;

theorem Th41: :: NDIFF_4:41
for n being non empty Element of NAT
for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) &amp; ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) )
proofend;

theorem Th42: :: NDIFF_4:42
for n being non empty Element of NAT
for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " &amp; x0 in dom f &amp; y0 in dom g &amp; x0 = <*y0*> &amp; f * I = g &amp; f is_differentiable_in x0 holds
( g is_differentiable_in y0 &amp; diff (g,y0) = (diff (f,x0)) . <*1*> &amp; ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
proofend;

theorem Th43: :: NDIFF_4:43
for n being non empty Element of NAT
for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " &amp; x0 in dom f &amp; y0 in dom g &amp; x0 = <*y0*> &amp; f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
proofend;

theorem Th44: :: NDIFF_4:44
for n being non empty Element of NAT
for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) &amp; x0 in dom f &amp; y0 in dom g &amp; x0 = <*y0*> &amp; f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
proofend;

theorem :: NDIFF_4:45
for n being non empty Element of NAT
for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) &amp; x0 in dom f &amp; y0 in dom g &amp; x0 = <*y0*> &amp; f = g * J &amp; g is_differentiable_in y0 holds
( f is_differentiable_in x0 &amp; diff (g,y0) = (diff (f,x0)) . <*1*> &amp; ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
proofend;

theorem Th46: :: NDIFF_4:46
for n being non empty Element of NAT
for R being RestFunc of (REAL-NS n) st R /. 0 = 0. (REAL-NS n) holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
proofend;

theorem Th47: :: NDIFF_4:47
for n, m being non empty Element of NAT
for R being RestFunc of (REAL-NS n)
for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)
proofend;

theorem Th48: :: NDIFF_4:48
for n, m being non empty Element of NAT
for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds
for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
proofend;

theorem Th49: :: NDIFF_4:49
for n, m being non empty Element of NAT
for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds
for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L1 being LinearFunc of (REAL-NS n)
for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)
proofend;

theorem :: NDIFF_4:50
for n, m being non empty Element of NAT
for x0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds
for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 &amp; diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
proofend;