:: NDIFF_4 semantic presentation

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)
proof
let m be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL m) holds f1 - f2 = f1 + (- f2)
let f1, f2 be PartFunc of REAL,(REAL m); ::_thesis: f1 - f2 = f1 + (- f2)
A1: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def_46;
A2: dom (f1 + (- f2)) = (dom f1) /\ (dom (- f2)) by VALUED_2:def_45;
A3: dom (- f2) = dom f2 by NFCONT_4:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_._x_=_(f1_+_(-_f2))_._x
let x be set ; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (f1 + (- f2)) . x )
assume A4: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (f1 + (- f2)) . x
then A5: x in dom f2 by A1, XBOOLE_0:def_4;
then A6: ( f2 . x = f2 /. x & (- f2) . x = (- f2) /. x ) by A3, PARTFUN1:def_6;
thus (f1 - f2) . x = (f1 . x) - (f2 . x) by A4, VALUED_2:def_46
.= (f1 . x) + ((- f2) . x) by A3, A5, A6, NFCONT_4:def_3
.= (f1 + (- f2)) . x by A1, A2, A3, A4, VALUED_2:def_45 ; ::_thesis: verum
end;
hence  f1 - f2 = f1 + (- f2) by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
end;

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 )
proof
let n be non empty Element of NAT ; ::_thesis: 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 )
let f be PartFunc of REAL,(REAL n); ::_thesis: 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 )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: for x being real number st h = f holds
( f is_differentiable_in x iff h is_differentiable_in x )
let x be real number ; ::_thesis: ( h = f implies ( f is_differentiable_in x iff h is_differentiable_in x ) )
assume A1: h = f ; ::_thesis: ( f is_differentiable_in x iff h is_differentiable_in x )
hereby  ::_thesis: ( h is_differentiable_in x implies f is_differentiable_in x )
assume  f is_differentiable_in x ; ::_thesis: h is_differentiable_in x
then  ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_differentiable_in x ) by Def1;
hence  h is_differentiable_in x by A1; ::_thesis: verum
end;
thus  ( h is_differentiable_in x implies f is_differentiable_in x ) by A1, Def1; ::_thesis: verum
end;

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) )
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 diff (g,x) is Element of REAL n by REAL_NS1:def_4;
hence  ex b1 being Element of REAL n ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & b1 = diff (g,x) ) ; ::_thesis: verum
end;
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)
proof
let n be non empty Element of NAT ; ::_thesis: 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)
let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n)
for x being real number st h = f holds
diff (f,x) = diff (h,x)
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: for x being real number st h = f holds
diff (f,x) = diff (h,x)
let x be real number ; ::_thesis: ( h = f implies diff (f,x) = diff (h,x) )
 ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & diff (f,x) = diff (g,x) ) by Def2;
hence  ( h = f implies diff (f,x) = diff (h,x) ) ; ::_thesis: verum
end;

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
proof
let X be set ; ::_thesis: 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
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds
X is Subset of REAL
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X implies X is Subset of REAL )
assume  f is_differentiable_on X ; ::_thesis: X is Subset of REAL
then  X c= dom f by Def3;
hence  X is Subset of REAL by XBOOLE_1:1; ::_thesis: verum
end;

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 ) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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 ) ) )
let Z be open Subset of REAL; ::_thesis: 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 ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
thus  ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )
proof
assume A1: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) )
A2: Z c= dom g by A1, Def3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
g_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies g | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: g | Z is_differentiable_in x
then  f | Z is_differentiable_in x by A1, Def3;
hence  g | Z is_differentiable_in x by Th2; ::_thesis: verum
end;
then A3: g is_differentiable_on Z by A2, NDIFF_3:def_5;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies f is_differentiable_in x )
assume  x in Z ; ::_thesis: f is_differentiable_in x
then  g is_differentiable_in x by A3, NDIFF_3:10;
hence  f is_differentiable_in x by Def1; ::_thesis: verum
end;
hence  ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) by A1, Def3; ::_thesis: verum
end;
assume A4: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) ; ::_thesis: f is_differentiable_on Z
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
g_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies g is_differentiable_in x )
assume  x in Z ; ::_thesis: g is_differentiable_in x
then  f is_differentiable_in x by A4;
hence  g is_differentiable_in x by Th2; ::_thesis: verum
end;
then A5: g is_differentiable_on Z by A4, NDIFF_3:10;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: f | Z is_differentiable_in x
then  g | Z is_differentiable_in x by A5, NDIFF_3:def_5;
hence  f | Z is_differentiable_in x by Def1; ::_thesis: verum
end;
hence  f is_differentiable_on Z by A4, Def3; ::_thesis: verum
end;

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
proof
let n be non empty Element of NAT ; ::_thesis: for Y being Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds
Y is open
let Y be Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds
Y is open
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on Y implies Y is open )
assume A1: f is_differentiable_on Y ; ::_thesis: Y is open
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: Y c= dom g by A1, Def3;
now__::_thesis:_for_x_being_Real_st_x_in_Y_holds_
g_|_Y_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Y implies g | Y is_differentiable_in x )
assume  x in Y ; ::_thesis: g | Y is_differentiable_in x
then  f | Y is_differentiable_in x by A1, Def3;
hence  g | Y is_differentiable_in x by Th2; ::_thesis: verum
end;
then  g is_differentiable_on Y by A2, NDIFF_3:def_5;
hence  Y is open by NDIFF_3:11; ::_thesis: verum
end;

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) ) )
proof
deffunc H1( Real) ->  Element of REAL n = diff (f,$1);
defpred S1[ set ] means $1 in X;
consider F0 being PartFunc of REAL,(REAL n) such that
A2: ( ( for x being Real holds
( x in dom F0 iff S1[x] ) ) & ( for x being Real st x in dom F0 holds
F0 . x = H1(x) ) ) from SEQ_1:sch_3();
take  F0 ; ::_thesis: ( dom F0 = X & ( for x being Real st x in X holds
F0 . x = diff (f,x) ) )
now__::_thesis:_for_y_being_set_st_y_in_X_holds_
y_in_dom_F0
A3: X is Subset of REAL by A1, Th4;
let y be set ; ::_thesis: ( y in X implies y in dom F0 )
assume  y in X ; ::_thesis: y in dom F0
hence  y in dom F0 by A2, A3; ::_thesis: verum
end;
then A4: X c= dom F0 by TARSKI:def_3;
 for y being set st y in dom F0 holds
y in X by A2;
then  dom F0 c= X by TARSKI:def_3;
hence  dom F0 = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Real st x in X holds
F0 . x = diff (f,x)
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
F0_._x_=_diff_(f,x)
let x be Real; ::_thesis: ( x in X implies F0 . x = diff (f,x) )
assume  x in X ; ::_thesis: F0 . x = diff (f,x)
then  x in dom F0 by A2;
hence  F0 . x = diff (f,x) by A2; ::_thesis: verum
end;
hence  for x being Real st x in X holds
F0 . x = diff (f,x) ; ::_thesis: verum
end;
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
proof
let F0, G0 be PartFunc of REAL,(REAL n); ::_thesis: ( dom F0 = X & ( for x being Real st x in X holds
F0 . x = diff (f,x) ) & dom G0 = X & ( for x being Real st x in X holds
G0 . x = diff (f,x) ) implies F0 = G0 )
assume that
A5: dom F0 = X and
A6: for x being Real st x in X holds
F0 . x = diff (f,x) and
A7: dom G0 = X and
A8: for x being Real st x in X holds
G0 . x = diff (f,x) ; ::_thesis: F0 = G0
now__::_thesis:_for_x_being_Real_st_x_in_dom_F0_holds_
F0_._x_=_G0_._x
let x be Real; ::_thesis: ( x in dom F0 implies F0 . x = G0 . x )
assume A9: x in dom F0 ; ::_thesis: F0 . x = G0 . x
then  F0 . x = diff (f,x) by A5, A6;
hence  F0 . x = G0 . x by A5, A8, A9; ::_thesis: verum
end;
hence  F0 = G0 by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
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 ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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 ) )
let Z be open Subset of REAL; ::_thesis: 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 ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & ex r being Element of REAL n st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0* n ) ) )
assume A1: Z c= dom f ; ::_thesis: ( for r being Element of REAL n holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0* n ) ) )
given r being Element of REAL n such that A2: rng f = {r} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0* n ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A3: r is Point of (REAL-NS n) by REAL_NS1:def_4;
then A4: ( g is_differentiable_on Z & ( for x being Real st x in Z holds
(g `| Z) /. x = 0. (REAL-NS n) ) ) by A1, A2, NDIFF_3:12;
A5: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: f | Z is_differentiable_in x
then  g | Z is_differentiable_in x by A4, NDIFF_3:def_5;
hence  f | Z is_differentiable_in x by Def1; ::_thesis: verum
end;
then A6: f is_differentiable_on Z by A1, Def3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(f_`|_Z)_/._x_=_0*_n
let x be Real; ::_thesis: ( x in Z implies (f `| Z) /. x = 0* n )
assume A7: x in Z ; ::_thesis: (f `| Z) /. x = 0* n
then A8: (g `| Z) /. x = 0. (REAL-NS n) by A3, A1, A2, NDIFF_3:12;
 x in dom (g `| Z) by A4, A7, NDIFF_3:def_6;
then A9: (g `| Z) . x = 0. (REAL-NS n) by A8, PARTFUN1:def_6;
A10: (g `| Z) . x = diff (g,x) by A7, A4, NDIFF_3:def_6;
A11: (f `| Z) . x = diff (f,x) by A7, A6, Def4;
 diff (f,x) = diff (g,x) by Th3;
then A12: (f `| Z) . x = 0* n by A9, A10, A11, REAL_NS1:def_4;
 x in dom (f `| Z) by A6, Def4, A7;
hence  (f `| Z) /. x = 0* n by A12, PARTFUN1:def_6; ::_thesis: verum
end;
hence  ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0* n ) ) by A5, A1, Def3; ::_thesis: verum
end;

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))) )
proof
let n be non empty Element of NAT ; ::_thesis: 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))) )
let x0 be real number ; ::_thesis: 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))) )
let f be PartFunc of REAL,(REAL n); ::_thesis: 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))) )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: 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))) )
let N be Neighbourhood of x0; ::_thesis: ( f = g & f is_differentiable_in x0 & N c= dom f implies 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))) ) )
assume that
A1: f = g and
A2: f is_differentiable_in x0 and
A3: N c= dom f ; ::_thesis: 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))) )
A4: g is_differentiable_in x0 by A1, A2, Th2;
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: 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))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) )
assume  ( rng c = {x0} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
then  ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (g,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) by A4, A1, A3, NDIFF_3:13;
hence  ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) by A1, Th3; ::_thesis: verum
end;

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)) )
proof
let x0, r be Real; ::_thesis: 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)) )
let n be non empty Element of NAT ; ::_thesis: 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)) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) )
assume  f is_differentiable_in x0 ; ::_thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_differentiable_in x0 ) by Def1;
A2: ( r (#) g is_differentiable_in x0 & diff ((r (#) g),x0) = r * (diff (g,x0)) ) by A1, NDIFF_3:16;
A3: r (#) f = r (#) g by A1, NFCONT_4:6;
A4: diff (f,x0) = diff (g,x0) by A1, Th3;
 diff ((r (#) f),x0) = diff ((r (#) g),x0) by A1, Th3, NFCONT_4:6;
hence  ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by A3, A2, Def1, A4, REAL_NS1:3; ::_thesis: verum
end;

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)) )
proof
let x0 be Real; ::_thesis: 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)) )
let n be non empty Element of NAT ; ::_thesis: 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)) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_in x0 implies ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) )
 (- 1) (#) f = - f by NFCONT_4:7;
hence  ( f is_differentiable_in x0 implies ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) ) by Th9; ::_thesis: verum
end;

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)) )
proof
let x0 be Real; ::_thesis: 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)) )
let n be non empty Element of NAT ; ::_thesis: 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)) )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) )
assume A1: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) ; ::_thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
consider g1 being PartFunc of REAL,(REAL-NS n) such that
A2: ( f1 = g1 & g1 is_differentiable_in x0 ) by A1, Def1;
consider g2 being PartFunc of REAL,(REAL-NS n) such that
A3: ( f2 = g2 & g2 is_differentiable_in x0 ) by A1, Def1;
A4: ( g1 + g2 is_differentiable_in x0 & diff ((g1 + g2),x0) = (diff (g1,x0)) + (diff (g2,x0)) ) by A2, A3, NDIFF_3:14;
A5: f1 + f2 = g1 + g2 by A2, A3, NFCONT_4:5;
A6: ( diff (f1,x0) = diff (g1,x0) & diff (f2,x0) = diff (g2,x0) ) by A2, A3, Th3;
 diff ((f1 + f2),x0) = diff ((g1 + g2),x0) by A2, A3, Th3, NFCONT_4:5;
hence  ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) by A5, A4, Def1, A6, REAL_NS1:2; ::_thesis: verum
end;

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)) )
proof
let x0 be Real; ::_thesis: 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)) )
let n be non empty Element of NAT ; ::_thesis: 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)) )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) )
A1: f1 - f2 = f1 + (- f2) by Th1;
assume A2: f1 is_differentiable_in x0 ; ::_thesis: ( not f2 is_differentiable_in x0 or ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) )
assume  f2 is_differentiable_in x0 ; ::_thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
then  ( - f2 is_differentiable_in x0 & diff ((- f2),x0) = - (diff (f2,x0)) ) by Th10;
hence  ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) by A1, A2, Th11; ::_thesis: verum
end;

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)) ) )
proof
let r be Real; ::_thesis: 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)) ) )
let n be non empty Element of NAT ; ::_thesis: 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)) ) )
let Z be open Subset of REAL; ::_thesis: 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)) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) )
assume that
A1: Z c= dom f and
A2: f is_differentiable_on Z ; ::_thesis: ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A3: dom f = dom (r (#) f) by VALUED_2:def_39;
A4: r (#) f = r (#) g by NFCONT_4:6;
A5: Z c= dom (r (#) g) by A3, A1, NFCONT_4:6;
A6: Z c= dom g by A2, Def3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
g_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies g | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: g | Z is_differentiable_in x
then  f | Z is_differentiable_in x by A2, Def3;
hence  g | Z is_differentiable_in x by Th2; ::_thesis: verum
end;
then  g is_differentiable_on Z by A6, NDIFF_3:def_5;
then A7: ( r (#) g is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) g) `| Z) . x = r * (diff (g,x)) ) ) by A5, NDIFF_3:19;
A8: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(r_(#)_f)_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies (r (#) f) | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: (r (#) f) | Z is_differentiable_in x
then  (r (#) g) | Z is_differentiable_in x by A7, NDIFF_3:def_5;
hence  (r (#) f) | Z is_differentiable_in x by A4, Def1; ::_thesis: verum
end;
then A9: r (#) f is_differentiable_on Z by A3, A1, Def3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((r_(#)_f)_`|_Z)_._x_=_r_*_(diff_(f,x))
let x be Real; ::_thesis: ( x in Z implies ((r (#) f) `| Z) . x = r * (diff (f,x)) )
assume A10: x in Z ; ::_thesis: ((r (#) f) `| Z) . x = r * (diff (f,x))
then  f is_differentiable_in x by A2, Th5;
then  ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r * (diff (f,x)) ) by Th9;
hence  ((r (#) f) `| Z) . x = r * (diff (f,x)) by A10, A9, Def4; ::_thesis: verum
end;
hence  ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) by A3, A8, A1, Def3; ::_thesis: verum
end;

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)) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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)) ) )
let Z be open Subset of REAL; ::_thesis: 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)) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & f is_differentiable_on Z implies ( - f is_differentiable_on Z & ( for x being Real st x in Z holds
((- f) `| Z) . x = - (diff (f,x)) ) ) )
 (- 1) (#) f = - f by NFCONT_4:7;
hence  ( Z c= dom f & f is_differentiable_on Z implies ( - f is_differentiable_on Z & ( for x being Real st x in Z holds
((- f) `| Z) . x = - (diff (f,x)) ) ) ) by Th13; ::_thesis: verum
end;

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)) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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)) ) )
let Z be open Subset of REAL; ::_thesis: 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)) ) )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( 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)) ) ) )
assume that
A1: Z c= dom (f1 + f2) and
A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( 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)) ) )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A3: f1 + f2 = g1 + g2 by NFCONT_4:5;
A4: Z c= dom (g1 + g2) by A1, NFCONT_4:5;
A5: ( Z c= dom g1 & Z c= dom g2 ) by A2, Def3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
g1_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies g1 | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: g1 | Z is_differentiable_in x
then  f1 | Z is_differentiable_in x by A2, Def3;
hence  g1 | Z is_differentiable_in x by Th2; ::_thesis: verum
end;
then A6: g1 is_differentiable_on Z by A5, NDIFF_3:def_5;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
g2_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies g2 | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: g2 | Z is_differentiable_in x
then  f2 | Z is_differentiable_in x by A2, Def3;
hence  g2 | Z is_differentiable_in x by Th2; ::_thesis: verum
end;
then  g2 is_differentiable_on Z by A5, NDIFF_3:def_5;
then A7: ( g1 + g2 is_differentiable_on Z & ( for x being Real st x in Z holds
((g1 + g2) `| Z) . x = (diff (g1,x)) + (diff (g2,x)) ) ) by A4, A6, NDIFF_3:17;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(f1_+_f2)_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies (f1 + f2) | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: (f1 + f2) | Z is_differentiable_in x
then  (g1 + g2) | Z is_differentiable_in x by A7, NDIFF_3:def_5;
hence  (f1 + f2) | Z is_differentiable_in x by A3, Def1; ::_thesis: verum
end;
hence A8: f1 + f2 is_differentiable_on Z by A1, Def3; ::_thesis: for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) )
assume A9: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
then  ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th5;
then  ( f1 + f2 is_differentiable_in x & diff ((f1 + f2),x) = (diff (f1,x)) + (diff (f2,x)) ) by Th11;
hence  ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A9, A8, Def4; ::_thesis: verum
end;

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)) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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)) ) )
let Z be open Subset of REAL; ::_thesis: 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)) ) )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( 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)) ) ) )
A1: f1 - f2 = f1 + (- f2) by Th1;
A2: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def_46;
assume that
A3: Z c= dom (f1 - f2) and
A4: f1 is_differentiable_on Z and
A5: f2 is_differentiable_on Z ; ::_thesis: ( 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)) ) )
 Z c= dom f2 by A3, A2, XBOOLE_1:18;
then A6: - f2 is_differentiable_on Z by A5, Th14;
hence  f1 - f2 is_differentiable_on Z by A1, A3, A4, Th15; ::_thesis: for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x))
let x be Real; ::_thesis: ( x in Z implies ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) )
assume A7: x in Z ; ::_thesis: ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x))
then A8: f2 is_differentiable_in x by A5, Th5;
thus ((f1 - f2) `| Z) . x = (diff (f1,x)) + (diff ((- f2),x)) by A1, A3, A4, A6, A7, Th15
.= (diff (f1,x)) - (diff (f2,x)) by A8, Th10 ; ::_thesis: verum
end;

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 ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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 ) )
let Z be open Subset of REAL; ::_thesis: 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 ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0* n ) ) )
assume that
A1: Z c= dom f and
A2: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0* n ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A3: g | Z is constant by A2;
then A4: ( g is_differentiable_on Z & ( for x being Real st x in Z holds
(g `| Z) . x = 0. (REAL-NS n) ) ) by A1, NDIFF_3:20;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: f | Z is_differentiable_in x
then  g | Z is_differentiable_in x by A4, NDIFF_3:def_5;
hence  f | Z is_differentiable_in x by Def1; ::_thesis: verum
end;
hence A5: f is_differentiable_on Z by A1, Def3; ::_thesis: for x being Real st x in Z holds
(f `| Z) . x = 0* n
let x be Real; ::_thesis: ( x in Z implies (f `| Z) . x = 0* n )
assume A6: x in Z ; ::_thesis: (f `| Z) . x = 0* n
then A7: (g `| Z) . x = 0. (REAL-NS n) by A3, A1, NDIFF_3:20;
A8: (g `| Z) . x = diff (g,x) by A6, A4, NDIFF_3:def_6;
A9: (f `| Z) . x = diff (f,x) by A6, A5, Def4;
 diff (f,x) = diff (g,x) by Th3;
hence  (f `| Z) . x = 0* n by A7, A8, A9, REAL_NS1:def_4; ::_thesis: verum
end;

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 ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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 ) )
let Z be open Subset of REAL; ::_thesis: 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 ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: 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 ) )
let r, p be Element of REAL n; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) ) )
assume that
A1: Z c= dom f and
A2: for x being Real st x in Z holds
f /. x = (x * r) + p ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
reconsider r1 = r, p1 = p as Point of (REAL-NS n) by REAL_NS1:def_4;
A3: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
g_/._x_=_(x_*_r1)_+_p1
let x be Real; ::_thesis: ( x in Z implies g /. x = (x * r1) + p1 )
assume  x in Z ; ::_thesis: g /. x = (x * r1) + p1
then A4: f /. x = (x * r) + p by A2;
A5: f /. x = g /. x by REAL_NS1:def_4;
 x * r = x * r1 by REAL_NS1:3;
hence  g /. x = (x * r1) + p1 by A4, A5, REAL_NS1:2; ::_thesis: verum
end;
then A6: ( g is_differentiable_on Z & ( for x being Real st x in Z holds
(g `| Z) . x = r1 ) ) by A1, NDIFF_3:21;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: f | Z is_differentiable_in x
then  g | Z is_differentiable_in x by A6, NDIFF_3:def_5;
hence  f | Z is_differentiable_in x by Def1; ::_thesis: verum
end;
hence A7: f is_differentiable_on Z by A1, Def3; ::_thesis: for x being Real st x in Z holds
(f `| Z) . x = r
let x be Real; ::_thesis: ( x in Z implies (f `| Z) . x = r )
assume A8: x in Z ; ::_thesis: (f `| Z) . x = r
then A9: (g `| Z) . x = diff (g,x) by A6, NDIFF_3:def_6;
A10: (f `| Z) . x = diff (f,x) by A8, A7, Def4;
 diff (f,x) = diff (g,x) by Th3;
hence  (f `| Z) . x = r by A8, A3, A1, A9, A10, NDIFF_3:21; ::_thesis: verum
end;

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
proof
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Real; ::_thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume  f is_differentiable_in x0 ; ::_thesis: f is_continuous_in x0
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_differentiable_in x0 ) by Def1;
 g is_continuous_in x0 by A1, NDIFF_3:22;
hence  f is_continuous_in x0 by A1, NFCONT_4:def_1; ::_thesis: verum
end;

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
proof
let X be set ; ::_thesis: 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
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds
f | X is continuous
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X implies f | X is continuous )
assume A1: f is_differentiable_on X ; ::_thesis: f | X is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: X c= dom g by A1, Def3;
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
g_|_X_is_differentiable_in_x
let x be Real; ::_thesis: ( x in X implies g | X is_differentiable_in x )
assume  x in X ; ::_thesis: g | X is_differentiable_in x
then  f | X is_differentiable_in x by A1, Def3;
hence  g | X is_differentiable_in x by Th2; ::_thesis: verum
end;
then  g is_differentiable_on X by A2, NDIFF_3:def_5;
then  g | X is continuous by NDIFF_3:23;
hence  f | X is continuous by NFCONT_4:23; ::_thesis: verum
end;

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
proof
let X be set ; ::_thesis: 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
let n be non empty Element of NAT ; ::_thesis: 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
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )
assume A1: ( f is_differentiable_on X & Z c= X ) ; ::_thesis: f is_differentiable_on Z
then A2: ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) by Def3;
A3: Z c= dom f by A1, A2, XBOOLE_1:1;
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
g_|_X_is_differentiable_in_x
let x be Real; ::_thesis: ( x in X implies g | X is_differentiable_in x )
assume  x in X ; ::_thesis: g | X is_differentiable_in x
then  f | X is_differentiable_in x by A1, Def3;
hence  g | X is_differentiable_in x by Th2; ::_thesis: verum
end;
then  g is_differentiable_on X by A2, NDIFF_3:def_5;
then A4: g is_differentiable_on Z by A1, NDIFF_3:24;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_|_Z_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x )
assume  x in Z ; ::_thesis: f | Z is_differentiable_in x
then  g | Z is_differentiable_in x by A4, NDIFF_3:def_5;
hence  f | Z is_differentiable_in x by Def1; ::_thesis: verum
end;
hence  f is_differentiable_on Z by A3, Def3; ::_thesis: verum
end;

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
proof
set f = REAL --> (0* n);
A1: [#] REAL = dom (REAL --> (0* n)) by FUNCT_2:def_1;
now__::_thesis:_for_x_being_Real_st_x_in_[#]_REAL_holds_
(REAL_-->_(0*_n))_/._x_=_(x_*_(0*_n))_+_(0*_n)
let x be Real; ::_thesis: ( x in [#] REAL implies (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n) )
assume  x in [#] REAL ; ::_thesis: (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n)
A2: (REAL --> (0* n)) /. x = 0* n by FUNCOP_1:7
.= 0. (TOP-REAL n) by EUCLID:70
.= x * (0. (TOP-REAL n)) by EUCLID:28
.= (x * (0. (TOP-REAL n))) + (0. (TOP-REAL n)) by EUCLID:27 ;
A3: x * (0. (TOP-REAL n)) = x (#) (0* n) by EUCLID:65, EUCLID:70;
 0. (TOP-REAL n) = 0* n by EUCLID:70;
hence  (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n) by A2, A3, EUCLID:64; ::_thesis: verum
end;
then  REAL --> (0* n) is_differentiable_on [#] REAL by A1, Th18;
hence  for b1 being Function of REAL,(REAL n) st b1 = REAL --> (0* n) holds
b1 is differentiable by A1, Def5; ::_thesis: verum
end;
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
proof
take  REAL --> (0* n) ; ::_thesis: REAL --> (0* n) is differentiable
thus  REAL --> (0* n) is differentiable ; ::_thesis: verum
end;
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
proof
let n be non empty Element of NAT ; ::_thesis: 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
let Z be open Subset of REAL; ::_thesis: for f being differentiable PartFunc of REAL,(REAL n) st Z c= dom f holds
f is_differentiable_on Z
let f be differentiable PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f implies f is_differentiable_on Z )
 f is_differentiable_on dom f by Def5;
hence  ( Z c= dom f implies f is_differentiable_on Z ) by Th21; ::_thesis: verum
end;


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 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) )
let R be PartFunc of REAL,(REAL-NS n); ::_thesis: ( R is total implies ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) ) )
assume A1: R is total ; ::_thesis: ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) )
A2: now__::_thesis:_(_R_is_RestFunc-like_&_ex_r_being_Real_st_
(_r_>_0_&_(_for_d_being_Real_holds_
(_not_d_>_0_or_ex_z_being_Real_st_
(_z_<>_0_&_|.z.|_<_d_&_not_(|.z.|_")_*_||.(R_/._z).||_<_r_)_)_)_)_implies_for_r_being_Real_st_r_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_z_being_Real_st_z_<>_0_&_|.z.|_<_d_holds_
(|.z.|_")_*_||.(R_/._z).||_<_r_)_)_)
assume A3: R is RestFunc-like ; ::_thesis: ( ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Real st
( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ) ) ) implies for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) )
assume  ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Real st
( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ) ) ) ; ::_thesis: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
then consider r being Real such that
A4: r > 0 and
A5: for d being Real st d > 0 holds
ex z being Real st
( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ;
defpred S1[ Element of NAT , Real] means ( $2 <> 0 & |.$2.| < 1 / ($1 + 1) & not (|.$2.| ") * ||.(R /. $2).|| < r );
A6: for n being Element of NAT ex z being Real st S1[n,z]
proof
let n be Element of NAT ; ::_thesis: ex z being Real st S1[n,z]
 1 / (n + 1) is Real by XREAL_0:def_1;
hence  ex z being Real st S1[n,z] by A5; ::_thesis: verum
end;
consider s being Real_Sequence such that
A7: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch_3(A6);
A8: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((s_._m)_-_0).|_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - 0).| < p )
assume A9: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - 0).| < p
consider n being Element of NAT  such that
A10: p " < n by SEQ_4:3;
reconsider q0 = 0 , q1 = 1 as real number ;
 (p ") + q0 < n + q1 by A10, XREAL_1:8;
then A11: 1 / (n + 1) < 1 / (p ") by A9, XREAL_1:76;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.((s . m) - 0).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s . m) - 0).| < p )
assume  n <= m ; ::_thesis: |.((s . m) - 0).| < p
then A12: n + 1 <= m + 1 by XREAL_1:6;
 1 / (m + 1) <= 1 / (n + 1) by A12, XREAL_1:118;
then  |.((s . m) - 0).| < 1 / (n + 1) by A7, XXREAL_0:2;
hence  |.((s . m) - 0).| < p by A11, XXREAL_0:2; ::_thesis: verum
end;
A13: s is convergent by A8, SEQ_2:def_6;
then A14: lim s = 0 by A8, SEQ_2:def_7;
 s is non-zero by A7, SEQ_1:5;
then reconsider s = s as non-zero 0 -convergent Real_Sequence by A13, A14, FDIFF_1:def_1;
 ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) ) by A3, NDIFF_3:def_1;
then consider n0 being Element of NAT  such that
A15: for m being Element of NAT st n0 <= m holds
||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A4, NORMSP_1:def_7;
A16: ||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| < r by A15;
A17: ||.(((s . n0) ") * (R /. (s . n0))).|| = (abs ((s . n0) ")) * ||.(R /. (s . n0)).|| by NORMSP_1:def_1
.= (|.(s . n0).| ") * ||.(R /. (s . n0)).|| by COMPLEX1:66 ;
 dom R = REAL by A1, PARTFUN1:def_2;
then A18: rng s c= dom R ;
||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| = ||.(((s ") (#) (R /* s)) . n0).|| by RLVECT_1:13
.= ||.(((s ") . n0) * ((R /* s) . n0)).|| by NDIFF_1:def_2
.= ||.(((s . n0) ") * ((R /* s) . n0)).|| by VALUED_1:10
.= ||.(((s . n0) ") * (R /. (s . n0))).|| by A18, FUNCT_2:109 ;
hence  for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) by A7, A16, A17; ::_thesis: verum
end;
now__::_thesis:_(_(_for_r_being_Real_st_r_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_z_being_Real_st_z_<>_0_&_|.z.|_<_d_holds_
(|.z.|_")_*_||.(R_/._z).||_<_r_)_)_)_implies_R_is_RestFunc-like_)
assume A19: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) ; ::_thesis: R is RestFunc-like
now__::_thesis:_for_s_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(s_")_(#)_(R_/*_s)_is_convergent_&_lim_((s_")_(#)_(R_/*_s))_=_0._(REAL-NS_n)_)
let s be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) )
A20: ( s is convergent & lim s = 0 ) ;
A21: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_n0_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n0_<=_m_holds_
||.((((s_")_(#)_(R_/*_s))_._m)_-_(0._(REAL-NS_n))).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r )
assume  r > 0 ; ::_thesis: ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r
then consider d being Real such that
A22: d > 0 and
A23: for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r by A19;
consider n0 being Element of NAT  such that
A24: for m being Element of NAT st n0 <= m holds
|.((s . m) - 0).| < d by A20, A22, SEQ_2:def_7;
take n0 = n0; ::_thesis: for m being Element of NAT st n0 <= m holds
||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r
thus  for m being Element of NAT st n0 <= m holds
||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r ::_thesis: verum
proof
 dom R = REAL by A1, PARTFUN1:def_2;
then A25: rng s c= dom R ;
let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r )
assume  n0 <= m ; ::_thesis: ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r
then A26: |.((s . m) - 0).| < d by A24;
A27: s . m <> 0 by SEQ_1:5;
(|.(s . m).| ") * ||.(R /. (s . m)).|| = (abs ((s . m) ")) * ||.(R /. (s . m)).|| by COMPLEX1:66
.= ||.(((s . m) ") * (R /. (s . m))).|| by NORMSP_1:def_1
.= ||.(((s . m) ") * ((R /* s) . m)).|| by A25, FUNCT_2:109
.= ||.(((s ") . m) * ((R /* s) . m)).|| by VALUED_1:10
.= ||.(((s ") (#) (R /* s)) . m).|| by NDIFF_1:def_2
.= ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| by RLVECT_1:13 ;
hence  ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A23, A26, A27; ::_thesis: verum
end;
end;
hence  (s ") (#) (R /* s) is convergent by NORMSP_1:def_6; ::_thesis: lim ((s ") (#) (R /* s)) = 0. (REAL-NS n)
hence  lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) by A21, NORMSP_1:def_7; ::_thesis: verum
end;
hence  R is RestFunc-like by A1, NDIFF_3:def_1; ::_thesis: verum
end;
hence  ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) ) by A2; ::_thesis: verum
end;

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 & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
proof
let i be Element of NAT ; ::_thesis: 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 & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
let n be non empty Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n)
for x0 being real number st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for x0 being real number st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
let x0 be real number ; ::_thesis: ( 1 <= i & i <= n & g is_differentiable_in x0 implies ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) )
assume A1: ( 1 <= i & i <= n & g is_differentiable_in x0 ) ; ::_thesis: ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
then consider N being Neighbourhood of x0 such that
A2: ( N c= dom g & ex DFG being LinearFunc of (REAL-NS n) ex GR being RestFunc of (REAL-NS n) st
( diff (g,x0) = DFG . 1 & ( for x being Real st x in N holds
(g /. x) - (g /. x0) = (DFG . (x - x0)) + (GR /. (x - x0)) ) ) ) by NDIFF_3:def_4;
consider GR being RestFunc of (REAL-NS n), DFG being LinearFunc of (REAL-NS n) such that
A3: ( diff (g,x0) = DFG . 1 & ( for x being Element of REAL st x in N holds
(g /. x) - (g /. x0) = (DFG . (x - x0)) + (GR /. (x - x0)) ) ) by A2;
consider LP being Point of (REAL-NS n) such that
A4: for p being Real holds DFG . p = p * LP by NDIFF_3:def_2;
reconsider PG = Proj (i,n) as Function of (REAL-NS n),(REAL-NS 1) ;
reconsider L = (Proj (i,n)) * DFG as Function of REAL,(REAL-NS 1) ;
A5: for r being Real holds L . r = r * ((Proj (i,n)) . LP)
proof
let r be Real; ::_thesis: L . r = r * ((Proj (i,n)) . LP)
A6: dom L = REAL by FUNCT_2:def_1;
 DFG . r = r * LP by A4;
then  (Proj (i,n)) . (DFG . r) = r * ((Proj (i,n)) . LP) by PDIFF_6:27;
hence  L . r = r * ((Proj (i,n)) . LP) by A6, FUNCT_1:12; ::_thesis: verum
end;
then reconsider L = L as LinearFunc of (REAL-NS 1) by NDIFF_3:def_2;
A7: GR is total by NDIFF_3:def_1;
then reconsider FGR = GR as Function of REAL,(REAL-NS n) ;
A8: (Proj (i,n)) * FGR is Function of REAL,(REAL-NS 1) ;
 (Proj (i,n)) * GR is RestFunc of (REAL-NS 1)
proof
A9: dom GR = REAL by A7, PARTFUN1:def_2;
reconsider R = (Proj (i,n)) * GR as PartFunc of REAL,(REAL-NS 1) ;
 for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) )
assume  r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
then consider d being Real such that
A10: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(GR /. z).|| < r ) ) by A7, Th23;
take  d ; ::_thesis: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
thus  d > 0 by A10; ::_thesis: for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r
let z be Element of REAL ; ::_thesis: ( z <> 0 & |.z.| < d implies (|.z.| ") * ||.(R /. z).|| < r )
assume A11: ( z <> 0 & |.z.| < d ) ; ::_thesis: (|.z.| ") * ||.(R /. z).|| < r
A12: GR /. z = GR . z by A9, PARTFUN1:def_6;
A13: i in Seg n by A1;
reconsider GRz = GR /. z as Point of (REAL-NS n) ;
reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def_4;
reconsider GRzi = GRz1 . i as Element of REAL ;
 dom (Proj (i,n)) = the carrier of (REAL-NS n) by PARTFUN1:def_2;
then A14: z in dom ((Proj (i,n)) * GR) by A9, A12, FUNCT_1:11;
then ((Proj (i,n)) * GR) . z = (Proj (i,n)) . (GR . z) by FUNCT_1:12
.= <*((proj (i,n)) . GRz1)*> by A12, PDIFF_1:def_4 ;
then A15: ((Proj (i,n)) * GR) . z = <*GRzi*> by PDIFF_1:def_1;
A16: abs GRzi <= ||.(GR /. z).|| by A13, REAL_NS1:9;
A17: 0 <= |.z.| by COMPLEX1:46;
 0 <= abs GRzi by COMPLEX1:46;
then A18: (|.z.| ") * (abs GRzi) <= (|.z.| ") * ||.(GR /. z).|| by A16, A17, XREAL_1:66;
 (|.z.| ") * ||.(GR /. z).|| < r by A10, A11;
then A19: (|.z.| ") * (abs GRzi) < r by A18, XXREAL_0:2;
 ((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR) by A14, FUNCT_1:3;
then reconsider Rz = ((Proj (i,n)) * GR) . z as VECTOR of (REAL-NS 1) ;
set VGRzi = <*GRzi*>;
 <*GRzi*> is Element of REAL 1 by FINSEQ_2:98;
then  ||.Rz.|| = |.<*GRzi*>.| by A15, REAL_NS1:1;
then  (|.z.| ") * ||.Rz.|| < r by A19, JORDAN2C:10;
hence  (|.z.| ") * ||.(R /. z).|| < r by A14, PARTFUN1:def_6; ::_thesis: verum
end;
hence  (Proj (i,n)) * GR is RestFunc of (REAL-NS 1) by A8, Th23; ::_thesis: verum
end;
then reconsider R = (Proj (i,n)) * GR as RestFunc of (REAL-NS 1) ;
set pg = (Proj (i,n)) * g;
A20: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
then  rng g c= dom (Proj (i,n)) ;
then A21: dom g = dom ((Proj (i,n)) * g) by RELAT_1:27;
A22: dom (Proj (i,n)) = REAL n by A20, REAL_NS1:def_4;
A23: for x being Real st x in N holds
(((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
now__::_thesis:_(_x_in_N_&_x_in_N_implies_(((Proj_(i,n))_*_g)_/._x)_-_(((Proj_(i,n))_*_g)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))_)
assume A24: x in N ; ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
then A25: (g /. x) - (g /. x0) = (DFG . (x - x0)) + (GR /. (x - x0)) by A3;
A26: x0 in N by RCOMP_1:16;
then A27: ( ((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x & ((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 ) by A2, A21, A24, PARTFUN1:def_6;
A28: ( g /. x = g . x & g /. x0 = g . x0 ) by A2, A24, A26, PARTFUN1:def_6;
reconsider PGSx = (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) as Element of REAL 1 by REAL_NS1:def_4;
 ((Proj (i,n)) * g) . x in rng ((Proj (i,n)) * g) by A2, A21, A24, FUNCT_1:3;
then reconsider PGdx = ((Proj (i,n)) * g) . x as Element of REAL 1 by REAL_NS1:def_4;
 ((Proj (i,n)) * g) . x0 in rng ((Proj (i,n)) * g) by A2, A21, A26, FUNCT_1:3;
then reconsider PGdx0 = ((Proj (i,n)) * g) . x0 as Element of REAL 1 by REAL_NS1:def_4;
 g . x in rng g by A2, A24, FUNCT_1:3;
then reconsider Gx = g . x as Element of REAL n by REAL_NS1:def_4;
 g . x0 in rng g by A2, A26, FUNCT_1:3;
then reconsider Gx0 = g . x0 as Element of REAL n by REAL_NS1:def_4;
set ProjGx = (Proj (i,n)) . (g . x);
 Gx in dom (Proj (i,n)) by A22;
then  (Proj (i,n)) . (g . x) in rng (Proj (i,n)) by FUNCT_1:3;
then reconsider ProjGx = (Proj (i,n)) . (g . x) as Element of REAL 1 by REAL_NS1:def_4;
set ProjGx0 = (Proj (i,n)) . (g . x0);
 Gx0 in dom (Proj (i,n)) by A22;
then  (Proj (i,n)) . (g . x0) in rng (Proj (i,n)) by FUNCT_1:3;
then reconsider ProjGx0 = (Proj (i,n)) . (g . x0) as Element of REAL 1 by REAL_NS1:def_4;
reconsider Gx1 = Gx as Element of (REAL-NS n) by REAL_NS1:def_4;
reconsider Gx01 = Gx0 as Element of (REAL-NS n) by REAL_NS1:def_4;
reconsider Gsx = g /. x as Element of REAL n by REAL_NS1:def_4;
reconsider Gsx0 = g /. x0 as Element of REAL n by REAL_NS1:def_4;
set dxx0 = x - x0;
reconsider Ldxx0 = L . (x - x0) as Element of (REAL-NS 1) ;
A29: dom R = REAL by A8, PARTFUN1:def_2;
then A30: R /. (x - x0) = R . (x - x0) by PARTFUN1:def_6;
then reconsider Rdxx0 = R . (x - x0) as Element of (REAL-NS 1) ;
reconsider Lxx0Rxx0 = (L . (x - x0)) + (R /. (x - x0)) as Element of REAL 1 by REAL_NS1:def_4;
reconsider Ldiff = DFG . (x - x0) as Element of REAL n by REAL_NS1:def_4;
set ProjLdiff = (Proj (i,n)) . Ldiff;
 (Proj (i,n)) . Ldiff in rng (Proj (i,n)) by A20, FUNCT_1:3;
then reconsider ProjLdiff = (Proj (i,n)) . Ldiff as Element of REAL 1 by REAL_NS1:def_4;
A31: dom GR = REAL by A7, PARTFUN1:def_2;
then  GR . (x - x0) in rng GR by FUNCT_1:3;
then reconsider Rdiff = GR . (x - x0) as Element of REAL n by REAL_NS1:def_4;
A32: Rdiff = GR /. (x - x0) by A31, PARTFUN1:def_6;
set ProjRdiff = (Proj (i,n)) . Rdiff;
 (Proj (i,n)) . Rdiff in rng (Proj (i,n)) by A22, FUNCT_1:3;
then reconsider ProjRdiff = (Proj (i,n)) . Rdiff as Element of REAL 1 by REAL_NS1:def_4;
 dom L = REAL by FUNCT_2:def_1;
then  ( L . (x - x0) = (Proj (i,n)) . Ldiff & R . (x - x0) = (Proj (i,n)) . Rdiff ) by A29, FUNCT_1:12;
then A33: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by REAL_NS1:2;
 (Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*> by PDIFF_1:def_4;
then A34: (Proj (i,n)) . Ldiff = <*(Ldiff . i)*> by PDIFF_1:def_1;
 Rdiff in dom (Proj (i,n)) by A22;
then  (Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*> by PDIFF_1:def_4;
then A35: (Proj (i,n)) . Rdiff = <*(Rdiff . i)*> by PDIFF_1:def_1;
reconsider diffGR = (DFG . (x - x0)) + (GR /. (x - x0)) as Element of REAL n by REAL_NS1:def_4;
reconsider Rsdiff = GR /. (x - x0) as Element of REAL n by REAL_NS1:def_4;
PGSx = PGdx - PGdx0 by A27, REAL_NS1:5
.= ProjGx - PGdx0 by A2, A21, A24, FUNCT_1:12
.= ProjGx - ProjGx0 by A2, A21, A26, FUNCT_1:12
.= <*((proj (i,n)) . Gx1)*> - ProjGx0 by PDIFF_1:def_4
.= <*((proj (i,n)) . Gx1)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_4
.= <*(Gx . i)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_1
.= <*(Gx . i)*> - <*(Gx0 . i)*> by PDIFF_1:def_1
.= <*((Gx . i) - (Gx0 . i))*> by RVSUM_1:29
.= <*((Gsx - Gsx0) . i)*> by A28, RVSUM_1:27
.= <*(diffGR . i)*> by A25, REAL_NS1:5
.= <*((Ldiff + Rsdiff) . i)*> by REAL_NS1:2
.= <*((Ldiff . i) + (Rsdiff . i))*> by RVSUM_1:11 ;
hence  ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A30, A33, A34, A35, A32, RVSUM_1:13; ::_thesis: verum
end;
hence  ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ; ::_thesis: verum
end;
hence A36: (Proj (i,n)) * g is_differentiable_in x0 by A2, A21, NDIFF_3:def_3; ::_thesis: (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0)
L . 1 = 1 * ((Proj (i,n)) . LP) by A5
.= (Proj (i,n)) . LP by RLVECT_1:def_8
.= (Proj (i,n)) . (1 * LP) by RLVECT_1:def_8
.= (Proj (i,n)) . (diff (g,x0)) by A3, A4 ;
hence  (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) by A36, A2, A21, A23, NDIFF_3:def_4; ::_thesis: verum
end;

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 & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
proof
let n be non empty Element of NAT ; ::_thesis: 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 & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for x0 being real number holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let x0 be real number ; ::_thesis: ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
thus  ( g is_differentiable_in x0 implies for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) by Th24; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) implies g is_differentiable_in x0 )
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ; ::_thesis: g is_differentiable_in x0
defpred S1[ Element of NAT , Element of REAL ] means ( $2 > 0 & ].(x0 - $2),(x0 + $2).[ c= dom ((Proj ($1,n)) * g) & ex Ri being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - $2),(x0 + $2).[ holds
(((Proj ($1,n)) * g) /. x) - (((Proj ($1,n)) * g) /. x0) = ((x - x0) * (diff (((Proj ($1,n)) * g),x0))) + (Ri /. (x - x0)) );
A2: for k being Element of NAT st k in Seg n holds
ex dk being Element of REAL st S1[k,dk]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dk being Element of REAL st S1[k,dk] )
assume  k in Seg n ; ::_thesis: ex dk being Element of REAL st S1[k,dk]
then  ( 1 <= k & k <= n ) by FINSEQ_1:1;
then  (Proj (k,n)) * g is_differentiable_in x0 by A1;
then consider Nk being Neighbourhood of x0 such that
A3: ( Nk c= dom ((Proj (k,n)) * g) & ex L being LinearFunc of (REAL-NS 1) ex Rk being RestFunc of (REAL-NS 1) st
( L . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (L . (x - x0)) + (Rk /. (x - x0)) ) ) ) by NDIFF_3:def_4;
consider dk being real number  such that
A4: ( 0 < dk & Nk = ].(x0 - dk),(x0 + dk).[ ) by RCOMP_1:def_6;
reconsider dk = dk as Element of REAL by XREAL_0:def_1;
take  dk ; ::_thesis: S1[k,dk]
thus  0 < dk by A4; ::_thesis: ( ].(x0 - dk),(x0 + dk).[ c= dom ((Proj (k,n)) * g) & ex Ri being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Ri /. (x - x0)) )
thus  ].(x0 - dk),(x0 + dk).[ c= dom ((Proj (k,n)) * g) by A4, A3; ::_thesis: ex Ri being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Ri /. (x - x0))
thus  ex Rk being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) ::_thesis: verum
proof
consider L being LinearFunc of (REAL-NS 1), Rk being RestFunc of (REAL-NS 1) such that
A5: ( L . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (L . (x - x0)) + (Rk /. (x - x0)) ) ) by A3;
A6: now__::_thesis:_for_x_being_Real_st_x_in_Nk_holds_
(((Proj_(k,n))_*_g)_/._x)_-_(((Proj_(k,n))_*_g)_/._x0)_=_((x_-_x0)_*_(diff_(((Proj_(k,n))_*_g),x0)))_+_(Rk_/._(x_-_x0))
let x be Real; ::_thesis: ( x in Nk implies (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) )
assume A7: x in Nk ; ::_thesis: (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0))
consider L1 being Point of (REAL-NS 1) such that
A8: for p being Real holds L . p = p * L1 by NDIFF_3:def_2;
A9: diff (((Proj (k,n)) * g),x0) = 1 * L1 by A8, A5
.= L1 by RLVECT_1:def_8 ;
A10: L . (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A9, A8;
thus  (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) by A10, A5, A7; ::_thesis: verum
end;
take  Rk ; ::_thesis: for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0))
thus  for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) by A4, A6; ::_thesis: verum
end;
end;
consider d being FinSequence of REAL  such that
A11: ( dom d = Seg n & ( for k being Element of NAT st k in Seg n holds
S1[k,d /. k] ) ) from RECDEF_1:sch_17(A2);
set d0 = min d;
 len d = n by A11, FINSEQ_1:def_3;
then A12: min_p d in dom d by RFINSEQ2:def_2;
then  d /. (min_p d) > 0 by A11;
then A13: min d > 0 by A12, PARTFUN1:def_6;
defpred S2[ Real, set ] means  ex y being Element of REAL n st
( $2 = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . ($1 * (diff (((Proj (i,n)) * g),x0))) ) );
A14: for x being Real ex y being Point of (REAL-NS n) st S2[x,y]
proof
let x be Real; ::_thesis: ex y being Point of (REAL-NS n) st S2[x,y]
defpred S3[ Element of NAT , set ] means $2 = (proj (1,1)) . (x * (diff (((Proj ($1,n)) * g),x0)));
A15: for i being Element of NAT st i in Seg n holds
ex r being Element of REAL st S3[i,r] ;
consider y being FinSequence of REAL  such that
A16: ( dom y = Seg n & ( for i being Element of NAT st i in Seg n holds
S3[i,y /. i] ) ) from RECDEF_1:sch_17(A15);
 len y = n by A16, FINSEQ_1:def_3;
then reconsider y = y as Element of REAL n by FINSEQ_2:92;
A17: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
y_._i_=_(proj_(1,1))_._(x_*_(diff_(((Proj_(i,n))_*_g),x0)))
let i be Element of NAT ; ::_thesis: ( i in Seg n implies y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) )
assume  i in Seg n ; ::_thesis: y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0)))
then  ( S3[i,y /. i] & y /. i = y . i ) by A16, PARTFUN1:def_6;
hence  y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) ; ::_thesis: verum
end;
reconsider y0 = y as Point of (REAL-NS n) by REAL_NS1:def_4;
 ex y being Element of REAL n st
( y0 = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) ) ) by A17;
hence  ex y0 being Point of (REAL-NS n) st S2[x,y0] ; ::_thesis: verum
end;
consider L being Function of REAL,(REAL-NS n) such that
A18: for x being Real holds S2[x,L . x] from FUNCT_2:sch_3(A14);
 for r being Real holds L . r = r * (L . 1)
proof
let r be Real; ::_thesis: L . r = r * (L . 1)
consider Lx being Element of REAL n such that
A19: ( L . 1 = Lx & ( for i being Element of NAT st i in Seg n holds
Lx . i = (proj (1,1)) . (1 * (diff (((Proj (i,n)) * g),x0))) ) ) by A18;
A20: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
Lx_._i_=_(proj_(1,1))_._(diff_(((Proj_(i,n))_*_g),x0))
let i be Element of NAT ; ::_thesis: ( i in Seg n implies Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) )
assume  i in Seg n ; ::_thesis: Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0))
then  Lx . i = (proj (1,1)) . (1 * (diff (((Proj (i,n)) * g),x0))) by A19;
hence  Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) by RLVECT_1:def_8; ::_thesis: verum
end;
consider Lrx being Element of REAL n such that
A21: ( L . r = Lrx & ( for i being Element of NAT st i in Seg n holds
Lrx . i = (proj (1,1)) . (r * (diff (((Proj (i,n)) * g),x0))) ) ) by A18;
A22: dom (r * Lx) = Seg n by FINSEQ_2:124;
then A23: dom (r * Lx) = dom Lrx by FINSEQ_2:124;
 for i0 being Nat st i0 in dom (r * Lx) holds
(r * Lx) . i0 = Lrx . i0
proof
let i0 be Nat; ::_thesis: ( i0 in dom (r * Lx) implies (r * Lx) . i0 = Lrx . i0 )
reconsider i = i0 as Element of NAT by ORDINAL1:def_12;
assume  i0 in dom (r * Lx) ; ::_thesis: (r * Lx) . i0 = Lrx . i0
then A24: ( Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) & Lrx . i = (proj (1,1)) . (r * (diff (((Proj (i,n)) * g),x0))) ) by A20, A21, A22;
A25: (r * 1) * (diff (((Proj (i,n)) * g),x0)) = r * (1 * (diff (((Proj (i,n)) * g),x0))) by RLVECT_1:def_8;
reconsider Diffrx = (r * 1) * (diff (((Proj (i,n)) * g),x0)) as Element of REAL 1 by REAL_NS1:def_4;
reconsider Diffx = 1 * (diff (((Proj (i,n)) * g),x0)) as Element of REAL 1 by REAL_NS1:def_4;
A26: Diffx = diff (((Proj (i,n)) * g),x0) by RLVECT_1:def_8;
 Diffrx = r * Diffx by A25, REAL_NS1:3;
then  Lrx . i0 = (r * Diffx) . 1 by A24, PDIFF_1:def_1;
then  Lrx . i0 = r * (Diffx . 1) by RVSUM_1:45;
then  Lrx . i0 = r * (Lx . i0) by A24, A26, PDIFF_1:def_1;
hence  (r * Lx) . i0 = Lrx . i0 by RVSUM_1:45; ::_thesis: verum
end;
then  r * Lx = Lrx by A23, FINSEQ_1:13;
hence  L . r = r * (L . 1) by A19, A21, REAL_NS1:3; ::_thesis: verum
end;
then reconsider L = L as linear Function of REAL,(REAL-NS n) by NDIFF_3:def_2;
reconsider L0 = L as LinearFunc of (REAL-NS n) ;
deffunc H1( Element of REAL ) ->  Element of the carrier of (REAL-NS n) = ((g /. ($1 + x0)) - (g /. x0)) - (L . $1);
consider R being Function of REAL,(REAL-NS n) such that
A27: for x being Element of REAL holds R . x = H1(x) from FUNCT_2:sch_4();
A28: for x being Element of REAL
for i being Element of NAT st i in Seg n & x + x0 in dom g holds
((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
proof
let x be Element of REAL ; ::_thesis: for i being Element of NAT st i in Seg n & x + x0 in dom g holds
((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
let i be Element of NAT ; ::_thesis: ( i in Seg n & x + x0 in dom g implies ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) )
assume that
A29: i in Seg n and
A30: x + x0 in dom g ; ::_thesis: ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
A31: |.(x0 - x0).| = 0 by COMPLEX1:44;
A32: ( 0 < d /. i & ].(x0 - (d /. i)),(x0 + (d /. i)).[ c= dom ((Proj (i,n)) * g) ) by A29, A11;
then  x0 in ].(x0 - (d /. i)),(x0 + (d /. i)).[ by A31, RCOMP_1:1;
then A33: x0 in dom ((Proj (i,n)) * g) by A32;
A34: dom ((Proj (i,n)) * g) c= dom g by RELAT_1:25;
reconsider gxx0 = g /. (x + x0), gx0 = g /. x0, Lx = L . x as Element of REAL n by REAL_NS1:def_4;
reconsider gxx01 = g /. (x + x0), gx01 = g /. x0, Lx1 = L . x as Point of (REAL-NS n) ;
A35: ( - gx0 = (- 1) * (g /. x0) & - Lx = (- 1) * (L . x) ) by REAL_NS1:3;
then  gxx0 + (- gx0) = (g /. (x + x0)) + ((- 1) * (g /. x0)) by REAL_NS1:2;
then A36: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L . x)) by A35, REAL_NS1:2;
A37: - 1 is Real by XREAL_0:def_1;
 gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5;
then A38: ((g /. (x + x0)) - (g /. x0)) - (L . x) = (gxx0 - gx0) - Lx by REAL_NS1:5;
 ((Proj (i,n)) * R) . x = (Proj (i,n)) . (R . x) by FUNCT_2:15;
then  ((Proj (i,n)) * R) . x = (Proj (i,n)) . (((g /. (x + x0)) - (g /. x0)) - (L . x)) by A27;
then  ((Proj (i,n)) * R) . x = ((Proj (i,n)) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by A38, A36, PDIFF_6:26;
then A39: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + ((Proj (i,n)) . ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by PDIFF_6:26;
 ( (Proj (i,n)) . ((- 1) * (g /. x0)) = (- 1) * ((Proj (i,n)) . (g /. x0)) & (Proj (i,n)) . ((- 1) * Lx1) = (- 1) * ((Proj (i,n)) . Lx1) ) by A37, PDIFF_6:27;
then  ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + ((- 1) * ((Proj (i,n)) . (L . x))) by A39, RLVECT_1:16;
then A40: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) - ((Proj (i,n)) . (L . x)) by RLVECT_1:16;
 ( g /. (x + x0) in the carrier of (REAL-NS n) & g /. x0 in the carrier of (REAL-NS n) ) ;
then A41: ( g /. (x + x0) in dom (Proj (i,n)) & g /. x0 in dom (Proj (i,n)) ) by FUNCT_2:def_1;
A42: (Proj (i,n)) . (g /. (x + x0)) = (Proj (i,n)) /. (g /. (x + x0))
.= ((Proj (i,n)) * g) /. (x + x0) by A30, A41, PARTFUN2:4 ;
(Proj (i,n)) . (g /. x0) = (Proj (i,n)) /. (g /. x0)
.= ((Proj (i,n)) * g) /. x0 by A33, A34, A41, PARTFUN2:4 ;
hence  ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) by A40, A42, FUNCT_2:15; ::_thesis: verum
end;
 for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) )
assume A43: r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
set r0 = ((sqrt n) ") * r;
A44: sqrt n > 0 by SQUARE_1:25;
then A45: ((sqrt n) ") * r > 0 by A43, XREAL_1:129;
defpred S3[ Element of NAT , Element of REAL ] means ( $2 > 0 & ( for z being Real st z <> 0 & |.z.| < $2 holds
(|.z.| ") * ||.(((Proj ($1,n)) * R) /. z).|| < ((sqrt n) ") * r ) );
A46: for k being Element of NAT st k in Seg n holds
ex dd being Element of REAL st S3[k,dd]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dd being Element of REAL st S3[k,dd] )
assume A47: k in Seg n ; ::_thesis: ex dd being Element of REAL st S3[k,dd]
then  ( 1 <= k & k <= n ) by FINSEQ_1:1;
then  (Proj (k,n)) * g is_differentiable_in x0 by A1;
then consider Nk being Neighbourhood of x0 such that
A48: ( Nk c= dom ((Proj (k,n)) * g) & ex LR being LinearFunc of (REAL-NS 1) ex PR being RestFunc of (REAL-NS 1) st
( LR . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (LR . (x - x0)) + (PR /. (x - x0)) ) ) ) by NDIFF_3:def_4;
consider d0 being real number  such that
A49: ( 0 < d0 & Nk = ].(x0 - d0),(x0 + d0).[ ) by RCOMP_1:def_6;
reconsider d0 = d0 as Real by XREAL_0:def_1;
consider LR being LinearFunc of (REAL-NS 1), PR being RestFunc of (REAL-NS 1) such that
A50: ( LR . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (LR . (x - x0)) + (PR /. (x - x0)) ) ) by A48;
A51: now__::_thesis:_for_x_being_Real_st_x_in_Nk_holds_
(((Proj_(k,n))_*_g)_/._x)_-_(((Proj_(k,n))_*_g)_/._x0)_=_((x_-_x0)_*_(diff_(((Proj_(k,n))_*_g),x0)))_+_(PR_/._(x_-_x0))
let x be Real; ::_thesis: ( x in Nk implies (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) )
assume A52: x in Nk ; ::_thesis: (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0))
consider L1 being Point of (REAL-NS 1) such that
A53: for p being Real holds LR . p = p * L1 by NDIFF_3:def_2;
diff (((Proj (k,n)) * g),x0) = 1 * L1 by A53, A50
.= L1 by RLVECT_1:def_8 ;
then  LR . (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A53;
hence  (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) by A52, A50; ::_thesis: verum
end;
 PR is total by NDIFF_3:def_1;
then consider d1 being Real such that
A54: ( d1 > 0 & ( for z being Real st z <> 0 & |.z.| < d1 holds
(|.z.| ") * ||.(PR /. z).|| < ((sqrt n) ") * r ) ) by A45, Th23;
set dd = min (d0,d1);
take  min (d0,d1) ; ::_thesis: S3[k, min (d0,d1)]
 for z being Real st z <> 0 & |.z.| < min (d0,d1) holds
(|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r
proof
let z be Real; ::_thesis: ( z <> 0 & |.z.| < min (d0,d1) implies (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r )
assume A55: ( z <> 0 & |.z.| < min (d0,d1) ) ; ::_thesis: (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r
 min (d0,d1) <= d1 by XXREAL_0:17;
then  |.z.| < d1 by A55, XXREAL_0:2;
then A56: (|.z.| ") * ||.(PR /. z).|| < ((sqrt n) ") * r by A55, A54;
 min (d0,d1) <= d0 by XXREAL_0:17;
then A57: |.z.| < d0 by A55, XXREAL_0:2;
 (z + x0) - x0 = z ;
then A58: z + x0 in ].(x0 - d0),(x0 + d0).[ by A57, RCOMP_1:1;
then A59: z + x0 in dom ((Proj (k,n)) * g) by A48, A49;
 (((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0) = (((z + x0) - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. ((z + x0) - x0)) by A58, A49, A51;
then A60: PR /. z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (z * (diff (((Proj (k,n)) * g),x0))) by RLVECT_4:1;
 dom ((Proj (k,n)) * g) c= dom g by RELAT_1:25;
then A61: ((Proj (k,n)) * R) . z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (((Proj (k,n)) * L) . z) by A59, A47, A28;
consider y being Element of REAL n such that
A62: ( L . z = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . (z * (diff (((Proj (i,n)) * g),x0))) ) ) by A18;
A63: y . k = (proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))) by A62, A47;
 z * (diff (((Proj (k,n)) * g),x0)) is Element of REAL 1 by REAL_NS1:def_4;
then consider Dk being Element of REAL  such that
A64: z * (diff (((Proj (k,n)) * g),x0)) = <*Dk*> by FINSEQ_2:97;
reconsider y1 = y as Point of (REAL-NS n) by REAL_NS1:def_4;
 dom L = REAL by FUNCT_2:def_1;
then  ((Proj (k,n)) * L) . z = (Proj (k,n)) . (L . z) by FUNCT_1:13;
then  ((Proj (k,n)) * L) . z = <*((proj (k,n)) . y1)*> by A62, PDIFF_1:def_4;
then  ((Proj (k,n)) * L) . z = <*((proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))))*> by A63, PDIFF_1:def_1;
hence  (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r by A56, A60, A61, A64, PDIFF_1:1; ::_thesis: verum
end;
hence  S3[k, min (d0,d1)] by A49, A54, XXREAL_0:21; ::_thesis: verum
end;
consider dd being FinSequence of REAL  such that
A65: ( dom dd = Seg n & ( for i being Element of NAT st i in Seg n holds
S3[i,dd /. i] ) ) from RECDEF_1:sch_17(A46);
take d = min dd; ::_thesis: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
 len dd = n by A65, FINSEQ_1:def_3;
then A66: min_p dd in dom dd by RFINSEQ2:def_2;
then A67: dd /. (min_p dd) > 0 by A65;
 for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r
proof
let z be Real; ::_thesis: ( z <> 0 & |.z.| < d implies (|.z.| ") * ||.(R /. z).|| < r )
assume A68: ( z <> 0 & |.z.| < d ) ; ::_thesis: (|.z.| ") * ||.(R /. z).|| < r
reconsider Rz = R /. z as Element of REAL n by REAL_NS1:def_4;
reconsider R0 = n |-> ((|.z.| * (((sqrt n) ") * r)) ^2) as Element of n -tuples_on REAL ;
reconsider SRz = sqr Rz as Element of n -tuples_on REAL ;
A69: |.z.| > 0 by A68, COMPLEX1:47;
A70: for i0 being Nat st i0 in Seg n holds
SRz . i0 < R0 . i0
proof
let i0 be Nat; ::_thesis: ( i0 in Seg n implies SRz . i0 < R0 . i0 )
reconsider i = i0 as Element of NAT by ORDINAL1:def_12;
assume A71: i0 in Seg n ; ::_thesis: SRz . i0 < R0 . i0
then  i in dom Rz by FINSEQ_2:124;
then  (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13;
then A72: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2;
 ( 1 <= i & i <= n ) by A71, FINSEQ_1:1;
then  ( 1 <= i & i <= len dd ) by A65, FINSEQ_1:def_3;
then  d <= dd . i by RFINSEQ2:2;
then  d <= dd /. i by A71, A65, PARTFUN1:def_6;
then  |.z.| < dd /. i by A68, XXREAL_0:2;
then  (|.z.| ") * ||.(((Proj (i,n)) * R) /. z).|| < ((sqrt n) ") * r by A68, A71, A65;
then A73: ||.(((Proj (i,n)) * R) /. z).|| < (((sqrt n) ") * r) / (|.z.| ") by A69, XREAL_1:81;
reconsider Rzi = <*(Rz . i)*> as Element of REAL 1 by FINSEQ_2:98;
 ((Proj (i,n)) * R) . z = (Proj (i,n)) . (R . z) by FUNCT_2:15;
then  ((Proj (i,n)) * R) . z = <*((proj (i,n)) . Rz)*> by PDIFF_1:def_4;
then  ((Proj (i,n)) * R) . z = <*(Rz . i)*> by PDIFF_1:def_1;
then  ||.(((Proj (i,n)) * R) . z).|| = |.Rzi.| by REAL_NS1:1;
then  |.(Rz . i).| < |.z.| * (((sqrt n) ") * r) by A73, JORDAN2C:10;
then  |.(Rz . i).| ^2 < (|.z.| * (((sqrt n) ") * r)) ^2 by COMPLEX1:46, SQUARE_1:16;
then  (Rz . i0) ^2 < (|.z.| * (((sqrt n) ") * r)) ^2 by COMPLEX1:75;
hence  SRz . i0 < R0 . i0 by A71, A72, FINSEQ_2:57; ::_thesis: verum
end;
A74: for i being Nat st i in dom (sqr Rz) holds
0 <= (sqr Rz) . i
proof
let i be Nat; ::_thesis: ( i in dom (sqr Rz) implies 0 <= (sqr Rz) . i )
assume  i in dom (sqr Rz) ; ::_thesis: 0 <= (sqr Rz) . i
then  ( i in dom (sqrreal * Rz) & dom (sqrreal * Rz) c= dom Rz ) by RELAT_1:25;
then  (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13;
then  (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2;
hence  0 <= (sqr Rz) . i by XREAL_1:63; ::_thesis: verum
end;
A75: (|.z.| * (((sqrt n) ") * r)) ^2 >= 0 by XREAL_1:63;
A76: ex i being Nat st
( i in Seg n & SRz . i < R0 . i )
proof
take  1 ; ::_thesis: ( 1 in Seg n & SRz . 1 < R0 . 1 )
 1 <= n by NAT_1:14;
hence  1 in Seg n ; ::_thesis: SRz . 1 < R0 . 1
hence  SRz . 1 < R0 . 1 by A70; ::_thesis: verum
end;
A77: sqrt n > 0 by SQUARE_1:25;
 for i0 being Nat st i0 in Seg n holds
SRz . i0 <= R0 . i0 by A70;
then  Sum SRz < Sum R0 by A76, RVSUM_1:83;
then  Sum (sqr Rz) < n * ((|.z.| * (((sqrt n) ") * r)) ^2) by RVSUM_1:80;
then  |.Rz.| < sqrt (n * ((|.z.| * (((sqrt n) ") * r)) ^2)) by A74, RVSUM_1:84, SQUARE_1:27;
then  |.Rz.| < (sqrt n) * (sqrt ((|.z.| * (((sqrt n) ") * r)) ^2)) by A75, SQUARE_1:29;
then  |.Rz.| < (sqrt n) * |.(|.z.| * (((sqrt n) ") * r)).| by COMPLEX1:72;
then  |.Rz.| < (sqrt n) * (|.z.| * (((sqrt n) ") * r)) by A44, A43, A69, ABSVALUE:def_1;
then  |.Rz.| < ((sqrt n) * (((sqrt n) ") * r)) * |.z.| ;
then  |.Rz.| / |.z.| < (sqrt n) * (((sqrt n) ") * r) by A69, XREAL_1:83;
then  (|.z.| ") * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) ")) * r by REAL_NS1:1;
then  (|.z.| ") * ||.(R /. z).|| < 1 * r by A77, XCMPLX_0:def_7;
hence  (|.z.| ") * ||.(R /. z).|| < r ; ::_thesis: verum
end;
hence  ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) by A67, A66, PARTFUN1:def_6; ::_thesis: verum
end;
then reconsider R = R as RestFunc of (REAL-NS n) by Th23;
reconsider N = ].(x0 - (min d)),(x0 + (min d)).[ as Neighbourhood of x0 by A13, RCOMP_1:def_6;
now__::_thesis:_for_x_being_set_st_x_in_N_holds_
x_in_dom_g
let x be set ; ::_thesis: ( x in N implies x in dom g )
assume A78: x in N ; ::_thesis: x in dom g
then reconsider y = x as Real ;
A79: |.(y - x0).| < min d by A78, RCOMP_1:1;
 1 <= n by NAT_1:14;
then A80: ( 1 in Seg n & 1 in dom d ) by A11;
then A81: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom ((Proj (1,n)) * g) by A11;
 dom ((Proj (1,n)) * g) c= dom g by RELAT_1:25;
then A82: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom g by A81, XBOOLE_1:1;
 len d = n by A11, FINSEQ_1:def_3;
then  1 <= len d by NAT_1:14;
then  min d <= d . 1 by RFINSEQ2:2;
then  min d <= d /. 1 by A80, PARTFUN1:def_6;
then  |.(y - x0).| < d /. 1 by A79, XXREAL_0:2;
then  y in ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ by RCOMP_1:1;
hence  x in dom g by A82; ::_thesis: verum
end;
then A83: N c= dom g by TARSKI:def_3;
 ex L being LinearFunc of (REAL-NS n) ex R being RestFunc of (REAL-NS n) st
for x being Real st x in N holds
(g /. x) - (g /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
take  L0 ; ::_thesis: ex R being RestFunc of (REAL-NS n) st
for x being Real st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
take  R ; ::_thesis: for x being Real st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
let x be Real; ::_thesis: ( x in N implies (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) )
assume  x in N ; ::_thesis: (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
A84: dom R = REAL by PARTFUN1:def_2;
 R . (x - x0) = ((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0)) by A27;
then  R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by A84, PARTFUN1:def_6;
then  (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + ((- (L0 . (x - x0))) + (L0 . (x - x0))) by RLVECT_1:def_3;
then  (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + (0. (REAL-NS n)) by RLVECT_1:5;
hence  (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) by RLVECT_1:4; ::_thesis: verum
end;
hence  g is_differentiable_in x0 by A83, NDIFF_3:def_3; ::_thesis: verum
end;

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 & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
proof
let i be Element of NAT ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being real number st 1 <= i & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for x0 being real number st 1 <= i & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
let f be PartFunc of REAL,(REAL n); ::_thesis: for x0 being real number st 1 <= i & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
let x0 be real number ; ::_thesis: ( 1 <= i & i <= n & f is_differentiable_in x0 implies ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) )
assume A1: ( 1 <= i & i <= n & f is_differentiable_in x0 ) ; ::_thesis: ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A2: ( f = g & g is_differentiable_in x0 ) by Def1;
 diff (f,x0) = diff (g,x0) by A2, Th3;
hence  ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) by A2, A1, Th24; ::_thesis: verum
end;

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 & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 )
proof
let n be non empty Element of NAT ; ::_thesis: 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 & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 )
let f be PartFunc of REAL,(REAL n); ::_thesis: for x0 being real number holds
( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 )
let x0 be real number ; ::_thesis: ( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 )
thus  ( f is_differentiable_in x0 implies for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 ) ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 ) implies f is_differentiable_in x0 )
proof
assume  f is_differentiable_in x0 ; ::_thesis: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0
then  ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_differentiable_in x0 ) by Def1;
hence  for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 by Th25; ::_thesis: verum
end;
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_in x0 ; ::_thesis: f is_differentiable_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 by A1;
then  g is_differentiable_in x0 by Th25;
hence  f is_differentiable_in x0 by Def1; ::_thesis: verum
end;

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 & i <= n & g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
proof
let X be set ; ::_thesis: 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 & i <= n & g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
let i be Element of NAT ; ::_thesis: for n being non empty Element of NAT
for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
let n be non empty Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( 1 <= i & i <= n & g is_differentiable_on X implies ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) )
assume A1: ( 1 <= i & i <= n & g is_differentiable_on X ) ; ::_thesis: ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
then A2: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11;
A3: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng g c= the carrier of (REAL-NS n) ;
then  dom ((Proj (i,n)) * g) = dom g by A3, RELAT_1:27;
then A4: X c= dom ((Proj (i,n)) * g) by A2, A1, NDIFF_3:10;
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
(Proj_(i,n))_*_g_is_differentiable_in_x
let x be Real; ::_thesis: ( x in X implies (Proj (i,n)) * g is_differentiable_in x )
assume  x in X ; ::_thesis: (Proj (i,n)) * g is_differentiable_in x
then  g is_differentiable_in x by A2, A1, NDIFF_3:10;
hence  (Proj (i,n)) * g is_differentiable_in x by A1, Th24; ::_thesis: verum
end;
hence A5: (Proj (i,n)) * g is_differentiable_on X by A2, A4, NDIFF_3:10; ::_thesis: (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X
then A6: ( dom (((Proj (i,n)) * g) `| X) = X & ( for x being Real st x in X holds
(((Proj (i,n)) * g) `| X) . x = diff (((Proj (i,n)) * g),x) ) ) by NDIFF_3:def_6;
A7: ( dom (g `| X) = X & ( for x being Real st x in X holds
(g `| X) . x = diff (g,x) ) ) by A1, NDIFF_3:def_6;
 rng (g `| X) c= the carrier of (REAL-NS n) ;
then A8: dom ((Proj (i,n)) * (g `| X)) = dom (g `| X) by A3, RELAT_1:27;
now__::_thesis:_for_x_being_Real_st_x_in_dom_(((Proj_(i,n))_*_g)_`|_X)_holds_
((Proj_(i,n))_*_(g_`|_X))_._x_=_(((Proj_(i,n))_*_g)_`|_X)_._x
let x be Real; ::_thesis: ( x in dom (((Proj (i,n)) * g) `| X) implies ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x )
assume A9: x in dom (((Proj (i,n)) * g) `| X) ; ::_thesis: ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x
then A10: x in X by A5, NDIFF_3:def_6;
then  g is_differentiable_in x by A2, A1, NDIFF_3:10;
then A11: (Proj (i,n)) . (diff (g,x)) = diff (((Proj (i,n)) * g),x) by A1, Th24;
A12: (((Proj (i,n)) * g) `| X) . x = diff (((Proj (i,n)) * g),x) by A9, A6;
 (g `| X) . x = diff (g,x) by A10, A1, NDIFF_3:def_6;
hence  ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x by A7, A10, A11, A12, FUNCT_1:13; ::_thesis: verum
end;
hence  (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X by A8, A6, A7, PARTFUN1:5; ::_thesis: verum
end;

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 & i <= n & f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
proof
let X be set ; ::_thesis: 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 & i <= n & f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
let i be Element of NAT ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 1 <= i & i <= n & f is_differentiable_on X implies ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) )
assume A1: ( 1 <= i & i <= n & f is_differentiable_on X ) ; ::_thesis: ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
then A2: X is open Subset of REAL by Th4, Th6;
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A3: X c= dom g by A2, A1, Th5;
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
g_is_differentiable_in_x
let x be Real; ::_thesis: ( x in X implies g is_differentiable_in x )
assume  x in X ; ::_thesis: g is_differentiable_in x
then  f is_differentiable_in x by A2, A1, Th5;
hence  g is_differentiable_in x by Th2; ::_thesis: verum
end;
then A4: g is_differentiable_on X by A2, A3, NDIFF_3:10;
hence  (Proj (i,n)) * f is_differentiable_on X by A1, Th28; ::_thesis: (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X
A5: ( dom (g `| X) = X & ( for x being Real st x in X holds
(g `| X) . x = diff (g,x) ) ) by A4, NDIFF_3:def_6;
A6: dom (f `| X) = dom (g `| X) by A1, Def4, A5;
A7: now__::_thesis:_for_x_being_Real_st_x_in_dom_(f_`|_X)_holds_
(f_`|_X)_._x_=_(g_`|_X)_._x
let x be Real; ::_thesis: ( x in dom (f `| X) implies (f `| X) . x = (g `| X) . x )
assume  x in dom (f `| X) ; ::_thesis: (f `| X) . x = (g `| X) . x
then A8: x in X by A1, Def4;
then A9: (f `| X) . x = diff (f,x) by A1, Def4;
 diff (f,x) = diff (g,x) by Th3;
hence  (f `| X) . x = (g `| X) . x by A9, A8, A4, NDIFF_3:def_6; ::_thesis: verum
end;
 g `| X is PartFunc of REAL,(REAL n) by REAL_NS1:def_4;
then  (Proj (i,n)) * (f `| X) = (Proj (i,n)) * (g `| X) by A6, A7, PARTFUN1:5;
hence  (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X by A4, A1, Th28; ::_thesis: verum
end;

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 & i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
proof
let X be set ; ::_thesis: 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 & i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
let n be non empty Element of NAT ; ::_thesis: 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 & i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
thus  ( g is_differentiable_on X implies for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X ) by Th28; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X ) implies g is_differentiable_on X )
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X ; ::_thesis: g is_differentiable_on X
 1 <= n by NAT_1:14;
then A2: (Proj (1,n)) * g is_differentiable_on X by A1;
then A3: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11;
A4: dom (Proj (1,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
A5: rng g c= the carrier of (REAL-NS n) ;
 X c= dom ((Proj (1,n)) * g) by A2, A3, NDIFF_3:10;
then A6: X c= dom g by A5, A4, RELAT_1:27;
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
g_is_differentiable_in_x
let x be Real; ::_thesis: ( x in X implies g is_differentiable_in x )
assume A7: x in X ; ::_thesis: g is_differentiable_in x
now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_
(Proj_(i,n))_*_g_is_differentiable_in_x
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies (Proj (i,n)) * g is_differentiable_in x )
assume  ( 1 <= i & i <= n ) ; ::_thesis: (Proj (i,n)) * g is_differentiable_in x
then  (Proj (i,n)) * g is_differentiable_on X by A1;
hence  (Proj (i,n)) * g is_differentiable_in x by A7, A3, NDIFF_3:10; ::_thesis: verum
end;
hence  g is_differentiable_in x by Th25; ::_thesis: verum
end;
hence  g is_differentiable_on X by A3, A6, NDIFF_3:10; ::_thesis: verum
end;

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 & i <= n holds
(Proj (i,n)) * f is_differentiable_on X )
proof
let X be set ; ::_thesis: 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 & i <= n holds
(Proj (i,n)) * f is_differentiable_on X )
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds
( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_on X )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_on X )
thus  ( f is_differentiable_on X implies for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_on X ) by Th29; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_on X ) implies f is_differentiable_on X )
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_on X ; ::_thesis: f is_differentiable_on X
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X by A1;
then A2: g is_differentiable_on X by Th30;
then A3: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11;
then A4: X c= dom f by A2, NDIFF_3:10;
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
f_is_differentiable_in_x
let x be Real; ::_thesis: ( x in X implies f is_differentiable_in x )
assume  x in X ; ::_thesis: f is_differentiable_in x
then  g is_differentiable_in x by A3, A2, NDIFF_3:10;
hence  f is_differentiable_in x by Def1; ::_thesis: verum
end;
hence  f is_differentiable_on X by A3, A4, Th5; ::_thesis: verum
end;

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
proof
let J be Function of (REAL-NS 1),REAL; ::_thesis: for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds
J is_continuous_in x0
let x0 be Point of (REAL-NS 1); ::_thesis: ( J = proj (1,1) implies J is_continuous_in x0 )
assume A1: J = proj (1,1) ; ::_thesis: J is_continuous_in x0
A2: dom J = the carrier of (REAL-NS 1) by FUNCT_2:def_1;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_(REAL-NS_1)_st_x1_in_dom_J_&_||.(x1_-_x0).||_<_s_holds_
abs_((J_/._x1)_-_(J_/._x0))_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds
abs ((J /. x1) - (J /. x0)) < r ) ) )
assume A3: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds
abs ((J /. x1) - (J /. x0)) < r ) )
take s = r; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds
abs ((J /. x1) - (J /. x0)) < r ) )
thus  0 < s by A3; ::_thesis: for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds
abs ((J /. x1) - (J /. x0)) < r
thus  for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds
abs ((J /. x1) - (J /. x0)) < r ::_thesis: verum
proof
let x1 be Point of (REAL-NS 1); ::_thesis: ( x1 in dom J & ||.(x1 - x0).|| < s implies abs ((J /. x1) - (J /. x0)) < r )
 (J /. x1) - (J /. x0) = J . (x1 - x0) by A1, PDIFF_1:4;
hence  ( x1 in dom J & ||.(x1 - x0).|| < s implies abs ((J /. x1) - (J /. x0)) < r ) by A1, PDIFF_1:4; ::_thesis: verum
end;
end;
hence  J is_continuous_in x0 by A2, NFCONT_1:8; ::_thesis: verum
end;

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
proof
let x0 be Real; ::_thesis: for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
I is_continuous_in x0
let I be Function of REAL,(REAL-NS 1); ::_thesis: ( I = (proj (1,1)) " implies I is_continuous_in x0 )
assume A1: I = (proj (1,1)) " ; ::_thesis: I is_continuous_in x0
A2: I is Function of REAL,(REAL 1) by REAL_NS1:def_4;
A3: dom I = REAL by FUNCT_2:def_1;
reconsider y0 = x0 as real number ;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_y1_being_real_number_st_y1_in_dom_I_&_abs_(y1_-_y0)_<_s_holds_
||.((I_/._y1)_-_(I_/._y0)).||_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds
||.((I /. y1) - (I /. y0)).|| < r ) ) )
assume A4: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds
||.((I /. y1) - (I /. y0)).|| < r ) )
reconsider s1 = r as real number ;
take s = s1; ::_thesis: ( 0 < s & ( for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds
||.((I /. y1) - (I /. y0)).|| < r ) )
thus  0 < s by A4; ::_thesis: for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds
||.((I /. y1) - (I /. y0)).|| < r
thus  for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds
||.((I /. y1) - (I /. y0)).|| < r ::_thesis: verum
proof
let y1 be real number ; ::_thesis: ( y1 in dom I & abs (y1 - y0) < s implies ||.((I /. y1) - (I /. y0)).|| < r )
assume A5: ( y1 in dom I & abs (y1 - y0) < s ) ; ::_thesis: ||.((I /. y1) - (I /. y0)).|| < r
reconsider x1 = y1 as Element of REAL by XREAL_0:def_1;
 (I /. x1) - (I /. x0) = I . (x1 - x0) by A1, A2, PDIFF_1:3;
hence  ||.((I /. y1) - (I /. y0)).|| < r by A5, A1, A2, PDIFF_1:3; ::_thesis: verum
end;
end;
hence  I is_continuous_in x0 by A3, NFCONT_3:8; ::_thesis: verum
end;

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) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proof
let S, T be RealNormSpace; ::_thesis: 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) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f1 be PartFunc of S,REAL; ::_thesis: for f2 being PartFunc of REAL,T
for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f2 be PartFunc of REAL,T; ::_thesis: for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let x0 be Point of S; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 /. x0 or f2 * f1 is_continuous_in x0 )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 /. x0 ; ::_thesis: f2 * f1 is_continuous_in x0
thus  x0 in dom (f2 * f1) by A1; :: according to NFCONT_1:def_5 ::_thesis: for b1 being Element of K6(K7(NAT, the carrier of S)) holds
( not rng b1 c= dom (f2 * f1) or not b1 is convergent or not lim b1 = x0 or ( (f2 * f1) /* b1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* b1) ) )
let s1 be sequence of S; ::_thesis: ( not rng s1 c= dom (f2 * f1) or not s1 is convergent or not lim s1 = x0 or ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) )
assume that
A4: rng s1 c= dom (f2 * f1) and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) )
A6: dom (f2 * f1) c= dom f1 by RELAT_1:25;
now__::_thesis:_for_x_being_set_st_x_in_rng_(f1_/*_s1)_holds_
x_in_dom_f2
let x be set ; ::_thesis: ( x in rng (f1 /* s1) implies x in dom f2 )
assume  x in rng (f1 /* s1) ; ::_thesis: x in dom f2
then consider n being Element of NAT  such that
A7: x = (f1 /* s1) . n by FUNCT_2:113;
 s1 . n in rng s1 by VALUED_0:28;
then  f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11;
hence  x in dom f2 by A4, A6, A7, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum
end;
then A8: rng (f1 /* s1) c= dom f2 by TARSKI:def_3;
A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f2_*_f1)_/*_s1)_._n_=_(f2_/*_(f1_/*_s1))_._n
let n be Element of NAT ; ::_thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
 s1 . n in rng s1 by VALUED_0:28;
then A10: s1 . n in dom f1 by A4, FUNCT_1:11;
thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108
.= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:13
.= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by A8, FUNCT_2:108 ; ::_thesis: verum
end;
then A11: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63;
 rng s1 c= dom f1 by A4, A6, XBOOLE_1:1;
then A12: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) ) by A2, A5, NFCONT_1:def_6;
(f2 * f1) /. x0 = f2 /. (f1 /. x0) by A1, PARTFUN2:3
.= lim (f2 /* (f1 /* s1)) by A12, A3, A8, NFCONT_3:def_1
.= lim ((f2 * f1) /* s1) by A9, FUNCT_2:63 ;
hence  ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) by A3, A12, A8, A11, NFCONT_3:def_1; ::_thesis: verum
end;

Lm2:  ( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
proof
set f = proj (1,1);
 for y being set st y in REAL holds
ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x )
proof
let y be set ; ::_thesis: ( y in REAL implies ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x ) )
assume  y in REAL ; ::_thesis: ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x )
then reconsider y1 = y as Element of REAL ;
reconsider x = <*y1*> as Element of REAL 1 by FINSEQ_2:98;
 (proj (1,1)) . x = x . 1 by PDIFF_1:def_1;
then  (proj (1,1)) . x = y by FINSEQ_1:40;
hence  ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x ) ; ::_thesis: verum
end;
hence  ( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by FUNCT_2:10, FUNCT_2:def_1, PDIFF_1:1; ::_thesis: verum
end;

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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
proof
let n be non empty Element of NAT ; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let J be Function of (REAL-NS 1),REAL; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let x0 be Point of (REAL-NS 1); ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let y0 be Element of REAL ; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) )
assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J ) ; ::_thesis: ( f is_continuous_in x0 iff g is_continuous_in y0 )
thus  ( f is_continuous_in x0 implies g is_continuous_in y0 ) ::_thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 )
proof
reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def_4;
A2: J * I = id REAL by A1, Lm2, FUNCT_1:39;
A3: f * I = g * (id REAL) by A1, A2, RELAT_1:36
.= g by FUNCT_2:17 ;
 I /. y0 = x0 by A1, PDIFF_1:1;
hence  ( f is_continuous_in x0 implies g is_continuous_in y0 ) by A3, Th33, A1, NFCONT_3:15; ::_thesis: verum
end;
 J /. x0 = y0 by A1, PDIFF_1:1;
hence  ( g is_continuous_in y0 implies f is_continuous_in x0 ) by A1, Th32, Th34; ::_thesis: verum
end;

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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
proof
let n be non empty Element of NAT ; ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let I be Function of REAL,(REAL-NS 1); ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let x0 be Point of (REAL-NS 1); ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let y0 be Element of REAL ; ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) )
assume A1: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g ) ; ::_thesis: ( f is_continuous_in x0 iff g is_continuous_in y0 )
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
thus  ( f is_continuous_in x0 implies g is_continuous_in y0 ) ::_thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 )
proof
 I /. y0 = x0 by A1, PDIFF_1:1;
hence  ( f is_continuous_in x0 implies g is_continuous_in y0 ) by A1, Th33, NFCONT_3:15; ::_thesis: verum
end;
A2: I * J = id (REAL-NS 1) by A1, Lm2, Lm1, FUNCT_1:39;
A3: g * J = f * (id (REAL-NS 1)) by A2, A1, RELAT_1:36
.= f by FUNCT_2:17 ;
 J /. x0 = y0 by A1, PDIFF_1:1;
hence  ( g is_continuous_in y0 implies f is_continuous_in x0 ) by A3, Th32, A1, Th34; ::_thesis: verum
end;

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 & diff (I,x0) = <*1*> )
proof
let x0 be Real; ::_thesis: for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( I is_differentiable_in x0 & diff (I,x0) = <*1*> )
let I be Function of REAL,(REAL-NS 1); ::_thesis: ( I = (proj (1,1)) " implies ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) )
assume A1: I = (proj (1,1)) " ; ::_thesis: ( I is_differentiable_in x0 & diff (I,x0) = <*1*> )
 I . 1 = <*1*> by A1, PDIFF_1:1;
then reconsider r = <*1*> as Point of (REAL-NS 1) ;
A2: for x being Real st x in [#] REAL holds
I /. x = (x * r) + (0. (REAL-NS 1))
proof
let x be Real; ::_thesis: ( x in [#] REAL implies I /. x = (x * r) + (0. (REAL-NS 1)) )
assume  x in [#] REAL ; ::_thesis: I /. x = (x * r) + (0. (REAL-NS 1))
 I . 1 in REAL 1 by A1, FUNCT_1:3, PDIFF_1:2;
then A3: <*1*> is Element of REAL 1 by A1, PDIFF_1:1;
I /. x = <*(x * 1)*> by A1, PDIFF_1:1
.= x * <*1*> by RVSUM_1:47 ;
hence I /. x = x * r by A3, REAL_NS1:3
.= (x * r) + (0. (REAL-NS 1)) by RLVECT_1:4 ;
::_thesis: verum
end;
A4: [#] REAL c= dom I by FUNCT_2:def_1;
then A5: ( I is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(I `| ([#] REAL)) . x = r ) ) by A2, NDIFF_3:21;
r = (I `| ([#] REAL)) . x0 by A4, A2, NDIFF_3:21
.= diff (I,x0) by A5, NDIFF_3:def_6 ;
hence  ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) by A5, NDIFF_3:10; ::_thesis: verum
end;

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 & x = y & 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 & x = y & 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 & x = y & 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 & x = y & b1 = diff (g,y) )
proof
reconsider g = f as PartFunc of (REAL n),REAL by REAL_NS1:def_4;
reconsider y = x as Element of REAL n by REAL_NS1:def_4;
 REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4;
then  diff (g,y) is Function of (REAL-NS n),REAL ;
hence  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 & x = y & b1 = diff (g,y) ) ; ::_thesis: verum
end;
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 & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g & x = y & 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 & x = y & 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 & diff (J,x0) = J )
proof
let J be Function of (REAL 1),REAL; ::_thesis: for x0 being Element of REAL 1 st J = proj (1,1) holds
( J is_differentiable_in x0 & diff (J,x0) = J )
let x0 be Element of REAL 1; ::_thesis: ( J = proj (1,1) implies ( J is_differentiable_in x0 & diff (J,x0) = J ) )
assume A1: J = proj (1,1) ; ::_thesis: ( J is_differentiable_in x0 & diff (J,x0) = J )
A2: 1 in Seg 1 ;
set R = (REAL 1) --> (0* 1);
set L = <>* J;
 rng J = dom ((proj (1,1)) ") by A1, A2, PDIFF_1:1, PDIFF_1:2;
then A3: dom (<>* J) = dom J by RELAT_1:27
.= REAL 1 by A1, A2, PDIFF_1:1 ;
reconsider L = <>* J as Function of (REAL 1),(REAL 1) by PDIFF_1:2;
set f = <>* J;
A4: L = id (dom J) by A1, FUNCT_1:39
.= id (REAL 1) by A1, A2, PDIFF_1:1 ;
A5: for x, y being Element of REAL 1 holds L . (x + y) = (L . x) + (L . y)
proof
let x, y be Element of REAL 1; ::_thesis: L . (x + y) = (L . x) + (L . y)
thus L . (x + y) = x + y by A4, FUNCT_1:18
.= (L . x) + y by A4, FUNCT_1:18
.= (L . x) + (L . y) by A4, FUNCT_1:18 ; ::_thesis: verum
end;
A6: for x being Element of REAL 1
for r being Real holds L . (r * x) = r * (L . x)
proof
let x be Element of REAL 1; ::_thesis: for r being Real holds L . (r * x) = r * (L . x)
let r be Real; ::_thesis: L . (r * x) = r * (L . x)
thus L . (r * x) = r * x by A4, FUNCT_1:18
.= r * (L . x) by A4, FUNCT_1:18 ; ::_thesis: verum
end;
then A7: L is LinearOperator of 1,1 by A5, PDIFF_6:def_1, PDIFF_6:def_2;
reconsider r0 = 1 as Real ;
A8:  {  y where y is Element of REAL 1 : |.(y - x0).| < r0  }  c= dom (<>* J)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  y where y is Element of REAL 1 : |.(y - x0).| < r0  }  or x in dom (<>* J) )
assume  x in  {  y where y is Element of REAL 1 : |.(y - x0).| < r0  }  ; ::_thesis: x in dom (<>* J)
then  ex y being Element of REAL 1 st
( x = y & |.(y - x0).| < r0 ) ;
hence  x in dom (<>* J) by A3; ::_thesis: verum
end;
A9: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) )
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) ) )
assume A10: r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) )
take d = r; ::_thesis: ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) )
thus  0 < d by A10; ::_thesis: for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r
let z, w be Element of REAL 1; ::_thesis: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z implies (|.z.| ") * |.w.| < r )
assume A11: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z ) ; ::_thesis: (|.z.| ") * |.w.| < r
 w = 0* 1 by A11, FUNCOP_1:7;
then  |.w.| = 0 by EUCLID:7;
hence  (|.z.| ") * |.w.| < r by A10; ::_thesis: verum
end;
A12: for x being Element of REAL 1 st |.(x - x0).| < r0 holds
((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))
proof
let x be Element of REAL 1; ::_thesis: ( |.(x - x0).| < r0 implies ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) )
assume  |.(x - x0).| < r0 ; ::_thesis: ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))
A13: (<>* J) /. x0 = L . x0 by A3, PARTFUN1:def_6;
A14: - 1 is Real by XREAL_0:def_1;
thus ((<>* J) /. x) - ((<>* J) /. x0) = (L . x) - (L . x0) by A13, A3, PARTFUN1:def_6
.= (L . x) + (L . ((- 1) * x0)) by A14, A6
.= L . (x - x0) by A5
.= (L . (x - x0)) + (0* 1) by RVSUM_1:16
.= (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum
end;
then  ( <>* J is_differentiable_in x0 & diff ((<>* J),x0) = L ) by A7, A8, A9, PDIFF_6:24;
hence  J is_differentiable_in x0 by PDIFF_7:def_1; ::_thesis: diff (J,x0) = J
A15: rng J c= REAL ;
thus  diff (J,x0) = (proj (1,1)) * L by A12, A7, A8, A9, PDIFF_6:24
.= ((proj (1,1)) * ((proj (1,1)) ")) * J by RELAT_1:36
.= (id (rng (proj (1,1)))) * J by FUNCT_1:39
.= (id REAL) * J by A2, PDIFF_1:1
.= J by A15, RELAT_1:53 ; ::_thesis: verum
end;

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 & diff (J,x0) = J )
proof
let J be Function of (REAL-NS 1),REAL; ::_thesis: for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds
( J is_differentiable_in x0 & diff (J,x0) = J )
let x0 be Point of (REAL-NS 1); ::_thesis: ( J = proj (1,1) implies ( J is_differentiable_in x0 & diff (J,x0) = J ) )
assume A1: J = proj (1,1) ; ::_thesis: ( J is_differentiable_in x0 & diff (J,x0) = J )
reconsider J0 = J as Function of (REAL 1),REAL by Lm1;
reconsider y0 = x0 as Element of REAL 1 by REAL_NS1:def_4;
 ( J0 is_differentiable_in y0 & diff (J0,y0) = J ) by A1, Th38;
hence  J is_differentiable_in x0 by Def6; ::_thesis: diff (J,x0) = J
 ex g being PartFunc of (REAL 1),REAL ex y being Element of REAL 1 st
( J = g & x0 = y & diff (J,x0) = diff (g,y) ) by Def7;
hence  diff (J,x0) = J by A1, Th38; ::_thesis: verum
end;

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) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )
let I be Function of REAL,(REAL-NS 1); ::_thesis: ( I = (proj (1,1)) " implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) ) )
assume A1: I = (proj (1,1)) " ; ::_thesis: ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )
thus  for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ::_thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n)
proof
let R be RestFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: R * I is RestFunc of (REAL-NS n)
A2: R is total by NDIFF_1:def_5;
reconsider R0 = R as Function of (REAL 1),(REAL n) by A2, Lm1, REAL_NS1:def_4;
reconsider R1 = R * I as PartFunc of REAL,(REAL-NS n) ;
A3: R0 * I is Function of REAL,(REAL n) by Lm1;
then A4: dom R1 = REAL by FUNCT_2:def_1;
A5: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) )
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) ) )
assume  r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) )
then consider d being Real such that
A6: d > 0 and
A7: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r by A2, NDIFF_1:23;
take  d ; ::_thesis: ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) )
 for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r
proof
let z1 be Real; ::_thesis: ( z1 <> 0 & |.z1.| < d implies (|.z1.| ") * ||.(R1 /. z1).|| < r )
assume that
A8: z1 <> 0 and
A9: abs z1 < d ; ::_thesis: (|.z1.| ") * ||.(R1 /. z1).|| < r
reconsider z = I . z1 as Point of (REAL-NS 1) ;
 z1 in REAL ;
then reconsider z1r = z1 as R_eal by NUMBERS:31;
 0 < |.z1r.| by A8, EXTREAL2:4;
then  abs z1 > 0 by EXTREAL2:1;
then  ||.z.|| <> 0 by A1, Lm1, PDIFF_1:3;
then A10: z <> 0. (REAL-NS 1) ;
A11: dom I = REAL by FUNCT_2:def_1;
 R is total by NDIFF_1:def_5;
then  dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2;
then  R /. z = R . (I . z1) by PARTFUN1:def_6;
then  R /. z = R1 . z1 by A11, FUNCT_1:13;
then A12: ||.(R /. z).|| = ||.(R1 /. z1).|| by A4, PARTFUN1:def_6;
A13: ||.z.|| " = (abs z1) " by A1, Lm1, PDIFF_1:3;
 ||.z.|| < d by A1, A9, Lm1, PDIFF_1:3;
hence  (|.z1.| ") * ||.(R1 /. z1).|| < r by A7, A10, A13, A12; ::_thesis: verum
end;
hence  ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) ) by A6; ::_thesis: verum
end;
 for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) )
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) )
A14: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_n0_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n0_<=_m_holds_
||.((((h_")_(#)_(R1_/*_h))_._m)_-_(0._(REAL-NS_n))).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r )
A15: lim h = 0 ;
assume  r > 0 ; ::_thesis: ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r
then consider d being Real such that
A16: d > 0 and
A17: for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r by A5;
reconsider d1 = d as real number ;
consider n0 being Element of NAT  such that
A18: for m being Element of NAT st n0 <= m holds
abs ((h . m) - 0) < d1 by A16, A15, SEQ_2:def_7;
take n0 = n0; ::_thesis: for m being Element of NAT st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r
hereby  ::_thesis: verum
let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r )
A19: h . m <> 0 by SEQ_1:5;
 rng h c= dom R1 by A4;
then A20: ((abs (h . m)) ") * ||.(R1 /. (h . m)).|| = ((abs (h . m)) ") * ||.((R1 /* h) . m).|| by FUNCT_2:109
.= (((abs h) . m) ") * ||.((R1 /* h) . m).|| by SEQ_1:12
.= (((abs h) ") . m) * ||.((R1 /* h) . m).|| by VALUED_1:10
.= ((abs (h ")) . m) * ||.((R1 /* h) . m).|| by SEQ_1:54
.= (abs ((h ") . m)) * ||.((R1 /* h) . m).|| by SEQ_1:12
.= ||.(((h ") . m) * ((R1 /* h) . m)).|| by NORMSP_1:def_1
.= ||.(((h ") (#) (R1 /* h)) . m).|| by NDIFF_1:def_2
.= ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| by RLVECT_1:13 ;
assume  n0 <= m ; ::_thesis: ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r
then  abs ((h . m) - 0) < d by A18;
hence  ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r by A17, A19, A20; ::_thesis: verum
end;
end;
hence  (h ") (#) (R1 /* h) is convergent by NORMSP_1:def_6; ::_thesis: lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n)
hence  lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) by A14, NORMSP_1:def_7; ::_thesis: verum
end;
hence  R * I is RestFunc of (REAL-NS n) by A3, NDIFF_3:def_1; ::_thesis: verum
end;
let L be LinearOperator of (REAL-NS 1),(REAL-NS n); ::_thesis: L * I is LinearFunc of (REAL-NS n)
reconsider L0 = L as Function of (REAL 1),(REAL n) by Lm1, REAL_NS1:def_4;
reconsider L1 = L0 * I as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
reconsider r = L1 . 1 as Point of (REAL-NS n) by FUNCT_2:5;
A21: dom (L0 * I) = REAL by Lm1, FUNCT_2:def_1;
 for p being Real holds L1 . p = p * r
proof
reconsider 1p = I . 1 as VECTOR of (REAL-NS 1) ;
let p be Real; ::_thesis: L1 . p = p * r
 dom I = REAL by FUNCT_2:def_1;
then  L1 . p = L . (I . (p * 1)) by FUNCT_1:13;
then  L1 . p = L . (p * 1p) by A1, Lm1, PDIFF_1:3;
then  L1 . p = p * (L . 1p) by LOPBAN_1:def_5;
hence  L1 . p = p * r by A21, FUNCT_1:12; ::_thesis: verum
end;
hence  L * I is LinearFunc of (REAL-NS n) by NDIFF_3:def_2; ::_thesis: verum
end;

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) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) )
let J be Function of (REAL-NS 1),REAL; ::_thesis: ( J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) ) )
assume A1: J = proj (1,1) ; ::_thesis: ( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) )
thus  for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ::_thesis: for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n)
proof
let R be RestFunc of (REAL-NS n); ::_thesis: R * J is RestFunc of (REAL-NS 1),(REAL-NS n)
A2: R is total by NDIFF_3:def_1;
reconsider R0 = R as Function of REAL,(REAL n) by A2, REAL_NS1:def_4;
reconsider R1 = R0 * J as PartFunc of (REAL-NS 1),(REAL-NS n) by REAL_NS1:def_4;
 for h being non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1) holds
( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS n) )
proof
let h be non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1); ::_thesis: ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS n) )
A3: lim h = 0. (REAL-NS 1) by NDIFF_1:def_4;
deffunc H1( Element of NAT ) ->  Element of REAL = J . (h . $1);
consider s being Real_Sequence such that
A4: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
A5: h is convergent by NDIFF_1:def_4;
A6: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_((s_._n)_-_0)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p )
A7: p is Real by XREAL_0:def_1;
assume  0 < p ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
then consider m being Element of NAT  such that
A8: for n being Element of NAT st m <= n holds
||.((h . n) - (0. (REAL-NS 1))).|| < p by A5, A3, A7, NORMSP_1:def_7;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_((s_._n)_-_0)_<_p
let n be Element of NAT ; ::_thesis: ( m <= n implies abs ((s . n) - 0) < p )
assume  m <= n ; ::_thesis: abs ((s . n) - 0) < p
then  ||.((h . n) - (0. (REAL-NS 1))).|| < p by A8;
then A9: ||.(h . n).|| < p by RLVECT_1:13;
 s . n = J . (h . n) by A4;
hence  abs ((s . n) - 0) < p by A1, A9, PDIFF_1:4; ::_thesis: verum
end;
hence  for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p ; ::_thesis: verum
end;
then A10: s is convergent by SEQ_2:def_6;
then A11: lim s = 0 by A6, SEQ_2:def_7;
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
s_._x_<>_0
let x be set ; ::_thesis: ( x in NAT implies s . x <> 0 )
assume  x in NAT ; ::_thesis: s . x <> 0
then reconsider n = x as Element of NAT ;
A12: 0 <= abs (s . n) by COMPLEX1:46;
 h . n <> 0. (REAL-NS 1) by NDIFF_1:6;
then A13: ||.(h . n).|| <> 0 by NORMSP_0:def_5;
 s . n = J . (h . n) by A4;
then  abs (s . n) <> 0 by A1, A13, PDIFF_1:4;
hence  s . x <> 0 by A12, COMPLEX1:47; ::_thesis: verum
end;
then  s is non-zero by SEQ_1:4;
then reconsider s = s as non-zero 0 -convergent Real_Sequence by A10, A11, FDIFF_1:def_1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((||.h.||_")_(#)_(R1_/*_h)).||_._n_=_||.((s_")_(#)_(R_/*_s)).||_._n
reconsider f1 = R1 as Function ;
let n be Element of NAT ; ::_thesis: ||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.((s ") (#) (R /* s)).|| . n
A14: rng h c= the carrier of (REAL-NS 1) ;
 (R /* s) . n = R . (s . n) by A2, FUNCT_2:115;
then A15: (R /* s) . n = R . (J . (h . n)) by A4;
 NAT = dom h by FUNCT_2:def_1;
then A16: R1 . (h . n) = (f1 * h) . n by FUNCT_1:13;
 rng h c= dom R1 by A14, FUNCT_2:def_1;
then A17: R1 . (h . n) = (R1 /* h) . n by A16, FUNCT_2:def_11;
A18: s . n = J . (h . n) by A4;
||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| by NORMSP_0:def_4
.= ||.(((||.h.|| ") . n) * ((R1 /* h) . n)).|| by NDIFF_1:def_2
.= (abs ((||.h.|| ") . n)) * ||.((R1 /* h) . n).|| by NORMSP_1:def_1
.= (abs ((||.h.|| . n) ")) * ||.((R1 /* h) . n).|| by VALUED_1:10
.= (abs (||.(h . n).|| ")) * ||.((R1 /* h) . n).|| by NORMSP_0:def_4
.= (||.(h . n).|| ") * ||.((R1 /* h) . n).|| by ABSVALUE:def_1
.= ((abs (s . n)) ") * ||.((R1 /* h) . n).|| by A1, A18, PDIFF_1:4
.= ((abs (s . n)) ") * ||.((R /* s) . n).|| by A17, A15, FUNCT_2:15
.= (((abs s) . n) ") * ||.((R /* s) . n).|| by SEQ_1:12
.= (((abs s) ") . n) * ||.((R /* s) . n).|| by VALUED_1:10
.= ((abs (s ")) . n) * ||.((R /* s) . n).|| by SEQ_1:54
.= (abs ((s ") . n)) * ||.((R /* s) . n).|| by SEQ_1:12
.= ||.(((s ") . n) * ((R /* s) . n)).|| by NORMSP_1:def_1
.= ||.(((s ") (#) (R /* s)) . n).|| by NDIFF_1:def_2
.= ||.((s ") (#) (R /* s)).|| . n by NORMSP_0:def_4 ;
hence  ||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.((s ") (#) (R /* s)).|| . n ; ::_thesis: verum
end;
then A19: ||.((||.h.|| ") (#) (R1 /* h)).|| = ||.((s ") (#) (R /* s)).|| by FUNCT_2:63;
A20: lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) by NDIFF_3:def_1;
A21: (s ") (#) (R /* s) is convergent by NDIFF_3:def_1;
A22: lim ||.((s ") (#) (R /* s)).|| = ||.(0. (REAL-NS n)).|| by A20, A21, LOPBAN_1:20
.= 0 ;
A23: ||.((s ") (#) (R /* s)).|| is convergent by A21, NORMSP_1:23;
A24: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n0_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n0_<=_m_holds_
||.((((||.h.||_")_(#)_(R1_/*_h))_._m)_-_(0._(REAL-NS_n))).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p )
assume  0 < p ; ::_thesis: ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p
then consider n0 being Element of NAT  such that
A25: for m being Element of NAT st n0 <= m holds
abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . m) - 0) < p by A19, A23, A22, SEQ_2:def_7;
take n0 = n0; ::_thesis: for m being Element of NAT st n0 <= m holds
||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p
hereby  ::_thesis: verum
let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p )
assume  n0 <= m ; ::_thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p
then  abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . m) - 0) < p by A25;
then A26: abs ||.(((||.h.|| ") (#) (R1 /* h)) . m).|| < p by NORMSP_0:def_4;
 ||.(((||.h.|| ") (#) (R1 /* h)) . m).|| < p by A26, ABSVALUE:def_1;
hence  ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p by RLVECT_1:13; ::_thesis: verum
end;
end;
then  (||.h.|| ") (#) (R1 /* h) is convergent by NORMSP_1:def_6;
hence  ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS n) ) by A24, NORMSP_1:def_7; ::_thesis: verum
end;
hence  R * J is RestFunc of (REAL-NS 1),(REAL-NS n) by NDIFF_1:def_5; ::_thesis: verum
end;
let L be LinearFunc of (REAL-NS n); ::_thesis: L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n)
consider r being Point of (REAL-NS n) such that
A27: for p being Real holds L . p = p * r by NDIFF_3:def_2;
reconsider L0 = L as Function of REAL,(REAL n) by REAL_NS1:def_4;
set K = ||.r.||;
reconsider L1 = L * J as Function of (REAL-NS 1),(REAL-NS n) ;
A28: dom L1 = REAL 1 by Lm1, FUNCT_2:def_1;
A29: now__::_thesis:_for_x,_y_being_Point_of_(REAL-NS_1)_holds_L1_._(x_+_y)_=_(L1_._x)_+_(L1_._y)
let x, y be Point of (REAL-NS 1); ::_thesis: L1 . (x + y) = (L1 . x) + (L1 . y)
 L1 . (x + y) = L . (J . (x + y)) by Lm1, A28, FUNCT_1:12;
then  L1 . (x + y) = L . ((J . x) + (J . y)) by A1, PDIFF_1:4;
then  L1 . (x + y) = ((J . x) + (J . y)) * r by A27;
then  L1 . (x + y) = ((J . x) * r) + ((J . y) * r) by RLVECT_1:def_6;
then  L1 . (x + y) = (L . (J . x)) + ((J . y) * r) by A27;
then A30: L1 . (x + y) = (L . (J . x)) + (L . (J . y)) by A27;
 L . (J . x) = L1 . x by Lm1, A28, FUNCT_1:12;
hence  L1 . (x + y) = (L1 . x) + (L1 . y) by Lm1, A28, A30, FUNCT_1:12; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Point_of_(REAL-NS_1)
for_a_being_Real_holds_L1_._(a_*_x)_=_a_*_(L1_._x)
let x be Point of (REAL-NS 1); ::_thesis: for a being Real holds L1 . (a * x) = a * (L1 . x)
let a be Real; ::_thesis: L1 . (a * x) = a * (L1 . x)
 L1 . (a * x) = L . (J . (a * x)) by Lm1, A28, FUNCT_1:12;
then  L1 . (a * x) = L . (a * (J . x)) by A1, PDIFF_1:4;
then  L1 . (a * x) = (a * (J . x)) * r by A27;
then A31: L1 . (a * x) = a * ((J . x) * r) by RLVECT_1:def_7;
 L . (J . x) = L1 . x by Lm1, A28, FUNCT_1:12;
hence  L1 . (a * x) = a * (L1 . x) by A31, A27; ::_thesis: verum
end;
then reconsider L1 = L1 as LinearOperator of (REAL-NS 1),(REAL-NS n) by A29, VECTSP_1:def_20, LOPBAN_1:def_5;
now__::_thesis:_for_x_being_Point_of_(REAL-NS_1)_holds_||.(L1_._x).||_<=_||.r.||_*_||.x.||
let x be Point of (REAL-NS 1); ::_thesis: ||.(L1 . x).|| <= ||.r.|| * ||.x.||
 ||.(L1 . x).|| = ||.(L . (J . x)).|| by Lm1, A28, FUNCT_1:12;
then  ||.(L1 . x).|| = ||.((J . x) * r).|| by A27;
then  ||.(L1 . x).|| = ||.r.|| * |.(J . x).| by NORMSP_1:def_1;
hence  ||.(L1 . x).|| <= ||.r.|| * ||.x.|| by A1, PDIFF_1:4; ::_thesis: verum
end;
hence  L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def_8; ::_thesis: verum
end;

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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let I be Function of REAL,(REAL-NS 1); ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let x0 be Point of (REAL-NS 1); ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let y0 be Element of REAL ; ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 implies ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) )
assume that
A1: I = (proj (1,1)) " and
A2: x0 in dom f and
A3: y0 in dom g and
A4: x0 = <*y0*> and
A5: f * I = g ; ::_thesis: ( not f is_differentiable_in x0 or ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) )
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
assume A6: f is_differentiable_in x0 ; ::_thesis: ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
then consider NN being Neighbourhood of x0 such that
A7: NN c= dom f and
A8: ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ex R being RestFunc of (REAL-NS 1),(REAL-NS n) st
for x being Point of (REAL-NS 1) st x in NN holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by NDIFF_1:def_6;
A9: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39;
A10: g * J = f * (id (REAL-NS 1)) by A9, A5, RELAT_1:36
.= f by FUNCT_2:17 ;
consider e being Real such that
A11: 0 < e and
A12:  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  c= NN by NFCONT_1:def_1;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))), R being RestFunc of (REAL-NS 1),(REAL-NS n) such that
A13: for x9 being Point of (REAL-NS 1) st x9 in NN holds
(f /. x9) - (f /. x0) = (L . (x9 - x0)) + (R /. (x9 - x0)) by A8;
reconsider R0 = R * I as RestFunc of (REAL-NS n) by A1, Th40;
 L is LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def_9;
then reconsider L0 = L * I as LinearFunc of (REAL-NS n) by A1, Th40;
set N =  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  ;
A14:  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  c= the carrier of (REAL-NS 1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  or y in the carrier of (REAL-NS 1) )
assume  y in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  ; ::_thesis: y in the carrier of (REAL-NS 1)
then  ex z being Point of (REAL-NS 1) st
( y = z & ||.(z - x0).|| < e ) ;
hence  y in the carrier of (REAL-NS 1) ; ::_thesis: verum
end;
then reconsider N =  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  as Neighbourhood of x0 by A11, NFCONT_1:def_1;
set N0 =  {  z where z is Element of REAL : abs (z - y0) < e  }  ;
A15: N c= dom f by A7, A12, XBOOLE_1:1;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y0)_<_e__}__implies_z_in_J_.:_N_)_&_(_z_in_J_.:_N_implies_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y0)_<_e__}__)_)
let z be set ; ::_thesis: ( ( z in  {  z where z is Element of REAL : abs (z - y0) < e  }  implies z in J .: N ) & ( z in J .: N implies z in  {  z where z is Element of REAL : abs (z - y0) < e  }  ) )
hereby  ::_thesis: ( z in J .: N implies z in  {  z where z is Element of REAL : abs (z - y0) < e  }  )
assume  z in  {  z where z is Element of REAL : abs (z - y0) < e  }  ; ::_thesis: z in J .: N
then consider y9 being Element of REAL  such that
A16: z = y9 and
A17: abs (y9 - y0) < e ;
reconsider w = I . y9 as Point of (REAL-NS 1) ;
 x0 = I . y0 by A1, A4, Lm2;
then  w - x0 = I . (y9 - y0) by A1, Lm1, PDIFF_1:3;
then  ||.(w - x0).|| = abs (y9 - y0) by A1, Lm1, PDIFF_1:3;
then A18: w in  {  z0 where z0 is Point of (REAL-NS 1) : ||.(z0 - x0).|| < e  }  by A17;
 J . (I . y9) = y9 by A1, Lm2, FUNCT_1:35;
hence  z in J .: N by A18, A16, FUNCT_2:35; ::_thesis: verum
end;
assume  z in J .: N ; ::_thesis: z in  {  z where z is Element of REAL : abs (z - y0) < e  }
then consider ww being set  such that
 ww in REAL 1 and
A19: ww in N and
A20: z = J . ww by FUNCT_2:64;
consider w being Point of (REAL-NS 1) such that
A21: ww = w and
A22: ||.(w - x0).|| < e by A19;
reconsider y9 = J . w as Element of REAL ;
 J . x0 = y0 by A4, Lm2;
then  J . (w - x0) = y9 - y0 by PDIFF_1:4;
then  abs (y9 - y0) < e by A22, PDIFF_1:4;
hence  z in  {  z where z is Element of REAL : abs (z - y0) < e  }  by A20, A21; ::_thesis: verum
end;
then A23:  {  z where z is Element of REAL : abs (z - y0) < e  }  = J .: N by TARSKI:1;
 J .: (dom f) = J .: (J " (dom g)) by A10, RELAT_1:147;
then A24: J .: (dom f) = dom (f * I) by A5, Lm2, FUNCT_1:77;
A25: I * J = id (REAL 1) by A1, Lm2, FUNCT_1:39;
 N c= dom f by A7, A12, XBOOLE_1:1;
then A26:  {  z where z is Element of REAL : abs (z - y0) < e  }  c= dom (f * I) by A24, A23, RELAT_1:123;
A27: ].(y0 - e),(y0 + e).[ c=  {  z where z is Element of REAL : abs (z - y0) < e  }
proof
now__::_thesis:_for_d_being_set_st_d_in_].(y0_-_e),(y0_+_e).[_holds_
d_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y0)_<_e__}_
let d be set ; ::_thesis: ( d in ].(y0 - e),(y0 + e).[ implies d in  {  z where z is Element of REAL : abs (z - y0) < e  }  )
assume A28: d in ].(y0 - e),(y0 + e).[ ; ::_thesis: d in  {  z where z is Element of REAL : abs (z - y0) < e  }
reconsider y1 = d as Element of REAL by A28;
 abs (y1 - y0) < e by A28, RCOMP_1:1;
hence  d in  {  z where z is Element of REAL : abs (z - y0) < e  }  ; ::_thesis: verum
end;
hence  ].(y0 - e),(y0 + e).[ c=  {  z where z is Element of REAL : abs (z - y0) < e  }  by TARSKI:def_3; ::_thesis: verum
end;
  {  z where z is Element of REAL : abs (z - y0) < e  }  c= ].(y0 - e),(y0 + e).[
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in  {  z where z is Element of REAL : abs (z - y0) < e  }  or d in ].(y0 - e),(y0 + e).[ )
assume  d in  {  z where z is Element of REAL : abs (z - y0) < e  }  ; ::_thesis: d in ].(y0 - e),(y0 + e).[
then  ex r being Element of REAL st
( d = r & abs (r - y0) < e ) ;
hence  d in ].(y0 - e),(y0 + e).[ by RCOMP_1:1; ::_thesis: verum
end;
then   {  z where z is Element of REAL : abs (z - y0) < e  }  = ].(y0 - e),(y0 + e).[ by A27, XBOOLE_0:def_10;
then A29:  {  z where z is Element of REAL : abs (z - y0) < e  }  is Neighbourhood of y0 by A11, RCOMP_1:def_6;
 N c= REAL 1 by A14, REAL_NS1:def_4;
then  (I * J) .: N = N by A25, FRECHET:13;
then A30: I .:  {  z where z is Element of REAL : abs (z - y0) < e  }  = N by A23, RELAT_1:126;
A31: for y1 being Real st y1 in  {  z where z is Element of REAL : abs (z - y0) < e  }  holds
((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0))
proof
let y1 be Real; ::_thesis: ( y1 in  {  z where z is Element of REAL : abs (z - y0) < e  }  implies ((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0)) )
reconsider y9 = I . y1 as Point of (REAL-NS 1) ;
 R is total by NDIFF_1:def_5;
then A32: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2;
 R0 is total by NDIFF_3:def_1;
then A33: dom (R * I) = REAL by PARTFUN1:def_2;
 R /. (I . (y1 - y0)) = R . (I . (y1 - y0)) by A32, PARTFUN1:def_6;
then  R /. (I . (y1 - y0)) = R0 . (y1 - y0) by A33, FUNCT_1:12;
then A34: R /. (I . (y1 - y0)) = R0 /. (y1 - y0) by A33, PARTFUN1:def_6;
 L0 is total ;
then A35: dom (L * I) = REAL by PARTFUN1:def_2;
assume A36: y1 in  {  z where z is Element of REAL : abs (z - y0) < e  }  ; ::_thesis: ((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0))
then A37: I . y1 in N by A30, FUNCT_2:35;
then A38: f /. (I . y1) = f . (I . y1) by A15, PARTFUN1:def_6;
 f /. (I . y1) = (f * I) . y1 by A38, A26, A36, FUNCT_1:12;
then A39: f /. (I . y1) = (f * I) /. y1 by A26, A36, PARTFUN1:def_6;
A40: x0 = I . y0 by A4, A1, Lm2;
then  f /. (I . y0) = f . (I . y0) by A2, PARTFUN1:def_6;
then  f /. (I . y0) = (f * I) . y0 by A3, A5, FUNCT_1:12;
then A41: f /. (I . y0) = (f * I) /. y0 by A3, A5, PARTFUN1:def_6;
 (f /. y9) - (f /. x0) = (L . (y9 - x0)) + (R /. (y9 - x0)) by A13, A12, A37;
then A42: (f /. (I . y1)) - (f /. (I . y0)) = (L . (I . (y1 - y0))) + (R /. (y9 - x0)) by A1, A40, Lm1, PDIFF_1:3;
 L . (I . (y1 - y0)) = L0 . (y1 - y0) by A35, FUNCT_1:12;
hence  ((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0)) by A40, A42, A34, A39, A41, A1, Lm1, PDIFF_1:3; ::_thesis: verum
end;
then A43: f * I is_differentiable_in y0 by A29, A26, NDIFF_3:def_3;
thus  g is_differentiable_in y0 by A5, A31, A29, A26, NDIFF_3:def_3; ::_thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
A44: diff ((f * I),y0) = L0 . 1 by A31, A43, A29, A26, NDIFF_3:def_4;
thus A45: diff (g,y0) = ((diff (f,x0)) * I) . 1 by A5, A44, A6, A13, A7, NDIFF_1:def_7
.= (diff (f,x0)) . (I . 1) by A1, FUNCT_1:13, PDIFF_1:2
.= (diff (f,x0)) . <*1*> by A1, Lm2 ; ::_thesis: for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0))
let r be Element of REAL ; ::_thesis: (diff (f,x0)) . <*r*> = r * (diff (g,y0))
A46: <*1*> is Element of REAL 1 by FINSEQ_2:98;
then reconsider x = <*1*> as Point of (REAL-NS 1) by REAL_NS1:def_4;
A47: diff (f,x0) is LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def_9;
thus (diff (f,x0)) . <*r*> = (diff (f,x0)) . <*(r * 1)*>
.= (diff (f,x0)) . (r * <*1*>) by RVSUM_1:47
.= (diff (f,x0)) . (r * x) by A46, REAL_NS1:3
.= r * (diff (g,y0)) by A45, A47, LOPBAN_1:def_5 ; ::_thesis: verum
end;

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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
proof
let n be non empty Element of NAT ; ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let I be Function of REAL,(REAL-NS 1); ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let x0 be Point of (REAL-NS 1); ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let y0 be Element of REAL ; ::_thesis: 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)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g implies ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) )
assume that
A1: I = (proj (1,1)) " and
A2: x0 in dom f and
A3: y0 in dom g and
A4: x0 = <*y0*> and
A5: f * I = g ; ::_thesis: ( f is_differentiable_in x0 iff g is_differentiable_in y0 )
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
thus  ( f is_differentiable_in x0 implies g is_differentiable_in y0 ) by A2, A3, A4, A5, Th42, A1; ::_thesis: ( g is_differentiable_in y0 implies f is_differentiable_in x0 )
assume  g is_differentiable_in y0 ; ::_thesis: f is_differentiable_in x0
then consider N0 being Neighbourhood of y0 such that
A6: N0 c= dom (f * I) and
A7: ex L being LinearFunc of (REAL-NS n) ex R being RestFunc of (REAL-NS n) st
for y being Real st y in N0 holds
((f * I) /. y) - ((f * I) /. y0) = (L . (y - y0)) + (R /. (y - y0)) by A5, NDIFF_3:def_3;
A8: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39;
A9: g * J = f * (id (REAL-NS 1)) by A5, A8, RELAT_1:36
.= f by FUNCT_2:17 ;
consider e0 being real number  such that
A10: 0 < e0 and
A11: N0 = ].(y0 - e0),(y0 + e0).[ by RCOMP_1:def_6;
reconsider e = e0 as Real by XREAL_0:def_1;
set N =  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  ;
consider L being LinearFunc of (REAL-NS n), R being RestFunc of (REAL-NS n) such that
A12: for y1 being Real st y1 in N0 holds
((f * I) /. y1) - ((f * I) /. y0) = (L . (y1 - y0)) + (R /. (y1 - y0)) by A7;
reconsider R0 = R * J as RestFunc of (REAL-NS 1),(REAL-NS n) by Th41;
reconsider L0 = L * J as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) by Th41;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x0).||_<_e__}__implies_z_in_I_.:_N0_)_&_(_z_in_I_.:_N0_implies_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x0).||_<_e__}__)_)
let z be set ; ::_thesis: ( ( z in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  implies z in I .: N0 ) & ( z in I .: N0 implies z in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  ) )
hereby  ::_thesis: ( z in I .: N0 implies z in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  )
assume  z in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  ; ::_thesis: z in I .: N0
then consider w being Point of (REAL-NS 1) such that
A13: z = w and
A14: ||.(w - x0).|| < e ;
reconsider y2 = J . w as Element of REAL ;
 J . x0 = y0 by A4, Lm2;
then  J . (w - x0) = y2 - y0 by PDIFF_1:4;
then  abs (y2 - y0) < e by A14, PDIFF_1:4;
then A15: y2 in N0 by A11, RCOMP_1:1;
 w in the carrier of (REAL-NS 1) ;
then  w in dom J by Lm2, REAL_NS1:def_4;
then  w = I . y2 by A1, FUNCT_1:34;
hence  z in I .: N0 by A13, A15, FUNCT_2:35; ::_thesis: verum
end;
assume  z in I .: N0 ; ::_thesis: z in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }
then consider yy being set  such that
A16: yy in REAL and
A17: yy in N0 and
A18: z = I . yy by FUNCT_2:64;
reconsider y3 = yy as Element of REAL by A16;
set w = I . y3;
 I . y0 = x0 by A4, A1, Lm2;
then A19: (I . y3) - x0 = I . (y3 - y0) by A1, Lm1, PDIFF_1:3;
 abs (y3 - y0) < e by A11, A17, RCOMP_1:1;
then  ||.((I . y3) - x0).|| < e by A19, A1, Lm1, PDIFF_1:3;
hence  z in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  by A18; ::_thesis: verum
end;
then A20:  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  = I .: N0 by TARSKI:1;
 I .: (dom g) = I .: (I " (dom f)) by A5, RELAT_1:147;
then  I .: (dom g) = dom f by A1, Lm1, FUNCT_1:77, PDIFF_1:2;
then A21:  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  c= dom f by A5, A6, A20, RELAT_1:123;
  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  c= the carrier of (REAL-NS 1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  or y in the carrier of (REAL-NS 1) )
assume  y in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  ; ::_thesis: y in the carrier of (REAL-NS 1)
then  ex z being Point of (REAL-NS 1) st
( y = z & ||.(z - x0).|| < e ) ;
hence  y in the carrier of (REAL-NS 1) ; ::_thesis: verum
end;
then A22:  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  is Neighbourhood of x0 by A10, NFCONT_1:def_1;
 J * I = id REAL by A1, Lm2, FUNCT_1:39;
then  (J * I) .: N0 = N0 by FRECHET:13;
then A23: J .:  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  = N0 by A20, RELAT_1:126;
A24: for y being Point of (REAL-NS 1) st y in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  holds
(f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0))
proof
 x0 in the carrier of (REAL-NS 1) ;
then  x0 in dom J by Lm2, REAL_NS1:def_4;
then  g . (J . x0) = f . x0 by A9, FUNCT_1:13;
then A25: g . (J . x0) = f /. x0 by A2, PARTFUN1:def_6;
A26: J . x0 = y0 by A4, Lm2;
let y be Point of (REAL-NS 1); ::_thesis: ( y in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  implies (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) )
assume A27: y in  {  z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e  }  ; ::_thesis: (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0))
set y3 = J . y;
reconsider p1 = g /. (J . y), p2 = g /. y0, q1 = L . ((J . y) - y0), q2 = R /. ((J . y) - y0) as VECTOR of (REAL-NS n) ;
A28: J . x0 = y0 by A4, Lm2;
 (g /. (J . y)) - (g /. y0) = q1 + q2 by A5, A12, A23, A27, FUNCT_2:35;
then  (g /. (J . y)) - (g /. (J . x0)) = (L . (J . (y - x0))) + (R /. ((J . y) - y0)) by A28, PDIFF_1:4;
then A29: (g /. (J . y)) - (g /. (J . x0)) = (L . (J . (y - x0))) + (R /. (J . (y - x0))) by A28, PDIFF_1:4;
A30: dom L0 = the carrier of (REAL-NS 1) by FUNCT_2:def_1;
 y - x0 in the carrier of (REAL-NS 1) ;
then  y - x0 in dom J by Lm2, REAL_NS1:def_4;
then A31: R . (J . (y - x0)) = (R * J) . (y - x0) by FUNCT_1:13;
 R0 is total by NDIFF_1:def_5;
then A32: dom (R * J) = the carrier of (REAL-NS 1) by PARTFUN1:def_2;
A33: R . (J . (y - x0)) = R0 /. (y - x0) by A31, A32, PARTFUN1:def_6;
 J . (y - x0) in dom R by A32, FUNCT_1:11;
then A34: R /. (J . (y - x0)) = R0 /. (y - x0) by A33, PARTFUN1:def_6;
 y in the carrier of (REAL-NS 1) ;
then A35: y in dom J by Lm2, REAL_NS1:def_4;
 g . (J . y) = f . y by A9, A35, FUNCT_1:13;
then A36: g . (J . y) = f /. y by A21, A27, PARTFUN1:def_6;
 J . y in dom g by A21, A27, A9, FUNCT_1:11;
then  g /. (J . y) = f /. y by A36, PARTFUN1:def_6;
then  (g /. (J . y)) - (g /. (J . x0)) = (f /. y) - (f /. x0) by A3, A26, A25, PARTFUN1:def_6;
hence  (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) by A29, A34, A30, FUNCT_1:12; ::_thesis: verum
end;
 L0 is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) by LOPBAN_1:def_9;
hence  f is_differentiable_in x0 by A22, A21, A24, NDIFF_1:def_6; ::_thesis: verum
end;

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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
proof
let n be non empty Element of NAT ; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let J be Function of (REAL-NS 1),REAL; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let x0 be Point of (REAL-NS 1); ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let y0 be Element of REAL ; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J implies ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) )
assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J ) ; ::_thesis: ( f is_differentiable_in x0 iff g is_differentiable_in y0 )
reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def_4;
A2: J * I = id REAL by A1, Lm2, FUNCT_1:39;
f * I = g * (id REAL) by A1, A2, RELAT_1:36
.= g by FUNCT_2:17 ;
hence  ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) by A1, Th43; ::_thesis: verum
end;

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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds
( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds
( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let J be Function of (REAL-NS 1),REAL; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds
( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let x0 be Point of (REAL-NS 1); ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds
( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let y0 be Element of REAL ; ::_thesis: 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) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds
( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds
( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 implies ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) )
assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 ) ; ::_thesis: ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
hence A2: f is_differentiable_in x0 by Th44; ::_thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def_4;
A3: J * I = id REAL by A1, Lm2, FUNCT_1:39;
f * I = g * (id REAL) by A1, A3, RELAT_1:36
.= g by FUNCT_2:17 ;
hence  ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) by A1, Th42, A2; ::_thesis: verum
end;

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 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
proof
let n be non empty Element of NAT ; ::_thesis: 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 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
let R be RestFunc of (REAL-NS n); ::_thesis: ( R /. 0 = 0. (REAL-NS n) implies for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) ) )
assume A1: R /. 0 = 0. (REAL-NS n) ; ::_thesis: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
let e be Real; ::_thesis: ( e > 0 implies ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) ) )
assume A2: e > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
 R is total by NDIFF_3:def_1;
then consider d being Real such that
A3: d > 0 and
A4: for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < e by A2, Th23;
take  d ; ::_thesis: ( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
now__::_thesis:_for_h_being_Real_st_|.h.|_<_d_holds_
||.(R_/._h).||_<=_e_*_|.h.|
let h be Real; ::_thesis: ( |.h.| < d implies ||.(R /. h).|| <= e * |.h.| )
assume A5: |.h.| < d ; ::_thesis: ||.(R /. h).|| <= e * |.h.|
now__::_thesis:_(_(_h_<>_0_&_||.(R_/._h).||_<=_e_*_|.h.|_)_or_(_h_=_0_&_||.(R_/._h).||_<=_e_*_|.h.|_)_)
percases ( h <> 0 or h = 0 ) ;
caseA6: h <> 0 ; ::_thesis: ||.(R /. h).|| <= e * |.h.|
then  ( 0 <= |.h.| & (|.h.| ") * ||.(R /. h).|| <= e ) by A4, A5, COMPLEX1:46;
then  |.h.| * ((|.h.| ") * ||.(R /. h).||) <= |.h.| * e by XREAL_1:64;
then A7: (|.h.| * (|.h.| ")) * ||.(R /. h).|| <= e * |.h.| ;
 |.h.| <> 0 by A6, COMPLEX1:45;
then  1 * ||.(R /. h).|| <= e * |.h.| by A7, XCMPLX_0:def_7;
hence  ||.(R /. h).|| <= e * |.h.| ; ::_thesis: verum
end;
caseA8: h = 0 ; ::_thesis: ||.(R /. h).|| <= e * |.h.|
reconsider p0 = 0 as Real ;
 0 <= |.h.| by COMPLEX1:46;
then  p0 * |.h.| <= e * |.h.| by A2;
hence  ||.(R /. h).|| <= e * |.h.| by A1, A8; ::_thesis: verum
end;
end;
end;
hence  ||.(R /. h).|| <= e * |.h.| ; ::_thesis: verum
end;
hence  ( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) ) by A3; ::_thesis: verum
end;

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)
proof
let n, m be non empty Element of NAT ; ::_thesis: 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)
let R be RestFunc of (REAL-NS n); ::_thesis: for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)
let L be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); ::_thesis: L * R is RestFunc of (REAL-NS m)
set S = REAL-NS n;
set T = REAL-NS m;
consider K being Real such that
A1: 0 <= K and
A2: for z being Point of (REAL-NS n) holds ||.(L . z).|| <= K * ||.z.|| by LOPBAN_1:def_8;
 dom L = the carrier of (REAL-NS n) by FUNCT_2:def_1;
then A3: rng R c= dom L ;
A4: R is total by NDIFF_3:def_1;
then A5: dom R = REAL by PARTFUN1:def_2;
reconsider p0 = 0 , p1 = 1 as Real ;
A6: p0 + K < p1 + K by XREAL_1:8;
now__::_thesis:_for_ee_being_Real_st_ee_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_h_being_Real_st_h_<>_0_&_|.h.|_<_d_holds_
(|.h.|_")_*_||.((L_*_R)_/._h).||_<_ee_)_)
let ee be Real; ::_thesis: ( ee > 0 implies ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < ee ) ) )
assume A7: ee > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < ee ) )
set e = ee / 2;
 ee / 2 > 0 by A7, XREAL_1:215;
then A8: 0 / (1 + K) < (ee / 2) / (1 + K) by A1, XREAL_1:74;
set e1 = (ee / 2) / (1 + K);
consider d being Real such that
A9: 0 < d and
A10: for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A4, A8, Th23;
A11: ee / 2 < ee by A7, XREAL_1:216;
now__::_thesis:_for_h_being_Real_st_h_<>_0_&_|.h.|_<_d_holds_
(|.h.|_")_*_||.((L_*_R)_/._h).||_<_ee
let h be Real; ::_thesis: ( h <> 0 & |.h.| < d implies (|.h.| ") * ||.((L * R) /. h).|| < ee )
assume that
A12: h <> 0 and
A13: |.h.| < d ; ::_thesis: (|.h.| ") * ||.((L * R) /. h).|| < ee
 (|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A10, A12, A13;
then  (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K)) by A1, XREAL_1:64;
then A14: (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= ee / 2 by A1, XCMPLX_1:87;
 |.h.| <> 0 by A12, COMPLEX1:45;
then A15: |.h.| > 0 by COMPLEX1:46;
A16: K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).|| by A6, XREAL_1:64;
 ||.(L . (R /. h)).|| <= K * ||.(R /. h).|| by A2;
then  ||.(L . (R /. h)).|| <= (K + 1) * ||.(R /. h).|| by A16, XXREAL_0:2;
then  (|.h.| ") * ||.(L . (R /. h)).|| <= (|.h.| ") * ((K + 1) * ||.(R /. h).||) by A15, XREAL_1:64;
then A17: (|.h.| ") * ||.(L . (R /. h)).|| <= ee / 2 by A14, XXREAL_0:2;
L . (R /. h) = L /. (R /. h)
.= (L * R) /. h by A5, A3, PARTFUN2:5 ;
hence  (|.h.| ") * ||.((L * R) /. h).|| < ee by A11, A17, XXREAL_0:2; ::_thesis: verum
end;
hence  ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < ee ) ) by A9; ::_thesis: verum
end;
hence  L * R is RestFunc of (REAL-NS m) by A4, Th23; ::_thesis: verum
end;

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)
proof
let n, m be non empty Element of NAT ; ::_thesis: 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)
set S = REAL-NS n;
set T = REAL-NS m;
let R1 be RestFunc of (REAL-NS n); ::_thesis: ( R1 /. 0 = 0. (REAL-NS n) implies 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) )
assume  R1 /. 0 = 0. (REAL-NS n) ; ::_thesis: 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)
then consider d0 being Real such that
A1: 0 < d0 and
A2: for h being Real st |.h.| < d0 holds
||.(R1 /. h).|| <= 1 * |.h.| by Th46;
let R2 be RestFunc of (REAL-NS n),(REAL-NS m); ::_thesis: ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) implies for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) )
assume A3: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) ; ::_thesis: for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
let L be LinearFunc of (REAL-NS n); ::_thesis: R2 * (L + R1) is RestFunc of (REAL-NS m)
consider r being Point of (REAL-NS n) such that
A4: for h being Real holds L . h = h * r by NDIFF_3:def_2;
set K = ||.r.||;
 R2 is total by NDIFF_1:def_5;
then  dom R2 = the carrier of (REAL-NS n) by PARTFUN1:def_2;
then A5: rng (L + R1) c= dom R2 ;
 R1 is total by NDIFF_3:def_1;
then A6: L + R1 is total by VFUNCT_1:32;
then A7: dom (L + R1) = REAL by PARTFUN1:def_2;
A8: now__::_thesis:_for_ee_being_Real_st_ee_>_0_holds_
ex_dd1_being_Real_st_
(_dd1_>_0_&_(_for_h_being_Real_st_h_<>_0_&_|.h.|_<_dd1_holds_
(|.h.|_")_*_||.((R2_*_(L_+_R1))_/._h).||_<_ee_)_)
let ee be Real; ::_thesis: ( ee > 0 implies ex dd1 being Real st
( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds
(|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) )
assume A9: ee > 0 ; ::_thesis: ex dd1 being Real st
( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds
(|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) )
set e = ee / 2;
A10: ee / 2 < ee by A9, XREAL_1:216;
set e1 = (ee / 2) / (1 + ||.r.||);
 ee / 2 > 0 by A9, XREAL_1:215;
then  0 / (1 + ||.r.||) < (ee / 2) / (1 + ||.r.||) by XREAL_1:74;
then consider d being Real such that
A11: 0 < d and
A12: for z being Point of (REAL-NS n) st ||.z.|| < d holds
||.(R2 /. z).|| <= ((ee / 2) / (1 + ||.r.||)) * ||.z.|| by A3, NDIFF_2:7;
set d1 = d / (1 + ||.r.||);
set dd1 = min (d0,(d / (1 + ||.r.||)));
A13: min (d0,(d / (1 + ||.r.||))) <= d / (1 + ||.r.||) by XXREAL_0:17;
A14: min (d0,(d / (1 + ||.r.||))) <= d0 by XXREAL_0:17;
A15: now__::_thesis:_for_h_being_Real_st_h_<>_0_&_|.h.|_<_min_(d0,(d_/_(1_+_||.r.||)))_holds_
(|.h.|_")_*_||.((R2_*_(L_+_R1))_/._h).||_<_ee
let h be Real; ::_thesis: ( h <> 0 & |.h.| < min (d0,(d / (1 + ||.r.||))) implies (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee )
assume that
A16: h <> 0 and
A17: |.h.| < min (d0,(d / (1 + ||.r.||))) ; ::_thesis: (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee
 |.h.| < d0 by A14, A17, XXREAL_0:2;
then A18: ||.(R1 /. h).|| <= 1 * |.h.| by A2;
A19: L . h = h * r by A4;
reconsider p0 = 0 as Real ;
 (||.(L . h).|| - (||.r.|| * |.h.|)) + (||.r.|| * |.h.|) <= p0 + (||.r.|| * |.h.|) by A19, NORMSP_1:def_1;
then  ( ||.((L . h) + (R1 /. h)).|| <= ||.(L . h).|| + ||.(R1 /. h).|| & ||.(L . h).|| + ||.(R1 /. h).|| <= (||.r.|| * |.h.|) + (1 * |.h.|) ) by A18, NORMSP_1:def_1, XREAL_1:7;
then A20: ||.((L . h) + (R1 /. h)).|| <= (||.r.|| + 1) * |.h.| by XXREAL_0:2;
 |.h.| < d / (1 + ||.r.||) by A13, A17, XXREAL_0:2;
then  (||.r.|| + 1) * |.h.| < (||.r.|| + 1) * (d / (1 + ||.r.||)) by XREAL_1:68;
then  ||.((L . h) + (R1 /. h)).|| < (||.r.|| + 1) * (d / (1 + ||.r.||)) by A20, XXREAL_0:2;
then  ||.((L . h) + (R1 /. h)).|| < d by XCMPLX_1:87;
then A21: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + ||.r.||)) * ||.((L . h) + (R1 /. h)).|| by A12;
 ((ee / 2) / (1 + ||.r.||)) * ||.((L . h) + (R1 /. h)).|| <= ((ee / 2) / (1 + ||.r.||)) * ((||.r.|| + 1) * |.h.|) by A9, A20, XREAL_1:64;
then A22: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + ||.r.||)) * ((||.r.|| + 1) * |.h.|) by A21, XXREAL_0:2;
A23: R2 /. ((L . h) + (R1 /. h)) = R2 /. ((L /. h) + (R1 /. h))
.= R2 /. ((L + R1) /. h) by A7, VFUNCT_1:def_1
.= (R2 * (L + R1)) /. h by A7, A5, PARTFUN2:5 ;
A24: |.h.| <> 0 by A16, COMPLEX1:45;
then  |.h.| > 0 by COMPLEX1:46;
then  (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= (|.h.| ") * ((((ee / 2) / (1 + ||.r.||)) * (||.r.|| + 1)) * |.h.|) by A23, A22, XREAL_1:64;
then  (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= ((|.h.| * (|.h.| ")) * ((ee / 2) / (1 + ||.r.||))) * (||.r.|| + 1) ;
then  (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= (1 * ((ee / 2) / (1 + ||.r.||))) * (||.r.|| + 1) by A24, XCMPLX_0:def_7;
then  (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= ee / 2 by XCMPLX_1:87;
hence  (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee by A10, XXREAL_0:2; ::_thesis: verum
end;
 0 / (1 + ||.r.||) < d / (1 + ||.r.||) by A11, XREAL_1:74;
then  0 < min (d0,(d / (1 + ||.r.||))) by A1, XXREAL_0:15;
hence  ex dd1 being Real st
( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds
(|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) by A15; ::_thesis: verum
end;
dom (R2 * (L + R1)) = dom (L + R1) by A5, RELAT_1:27
.= REAL by A6, PARTFUN1:def_2 ;
then  R2 * (L + R1) is total by PARTFUN1:def_2;
hence  R2 * (L + R1) is RestFunc of (REAL-NS m) by A8, Th23; ::_thesis: verum
end;

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)
proof
let n, m be non empty Element of NAT ; ::_thesis: 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)
let R1 be RestFunc of (REAL-NS n); ::_thesis: ( R1 /. 0 = 0. (REAL-NS n) implies 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) )
assume A1: R1 /. 0 = 0. (REAL-NS n) ; ::_thesis: 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)
let R2 be RestFunc of (REAL-NS n),(REAL-NS m); ::_thesis: ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) implies 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) )
assume A2: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) ; ::_thesis: 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)
let L1 be LinearFunc of (REAL-NS n); ::_thesis: for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)
let L2 be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); ::_thesis: (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)
A3: L2 * R1 is RestFunc of (REAL-NS m) by Th47;
 R2 * (L1 + R1) is RestFunc of (REAL-NS m) by A1, A2, Th48;
hence  (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) by A3, NDIFF_3:7; ::_thesis: verum
end;

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 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
proof
let n, m be non empty Element of NAT ; ::_thesis: 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 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
let x0 be Element of REAL ; ::_thesis: 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 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
set S = REAL-NS n;
set T = REAL-NS m;
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( g is_differentiable_in x0 implies 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 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) )
assume A1: g is_differentiable_in x0 ; ::_thesis: 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 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom g and
A3: ex L1 being LinearFunc of (REAL-NS n) ex R1 being RestFunc of (REAL-NS n) st
( diff (g,x0) = L1 . 1 & ( for x being Real st x in N1 holds
(g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) ) ) by A1, NDIFF_3:def_4;
let f be PartFunc of (REAL-NS n),(REAL-NS m); ::_thesis: ( f is_differentiable_in g /. x0 implies ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) )
assume  f is_differentiable_in g /. x0 ; ::_thesis: ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
then consider N2 being Neighbourhood of g /. x0 such that
A4: N2 c= dom f and
A5: ex R2 being RestFunc of (REAL-NS n),(REAL-NS m) st
( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) & R2 is_continuous_in 0. (REAL-NS n) & ( for y being Point of (REAL-NS n) st y in N2 holds
(f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0))) ) ) by NDIFF_1:47;
consider R2 being RestFunc of (REAL-NS n),(REAL-NS m) such that
A6: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) and
A7: for y being Point of (REAL-NS n) st y in N2 holds
(f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0))) by A5;
reconsider L2 = diff (f,(g /. x0)) as Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) by LOPBAN_1:def_9;
consider L1 being LinearFunc of (REAL-NS n), R1 being RestFunc of (REAL-NS n) such that
A8: ( diff (g,x0) = L1 . 1 & ( for x being Real st x in N1 holds
(g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) ) ) by A3;
consider r being Point of (REAL-NS n) such that
A9: for p being Real holds L1 . p = p * r by NDIFF_3:def_2;
reconsider p0 = 0 as Element of REAL ;
 (g /. x0) - (g /. x0) = (L1 . (x0 - x0)) + (R1 /. (x0 - x0)) by A8, RCOMP_1:16;
then  0. (REAL-NS n) = (L1 . 0) + (R1 /. 0) by RLVECT_1:15;
then  0. (REAL-NS n) = (p0 * r) + (R1 /. 0) by A9;
then  0. (REAL-NS n) = (0. (REAL-NS n)) + (R1 /. 0) by RLVECT_1:10;
then A10: R1 /. 0 = 0. (REAL-NS n) by RLVECT_1:4;
A11: dom (L2 * L1) = REAL by FUNCT_2:def_1;
reconsider q = L2 . r as Point of (REAL-NS m) ;
 for p being Real holds (L2 * L1) . p = p * q
proof
let p be Real; ::_thesis: (L2 * L1) . p = p * q
L2 . (L1 . p) = L2 . (p * r) by A9
.= p * q by LOPBAN_1:def_5 ;
hence  (L2 * L1) . p = p * q by A11, FUNCT_1:12; ::_thesis: verum
end;
then reconsider L0 = L2 * L1 as LinearFunc of (REAL-NS m) by NDIFF_3:def_2;
 g is_continuous_in x0 by A1, NDIFF_3:22;
then consider N3 being Neighbourhood of x0 such that
A12: g .: N3 c= N2 by NFCONT_3:10;
reconsider R0 = (L2 * R1) + (R2 * (L1 + R1)) as RestFunc of (REAL-NS m) by A10, A6, Th49;
consider N being Neighbourhood of x0 such that
A13: N c= N1 and
A14: N c= N3 by RCOMP_1:17;
A15: N c= dom (f * g)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N or x in dom (f * g) )
assume A16: x in N ; ::_thesis: x in dom (f * g)
then reconsider x9 = x as Real ;
A17: x in N1 by A13, A16;
then  g . x9 in g .: N3 by A2, A14, A16, FUNCT_1:def_6;
then  g . x9 in N2 by A12;
hence  x in dom (f * g) by A2, A4, A17, FUNCT_1:11; ::_thesis: verum
end;
A18: now__::_thesis:_for_x_being_Real_st_x_in_N_holds_
((f_*_g)_/._x)_-_((f_*_g)_/._x0)_=_(L0_._(x_-_x0))_+_(R0_/._(x_-_x0))
let x be Real; ::_thesis: ( x in N implies ((f * g) /. x) - ((f * g) /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0)) )
assume A19: x in N ; ::_thesis: ((f * g) /. x) - ((f * g) /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0))
A20: (g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A8, A13, A19;
 x in N1 by A13, A19;
then  g . x in g .: N3 by A2, A14, A19, FUNCT_1:def_6;
then A21: g . x in N2 by A12;
 x in N1 by A13, A19;
then A22: g /. x in N2 by A2, A21, PARTFUN1:def_6;
A23: x0 in N by RCOMP_1:16;
A24: R1 is total by NDIFF_3:def_1;
then A25: dom R1 = REAL by PARTFUN1:def_2;
 dom L2 = the carrier of (REAL-NS n) by FUNCT_2:def_1;
then A26: rng R1 c= dom L2 ;
A27: dom (L2 * R1) = REAL by A24, PARTFUN1:def_2;
A28: L1 + R1 is total by A24, VFUNCT_1:32;
then A29: dom (L1 + R1) = REAL by PARTFUN1:def_2;
 R2 is total by NDIFF_1:def_5;
then  dom R2 = the carrier of (REAL-NS n) by PARTFUN1:def_2;
then A30: rng (L1 + R1) c= dom R2 ;
then  dom (R2 * (L1 + R1)) = dom (L1 + R1) by RELAT_1:27
.= REAL by A28, PARTFUN1:def_2 ;
then A31: dom ((L2 * R1) + (R2 * (L1 + R1))) = REAL /\ REAL by A27, VFUNCT_1:def_1
.= REAL ;
A32: L2 . (R1 /. (x - x0)) = L2 /. (R1 /. (x - x0))
.= (L2 * R1) /. (x - x0) by A25, A26, PARTFUN2:5 ;
A33: R2 /. ((L1 . (x - x0)) + (R1 /. (x - x0))) = R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0)))
.= R2 /. ((L1 + R1) /. (x - x0)) by A29, VFUNCT_1:def_1
.= (R2 * (L1 + R1)) /. (x - x0) by A29, A30, PARTFUN2:5 ;
A34: (L2 * L1) . (x - x0) = L2 . (L1 . (x - x0)) by A11, FUNCT_1:12;
thus ((f * g) /. x) - ((f * g) /. x0) = (f /. (g /. x)) - ((f * g) /. x0) by A15, A19, PARTFUN2:3
.= (f /. (g /. x)) - (f /. (g /. x0)) by A15, A23, PARTFUN2:3
.= ((diff (f,(g /. x0))) . ((g /. x) - (g /. x0))) + (R2 /. ((g /. x) - (g /. x0))) by A7, A22
.= ((L2 . (L1 . (x - x0))) + (L2 . (R1 /. (x - x0)))) + ((R2 * (L1 + R1)) /. (x - x0)) by A20, A33, VECTSP_1:def_20
.= (L2 . (L1 . (x - x0))) + (((L2 * R1) /. (x - x0)) + ((R2 * (L1 + R1)) /. (x - x0))) by A32, RLVECT_1:def_3
.= (L0 . (x - x0)) + (R0 /. (x - x0)) by A34, A31, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence A35: f * g is_differentiable_in x0 by A15, NDIFF_3:def_3; ::_thesis: diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0))
 (L2 * L1) . 1 = (diff (f,(g /. x0))) . (diff (g,x0)) by A8, A11, FUNCT_1:12;
hence  diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) by A35, A15, A18, NDIFF_3:def_4; ::_thesis: verum
end;