:: NDIFF_3 semantic presentation

begin

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

theorem Th1: :: NDIFF_3:1
for G being RealNormSpace
for s1 being Real_Sequence
for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds
( seq is convergent & lim seq = 0. G )
proof
let G be RealNormSpace; ::_thesis: for s1 being Real_Sequence
for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds
( seq is convergent & lim seq = 0. G )
let s1 be Real_Sequence; ::_thesis: for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds
( seq is convergent & lim seq = 0. G )
let seq be sequence of G; ::_thesis: ( ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 implies ( seq is convergent & lim seq = 0. G ) )
assume that
A1: for n being Element of NAT holds ||.(seq . n).|| <= s1 . n and
A2: s1 is convergent and
A3: lim s1 = 0 ; ::_thesis: ( seq is convergent & lim seq = 0. G )
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_
||.((seq_._m)_-_(0._G)).||_<_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
||.((seq . m) - (0. G)).|| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. G)).|| < p
then consider n being Element of NAT  such that
A4: for m being Element of NAT st n <= m holds
abs ((s1 . m) - 0) < p by A2, A3, SEQ_2:def_7;
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq_._m)_-_(0._G)).||_<_p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (0. G)).|| < p )
assume  n <= m ; ::_thesis: ||.((seq . m) - (0. G)).|| < p
then A5: abs ((s1 . m) - 0) < p by A4;
A6: ||.((seq . m) - (0. G)).|| = ||.(seq . m).|| by RLVECT_1:13;
A7: s1 . m <= abs (s1 . m) by ABSVALUE:4;
 ||.(seq . m).|| <= s1 . m by A1;
then  ||.((seq . m) - (0. G)).|| <= abs (s1 . m) by A6, A7, XXREAL_0:2;
hence  ||.((seq . m) - (0. G)).|| < p by A5, XXREAL_0:2; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. G)).|| < p ; ::_thesis: verum
end;
then A8: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. G)).|| < p ;
hence  seq is convergent by NORMSP_1:def_6; ::_thesis: lim seq = 0. G
hence  lim seq = 0. G by A8, NORMSP_1:def_7; ::_thesis: verum
end;

theorem Th2: :: NDIFF_3:2
for G being RealNormSpace
for k being Element of NAT
for s1 being Real_Sequence
for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
proof
let G be RealNormSpace; ::_thesis: for k being Element of NAT
for s1 being Real_Sequence
for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
let k be Element of NAT ; ::_thesis: for s1 being Real_Sequence
for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
let s1 be Real_Sequence; ::_thesis: for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
let seq be sequence of G; ::_thesis: (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
now__::_thesis:_for_n_being_Element_of_NAT_holds_((s1_(#)_seq)_^\_k)_._n_=_((s1_^\_k)_(#)_(seq_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((s1 (#) seq) ^\ k) . n = ((s1 ^\ k) (#) (seq ^\ k)) . n
thus ((s1 (#) seq) ^\ k) . n = (s1 (#) seq) . (n + k) by NAT_1:def_3
.= (s1 . (n + k)) * (seq . (n + k)) by NDIFF_1:def_2
.= ((s1 ^\ k) . n) * (seq . (n + k)) by NAT_1:def_3
.= ((s1 ^\ k) . n) * ((seq ^\ k) . n) by NAT_1:def_3
.= ((s1 ^\ k) (#) (seq ^\ k)) . n by NDIFF_1:def_2 ; ::_thesis: verum
end;
hence  (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k by FUNCT_2:63; ::_thesis: verum
end;

definition
let F be non trivial RealNormSpace;
let IT be PartFunc of REAL, the carrier of F;
attrIT is RestFunc-like  means :Def1: :: NDIFF_3:def 1
( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) );
end;

:: deftheorem Def1 defines RestFunc-like NDIFF_3:def_1_:_
 for F being non trivial RealNormSpace
for IT being PartFunc of REAL, the carrier of F holds
( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) ) );

registration
let F be non trivial RealNormSpace;
clusterV13() V16( REAL ) V17( the carrier of F) Function-like RestFunc-like for Element of K6(K7(REAL, the carrier of F));
existence
 ex b1 being PartFunc of REAL, the carrier of F st b1 is RestFunc-like
proof
take f = REAL --> (0. F); ::_thesis: f is RestFunc-like
thus  f is total ; :: according to NDIFF_3:def_1 ::_thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F )
A1: dom f = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_(f_/*_h)_is_convergent_&_lim_((h_")_(#)_(f_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(f_/*_h))_._n_=_0._F
let n be Nat; ::_thesis: ((h ") (#) (f /* h)) . n = 0. F
A2: rng h c= dom f by A1;
A3: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by NDIFF_1:def_2
.= ((h ") . n) * (f . (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
::_thesis: verum
end;
then  ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0. F ) by VALUED_0:def_18;
hence  ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum
end;
hence  for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) ; ::_thesis: verum
end;
end;

definition
let F be non trivial RealNormSpace;
mode RestFunc of F is RestFunc-like PartFunc of REAL, the carrier of F;
end;

definition
let F be non trivial RealNormSpace;
let IT be Function of REAL, the carrier of F;
attrIT is linear  means :Def2: :: NDIFF_3:def 2
 ex r being Point of F st
for p being Real holds IT . p = p * r;
end;

:: deftheorem Def2 defines linear NDIFF_3:def_2_:_
 for F being non trivial RealNormSpace
for IT being Function of REAL, the carrier of F holds
( IT is linear iff ex r being Point of F st
for p being Real holds IT . p = p * r );

registration
let F be non trivial RealNormSpace;
clusterV1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total linear for Element of K6(K7(REAL, the carrier of F));
existence
 ex b1 being Function of REAL, the carrier of F st b1 is linear
proof
deffunc H1( Element of REAL ) ->  Element of the carrier of F = F * (0. F);
consider f being Function of REAL, the carrier of F such that
A1: for x being Element of REAL holds f . x = H1(x) from FUNCT_2:sch_4();
take  f ; ::_thesis: f is linear
thus  f is linear by Def2, A1; ::_thesis: verum
end;
end;

definition
let F be non trivial RealNormSpace;
mode LinearFunc of F is linear Function of REAL, the carrier of F;
end;


theorem Th3: :: NDIFF_3:3
for F being non trivial RealNormSpace
for L1, L2 being LinearFunc of F holds
( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F )
proof
let F be non trivial RealNormSpace; ::_thesis: for L1, L2 being LinearFunc of F holds
( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F )
let L1, L2 be LinearFunc of F; ::_thesis: ( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F )
consider g1 being Point of F such that
A1: for p being Real holds L1 . p = p * g1 by Def2;
consider g2 being Point of F such that
A2: for p being Real holds L2 . p = p * g2 by Def2;
A3: L1 + L2 is total by VFUNCT_1:32;
then A4: dom (L1 + L2) = REAL by FUNCT_2:def_1;
now__::_thesis:_for_p_being_Real_holds_(L1_+_L2)_._p_=_p_*_(g1_+_g2)
let p be Real; ::_thesis: (L1 + L2) . p = p * (g1 + g2)
thus (L1 + L2) . p = (L1 + L2) /. p by A4, PARTFUN1:def_6
.= (L1 /. p) + (L2 /. p) by VFUNCT_1:37
.= (p * g1) + (L2 . p) by A1
.= (p * g1) + (p * g2) by A2
.= p * (g1 + g2) by RLVECT_1:def_5 ; ::_thesis: verum
end;
hence  L1 + L2 is LinearFunc of F by A3, Def2; ::_thesis: L1 - L2 is LinearFunc of F
A5: L1 - L2 is total by VFUNCT_1:32;
then A6: dom (L1 - L2) = REAL by FUNCT_2:def_1;
now__::_thesis:_for_p_being_Real_holds_(L1_-_L2)_._p_=_p_*_(g1_-_g2)
let p be Real; ::_thesis: (L1 - L2) . p = p * (g1 - g2)
thus (L1 - L2) . p = (L1 - L2) /. p by A6, PARTFUN1:def_6
.= (L1 /. p) - (L2 /. p) by VFUNCT_1:37
.= (p * g1) - (L2 . p) by A1
.= (p * g1) - (p * g2) by A2
.= p * (g1 - g2) by RLVECT_1:34 ; ::_thesis: verum
end;
hence  L1 - L2 is LinearFunc of F by A5, Def2; ::_thesis: verum
end;

theorem Th4: :: NDIFF_3:4
for F being non trivial RealNormSpace
for r being Real
for L being LinearFunc of F holds r (#) L is LinearFunc of F
proof
let F be non trivial RealNormSpace; ::_thesis: for r being Real
for L being LinearFunc of F holds r (#) L is LinearFunc of F
let r be Real; ::_thesis: for L being LinearFunc of F holds r (#) L is LinearFunc of F
let L be LinearFunc of F; ::_thesis: r (#) L is LinearFunc of F
consider g being Point of F such that
A1: for p being Real holds L . p = p * g by Def2;
A2: r (#) L is total by VFUNCT_1:34;
then A3: dom (r (#) L) = REAL by FUNCT_2:def_1;
now__::_thesis:_for_p_being_Real_holds_(r_(#)_L)_._p_=_p_*_(r_*_g)
let p be Real; ::_thesis: (r (#) L) . p = p * (r * g)
thus (r (#) L) . p = (r (#) L) /. p by A3, PARTFUN1:def_6
.= r * (L /. p) by VFUNCT_1:39
.= r * (p * g) by A1
.= (r * p) * g by RLVECT_1:def_7
.= p * (r * g) by RLVECT_1:def_7 ; ::_thesis: verum
end;
hence  r (#) L is LinearFunc of F by A2, Def2; ::_thesis: verum
end;

theorem Th5: :: NDIFF_3:5
for F being non trivial RealNormSpace
for h1, h2 being PartFunc of REAL, the carrier of F
for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proof
let F be non trivial RealNormSpace; ::_thesis: for h1, h2 being PartFunc of REAL, the carrier of F
for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let h1, h2 be PartFunc of REAL, the carrier of F; ::_thesis: for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let seq be Real_Sequence; ::_thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) )
A1: (dom h1) /\ (dom h2) c= dom h1 by XBOOLE_1:17;
A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17;
assume A3: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
then A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def_1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_+_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_+_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)
A5: seq . n in rng seq by FUNCT_2:4;
thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A4, FUNCT_2:109
.= (h1 /. (seq . n)) + (h2 /. (seq . n)) by A4, A5, VFUNCT_1:def_1
.= ((h1 /* seq) . n) + (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1
.= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum
end;
hence  (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NORMSP_1:def_2; ::_thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)
A6: rng seq c= dom (h1 - h2) by A3, VFUNCT_1:def_2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_-_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_-_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)
A7: seq . n in rng seq by FUNCT_2:4;
thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A6, FUNCT_2:109
.= (h1 /. (seq . n)) - (h2 /. (seq . n)) by A6, A7, VFUNCT_1:def_2
.= ((h1 /* seq) . n) - (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1
.= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum
end;
hence  (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by NORMSP_1:def_3; ::_thesis: verum
end;

theorem Th6: :: NDIFF_3:6
for F being non trivial RealNormSpace
for h1, h2 being PartFunc of REAL, the carrier of F
for seq being Real_Sequence st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proof
let F be non trivial RealNormSpace; ::_thesis: for h1, h2 being PartFunc of REAL, the carrier of F
for seq being Real_Sequence st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let h1, h2 be PartFunc of REAL, the carrier of F; ::_thesis: for seq being Real_Sequence st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let seq be Real_Sequence; ::_thesis: ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) )
assume  ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
then  h1 + h2 is total by VFUNCT_1:32;
then  dom (h1 + h2) = REAL by PARTFUN1:def_2;
then  (dom h1) /\ (dom h2) = REAL by VFUNCT_1:def_1;
then A1: rng seq c= (dom h1) /\ (dom h2) ;
hence  (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by Th5; ::_thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)
thus  (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, Th5; ::_thesis: verum
end;

theorem Th7: :: NDIFF_3:7
for F being non trivial RealNormSpace
for R1, R2 being RestFunc of F holds
( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )
proof
let F be non trivial RealNormSpace; ::_thesis: for R1, R2 being RestFunc of F holds
( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )
let R1, R2 be RestFunc of F; ::_thesis: ( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )
A1: ( R1 is total & R2 is total ) by Def1;
A2: now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((R1_+_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_+_R2)_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R1 + R2) /* h) is convergent & lim ((h ") (#) ((R1 + R2) /* h)) = 0. F )
A3: (h ") (#) ((R1 + R2) /* h) = (h ") (#) ((R1 /* h) + (R2 /* h)) by A1, Th6
.= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by NDIFF_1:9 ;
A4: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def1;
hence  (h ") (#) ((R1 + R2) /* h) is convergent by A3, NORMSP_1:19; ::_thesis: lim ((h ") (#) ((R1 + R2) /* h)) = 0. F
 ( lim ((h ") (#) (R1 /* h)) = 0. F & lim ((h ") (#) (R2 /* h)) = 0. F ) by Def1;
hence  lim ((h ") (#) ((R1 + R2) /* h)) = (0. F) + (0. F) by A4, A3, NORMSP_1:25
.= 0. F by RLVECT_1:def_4 ;
::_thesis: verum
end;
 R1 + R2 is total by A1, VFUNCT_1:32;
hence  R1 + R2 is RestFunc of F by A2, Def1; ::_thesis: R1 - R2 is RestFunc of F
A5: now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((R1_-_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_-_R2)_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R1 - R2) /* h) is convergent & lim ((h ") (#) ((R1 - R2) /* h)) = 0. F )
A6: (h ") (#) ((R1 - R2) /* h) = (h ") (#) ((R1 /* h) - (R2 /* h)) by A1, Th6
.= ((h ") (#) (R1 /* h)) - ((h ") (#) (R2 /* h)) by NDIFF_1:12 ;
A7: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def1;
hence  (h ") (#) ((R1 - R2) /* h) is convergent by A6, NORMSP_1:20; ::_thesis: lim ((h ") (#) ((R1 - R2) /* h)) = 0. F
 ( lim ((h ") (#) (R1 /* h)) = 0. F & lim ((h ") (#) (R2 /* h)) = 0. F ) by Def1;
hence  lim ((h ") (#) ((R1 - R2) /* h)) = (0. F) - (0. F) by A7, A6, NORMSP_1:26
.= 0. F by RLVECT_1:13 ;
::_thesis: verum
end;
 R1 - R2 is total by A1, VFUNCT_1:32;
hence  R1 - R2 is RestFunc of F by A5, Def1; ::_thesis: verum
end;

theorem Th8: :: NDIFF_3:8
for F being non trivial RealNormSpace
for r being Real
for R being RestFunc of F holds r (#) R is RestFunc of F
proof
let F be non trivial RealNormSpace; ::_thesis: for r being Real
for R being RestFunc of F holds r (#) R is RestFunc of F
let r be Real; ::_thesis: for R being RestFunc of F holds r (#) R is RestFunc of F
let R be RestFunc of F; ::_thesis: r (#) R is RestFunc of F
A1: R is total by Def1;
then A2: r (#) R is total by VFUNCT_1:34;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((r_(#)_R)_/*_h)_is_convergent_&_lim_((h_")_(#)_((r_(#)_R)_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((r (#) R) /* h) is convergent & lim ((h ") (#) ((r (#) R) /* h)) = 0. F )
 dom R = REAL by A1, FUNCT_2:def_1;
then  rng h c= dom R ;
then A3: (h ") (#) ((r (#) R) /* h) = (h ") (#) (r * (R /* h)) by NFCONT_3:4
.= r * ((h ") (#) (R /* h)) by NDIFF_1:10 ;
A4: (h ") (#) (R /* h) is convergent by Def1;
hence  (h ") (#) ((r (#) R) /* h) is convergent by A3, NORMSP_1:22; ::_thesis: lim ((h ") (#) ((r (#) R) /* h)) = 0. F
 lim ((h ") (#) (R /* h)) = 0. F by Def1;
hence  lim ((h ") (#) ((r (#) R) /* h)) = r * (0. F) by A4, A3, NORMSP_1:28
.= 0. F by RLVECT_1:10 ;
::_thesis: verum
end;
hence  r (#) R is RestFunc of F by A2, Def1; ::_thesis: verum
end;

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let x0 be real number ;
predf is_differentiable_in x0 means :Def3: :: NDIFF_3:def 3
 ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) );
end;

:: deftheorem Def3 defines is_differentiable_in NDIFF_3:def_3_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being real number holds
( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) );

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let x0 be real number ;
assume A1: f is_differentiable_in x0 ;
func diff (f,x0) ->  Point of F means :Def4: :: NDIFF_3:def 4
 ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( it = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) );
existence
 ex b1 being Point of F ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( b1 = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) )
proof
consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3;
consider L being LinearFunc of F, R being RestFunc of F such that
A4: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3;
consider r being Point of F such that
A5: for p being Real holds L . p = p * r by Def2;
take  r ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( r = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) )
L . 1 = 1 * r by A5
.= r by RLVECT_1:def_8 ;
hence  ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( r = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) by A2, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Point of F st ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( b1 = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( b2 = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) holds
b1 = b2
proof
let r, s be Point of F; ::_thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( r = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( s = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) implies r = s )
assume that
A6: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( r = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) and
A7: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( s = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) ; ::_thesis: r = s
consider N being Neighbourhood of x0 such that
 N c= dom f and
A8: ex L being LinearFunc of F ex R being RestFunc of F st
( r = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) by A6;
consider L being LinearFunc of F, R being RestFunc of F such that
A9: r = L . 1 and
A10: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8;
consider r1 being Point of F such that
A11: for p being Real holds L . p = p * r1 by Def2;
consider N1 being Neighbourhood of x0 such that
 N1 c= dom f and
A12: ex L being LinearFunc of F ex R being RestFunc of F st
( s = L . 1 & ( for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) by A7;
consider L1 being LinearFunc of F, R1 being RestFunc of F such that
A13: s = L1 . 1 and
A14: for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A12;
consider p1 being Point of F such that
A15: for p being Real holds L1 . p = p * p1 by Def2;
consider N0 being Neighbourhood of x0 such that
A16: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;
consider g being real number  such that
A17: 0 < g and
A18: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
deffunc H1( Element of NAT ) ->  Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A19: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_s1_._n
let n be Element of NAT ; ::_thesis: 0 <> s1 . n
 0 <> g / (n + 2) by A17, XREAL_1:139;
hence  0 <> s1 . n by A19; ::_thesis: verum
end;
then A20: s1 is non-zero by SEQ_1:5;
 ( s1 is convergent & lim s1 = 0 ) by A19, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A20, FDIFF_1:def_1;
A21: for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
proof
let n be Element of NAT ; ::_thesis: ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
take x = x0 + (g / (n + 2)); ::_thesis: ( x in N & x in N1 & h . n = x - x0 )
reconsider z0 = 0 as Element of NAT ;
 z0 + 1 < (n + 1) + 1 by XREAL_1:6;
then  g / (n + 2) < g / 1 by A17, XREAL_1:76;
then A22: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6;
 0 < g / (n + 2) by A17, XREAL_1:139;
then  x0 + (- g) < x0 + (g / (n + 2)) by A17, XREAL_1:6;
then  x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A22;
hence  ( x in N & x in N1 & h . n = x - x0 ) by A16, A18, A19; ::_thesis: verum
end;
A23: s = 1 * p1 by A13, A15;
A24: r = 1 * r1 by A9, A11;
A25: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_
((x_-_x0)_*_r)_+_(R_/._(x_-_x0))_=_((x_-_x0)_*_s)_+_(R1_/._(x_-_x0))
let x be Real; ::_thesis: ( x in N & x in N1 implies ((x - x0) * r) + (R /. (x - x0)) = ((x - x0) * s) + (R1 /. (x - x0)) )
assume that
A26: x in N and
A27: x in N1 ; ::_thesis: ((x - x0) * r) + (R /. (x - x0)) = ((x - x0) * s) + (R1 /. (x - x0))
 (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A10, A26;
then  (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A14, A27;
then  ((x - x0) * r1) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A11;
then  (((x - x0) * 1) * r1) + (R /. (x - x0)) = (((x - x0) * 1) * p1) + (R1 /. (x - x0)) by A15;
then  (((x - x0) * 1) * r) + (R /. (x - x0)) = (((x - x0) * 1) * p1) + (R1 /. (x - x0)) by A24, RLVECT_1:def_7;
hence  ((x - x0) * r) + (R /. (x - x0)) = ((x - x0) * s) + (R1 /. (x - x0)) by A23, RLVECT_1:def_7; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n
 R1 is total by Def1;
then  dom R1 = REAL by PARTFUN1:def_2;
then A28: rng h c= dom R1 ;
let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
 R is total by Def1;
then  dom R = REAL by PARTFUN1:def_2;
then A29: rng h c= dom R ;
A30: n in NAT by ORDINAL1:def_12;
then  ex x being Real st
( x in N & x in N1 & h . n = x - x0 ) by A21;
then  ((h . n) * r) + (R /. (h . n)) = ((h . n) * s) + (R1 /. (h . n)) by A25;
then  ((1 / (h . n)) * ((h . n) * r)) + ((1 / (h . n)) * (R /. (h . n))) = (1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n))) by RLVECT_1:def_5;
then  (((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n))) = (1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n))) by RLVECT_1:def_7;
then A31: (((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n))) = ((1 / (h . n)) * ((h . n) * s)) + ((1 / (h . n)) * (R1 /. (h . n))) by RLVECT_1:def_5;
A32: (1 / (h . n)) * (R /. (h . n)) = ((h . n) ") * (R /. (h . n)) by XCMPLX_1:215
.= ((h ") . n) * (R /. (h . n)) by VALUED_1:10
.= ((h ") . n) * ((R /* h) . n) by A30, A29, FUNCT_2:109
.= ((h ") (#) (R /* h)) . n by A30, NDIFF_1:def_2 ;
A33: h . n <> 0 by A30, SEQ_1:5;
A34: (1 / (h . n)) * (R1 /. (h . n)) = ((h . n) ") * (R1 /. (h . n)) by XCMPLX_1:215
.= ((h ") . n) * (R1 /. (h . n)) by VALUED_1:10
.= ((h ") . n) * ((R1 /* h) . n) by A30, A28, FUNCT_2:109
.= ((h ") (#) (R1 /* h)) . n by A30, NDIFF_1:def_2 ;
A35: ((1 / (h . n)) * (h . n)) * s = 1 * s by A33, XCMPLX_1:106
.= s by RLVECT_1:def_8 ;
((1 / (h . n)) * (h . n)) * r = 1 * r by A33, XCMPLX_1:106
.= r by RLVECT_1:def_8 ;
then  r + (((h ") (#) (R /* h)) . n) = s + (((h ") (#) (R1 /* h)) . n) by A31, A35, A32, A34, RLVECT_1:def_7;
then  r + ((((h ") (#) (R /* h)) . n) - (((h ") (#) (R /* h)) . n)) = (s + (((h ") (#) (R1 /* h)) . n)) - (((h ") (#) (R /* h)) . n) by RLVECT_1:28;
then  r + ((((h ") (#) (R /* h)) . n) - (((h ") (#) (R /* h)) . n)) = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by RLVECT_1:28;
then  r + (0. F) = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by RLVECT_1:15;
then  r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by RLVECT_1:4;
then  r - s = ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) + (s - s) by RLVECT_1:28;
then  r - s = ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) + (0. F) by RLVECT_1:15;
then A36: r - s = (((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n) by RLVECT_1:4;
 n is Element of NAT by ORDINAL1:def_12;
hence  r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A36, NORMSP_1:def_3; ::_thesis: verum
end;
then  ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 0 = r - s ) by VALUED_0:def_18;
then A37: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by NDIFF_1:18;
A38: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. F ) by Def1;
 ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. F ) by Def1;
then  r - s = (0. F) - (0. F) by A37, A38, NORMSP_1:26;
hence  r = s by RLVECT_1:13, RLVECT_1:21; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines diff NDIFF_3:def_4_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being real number st f is_differentiable_in x0 holds
for b4 being Point of F holds
( b4 = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( b4 = L . 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) );

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let X be set ;
predf is_differentiable_on X means :Def5: :: NDIFF_3:def 5
( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def5 defines is_differentiable_on NDIFF_3:def_5_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
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 Th9: :: NDIFF_3:9
for F being non trivial RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
X is Subset of REAL
proof
let F be non trivial RealNormSpace; ::_thesis: for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
X is Subset of REAL
let X be set ; ::_thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
X is Subset of REAL
let f be PartFunc of REAL, the carrier of F; ::_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 Def5;
hence  X is Subset of REAL by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th10: :: NDIFF_3:10
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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 F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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, the carrier of F 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, the carrier of F; ::_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 ) ) )
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 ) )
hence A2: Z c= dom f by Def5; ::_thesis: for x being Real st x in Z holds
f is_differentiable_in x
let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A3: x0 in Z ; ::_thesis: f is_differentiable_in x0
then  f | Z is_differentiable_in x0 by A1, Def5;
then consider N being Neighbourhood of x0 such that
A4: N c= dom (f | Z) and
A5: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
take  N ; :: according to NDIFF_3:def_3 ::_thesis: ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
 dom (f | Z) = (dom f) /\ Z by RELAT_1:61;
then  dom (f | Z) c= dom f by XBOOLE_1:17;
hence  N c= dom f by A4, XBOOLE_1:1; ::_thesis: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
consider L being LinearFunc of F, R being RestFunc of F such that
A6: for x being Real st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5;
now__::_thesis:_for_x_being_Real_st_x_in_N_holds_
(f_/._x)_-_(f_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A7: x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then A8: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6;
 (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8, A4, A7, PARTFUN2:15;
hence  (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, A3, PARTFUN2:17; ::_thesis: verum
end;
hence  ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; ::_thesis: verum
end;
assume that
A9: Z c= dom f and
A10: for x being Real st x in Z holds
f is_differentiable_in x ; ::_thesis: f is_differentiable_on Z
thus  Z c= dom f by A9; :: according to NDIFF_3:def_5 ::_thesis: for x being Real st x in Z holds
f | Z is_differentiable_in x
let x0 be Real; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A11: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0
then consider N1 being Neighbourhood of x0 such that
A12: N1 c= Z by RCOMP_1:18;
 f is_differentiable_in x0 by A10, A11;
then consider N being Neighbourhood of x0 such that
A13: N c= dom f and
A14: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
consider N2 being Neighbourhood of x0 such that
A15: N2 c= N1 and
A16: N2 c= N by RCOMP_1:17;
A17: N2 c= Z by A12, A15, XBOOLE_1:1;
take  N2 ; :: according to NDIFF_3:def_3 ::_thesis: ( N2 c= dom (f | Z) & ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
 N2 c= dom f by A13, A16, XBOOLE_1:1;
then  N2 c= (dom f) /\ Z by A17, XBOOLE_1:19;
hence A18: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
consider L being LinearFunc of F, R being RestFunc of F such that
A19: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A14;
A20: x0 in N2 by RCOMP_1:16;
take  L ; ::_thesis: ex R being RestFunc of F st
for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
take  R ; ::_thesis: for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
now__::_thesis:_for_x_being_Real_st_x_in_N2_holds_
((f_|_Z)_/._x)_-_((f_|_Z)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Real; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A21: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then  (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A16, A19;
then  ((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A21, A18, PARTFUN2:15;
hence  ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A20, A18, PARTFUN2:15; ::_thesis: verum
end;
hence  for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; ::_thesis: verum
end;

theorem :: NDIFF_3:11
for F being non trivial RealNormSpace
for Y being Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds
Y is open
proof
let F be non trivial RealNormSpace; ::_thesis: for Y being Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds
Y is open
let Y be Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds
Y is open
let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on Y implies Y is open )
assume A1: f is_differentiable_on Y ; ::_thesis: Y is open
now__::_thesis:_for_x0_being_real_number_st_x0_in_Y_holds_
ex_N_being_Neighbourhood_of_x0_st_N_c=_Y
let x0 be real number ; ::_thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y )
assume  x0 in Y ; ::_thesis: ex N being Neighbourhood of x0 st N c= Y
then  f | Y is_differentiable_in x0 by A1, Def5;
then consider N being Neighbourhood of x0 such that
A2: N c= dom (f | Y) and
 ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
((f | Y) /. x) - ((f | Y) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
take N = N; ::_thesis: N c= Y
thus  N c= Y by A2, XBOOLE_1:1; ::_thesis: verum
end;
hence  Y is open by RCOMP_1:20; ::_thesis: verum
end;

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X ->  PartFunc of REAL, the carrier of F means :Def6: :: NDIFF_3:def 6
( dom it = X & ( for x being Real st x in X holds
it . x = diff (f,x) ) );
existence
 ex b1 being PartFunc of REAL, the carrier of F st
( dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff (f,x) ) )
proof
deffunc H1( Real) ->  Point of F = diff (f,$1);
defpred S1[ set ] means $1 in X;
consider F0 being PartFunc of REAL, the carrier of F 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, Th9;
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, the carrier of F 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, the carrier of F; ::_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 Def6 defines `| NDIFF_3:def_6_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for X being set st f is_differentiable_on X holds
for b4 being PartFunc of REAL, the carrier of F holds
( b4 = f `| X iff ( dom b4 = X & ( for x being Real st x in X holds
b4 . x = diff (f,x) ) ) );

theorem :: NDIFF_3:12
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
proof
let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
let f be PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom f & ex r being Point of F st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) ) )
set R = REAL --> (0. F);
A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F
let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) by A1;
A3: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
::_thesis: verum
end;
then  ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18;
hence  ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum
end;
then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
reconsider L = REAL --> (0. F) as Function of REAL,F ;
now__::_thesis:_for_p_being_Real_holds_L_._p_=_p_*_(0._F)
let p be Real; ::_thesis: L . p = p * (0. F)
thus L . p = 0. F by FUNCOP_1:7
.= p * (0. F) by RLVECT_1:10 ; ::_thesis: verum
end;
then reconsider L = L as LinearFunc of F by Def2;
assume A4: Z c= dom f ; ::_thesis: ( for r being Point of F holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) ) )
given r being Point of F such that A5: rng f = {r} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
A6: now__::_thesis:_for_x0_being_Real_st_x0_in_dom_f_holds_
f_/._x0_=_r
let x0 be Real; ::_thesis: ( x0 in dom f implies f /. x0 = r )
assume A7: x0 in dom f ; ::_thesis: f /. x0 = r
then  f /. x0 = f . x0 by PARTFUN1:def_6;
then  f /. x0 in {r} by A5, A7, FUNCT_1:def_3;
hence  f /. x0 = r by TARSKI:def_1; ::_thesis: verum
end;
A8: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A9: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A10: N c= Z by RCOMP_1:18;
A11: N c= dom f by A4, A10, XBOOLE_1:1;
 for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A12: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6
.= 0. F by FUNCOP_1:7 ;
assume  x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A6, A11
.= r - r by A4, A6, A9
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A12, RLVECT_1:4 ;
::_thesis: verum
end;
hence  f is_differentiable_in x0 by A11, Def3; ::_thesis: verum
end;
hence A13: f is_differentiable_on Z by A4, Th10; ::_thesis: for x being Real st x in Z holds
(f `| Z) /. x = 0. F
let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. F )
assume A14: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0. F
then A15: f is_differentiable_in x0 by A8;
then  ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by Def3;
then consider N being Neighbourhood of x0 such that
A16: N c= dom f ;
A17: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A18: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6
.= 0. F by FUNCOP_1:7 ;
assume  x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A6, A16
.= r - r by A4, A6, A14
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A18, RLVECT_1:4 ;
::_thesis: verum
end;
 dom (f `| Z) = Z by A13, Def6;
hence (f `| Z) /. x0 = (f `| Z) . x0 by A14, PARTFUN1:def_6
.= diff (f,x0) by A13, A14, Def6
.= L . 1 by A15, A16, A17, Def4
.= 0. F by FUNCOP_1:7 ;
::_thesis: verum
end;

theorem Th13: :: NDIFF_3:13
for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being real number
for N being Neighbourhood of x0 st 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 ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
proof
let F be non trivial RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of F
for x0 being real number
for N being Neighbourhood of x0 st 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 ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let f be PartFunc of REAL, the carrier of F; ::_thesis: for x0 being real number
for N being Neighbourhood of x0 st 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 ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let x0 be real number ; ::_thesis: for N being Neighbourhood of x0 st 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 ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let N be Neighbourhood of x0; ::_thesis: ( 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 ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
assume that
A1: f is_differentiable_in x0 and
A2: 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 ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
consider N1 being Neighbourhood of x0 such that
 N1 c= dom f and
A3: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3;
consider N2 being Neighbourhood of x0 such that
A4: N2 c= N and
A5: N2 c= N1 by RCOMP_1:17;
A6: N2 c= dom f by A2, A4, XBOOLE_1:1;
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 ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
assume that
A7: rng c = {x0} and
A8: rng (h + c) c= N ; ::_thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
consider g being real number  such that
A9: 0 < g and
A10: N2 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
reconsider z0 = 0 as Nat ;
 ( x0 + z0 < x0 + g & x0 - g < x0 - 0 ) by A9, XREAL_1:8, XREAL_1:15;
then A11: x0 in N2 by A10;
now__::_thesis:_for_y_being_set_st_y_in_rng_c_holds_
y_in_dom_f
let y be set ; ::_thesis: ( y in rng c implies y in dom f )
assume  y in rng c ; ::_thesis: y in dom f
then  y = x0 by A7, TARSKI:def_1;
then  y in N by A4, A11;
hence  y in dom f by A2; ::_thesis: verum
end;
then A12: rng c c= dom f by TARSKI:def_3;
 ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
proof
 x0 in rng c by A7, TARSKI:def_1;
then A13: lim c = x0 by SEQ_4:25;
A14: h + c is convergent by SEQ_2:5;
reconsider z0 = 0 as Real ;
 lim h = z0 ;
then  lim (h + c) = z0 + x0 by A13, SEQ_2:6
.= x0 ;
then consider n being Element of NAT  such that
A15: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - x0) < g by A9, A14, SEQ_2:def_7;
take  n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A16: rng (c ^\ n) = {x0} by A7, VALUED_0:26;
 for y being set st y in rng (c ^\ n) holds
y in N2 by A11, A16, TARSKI:def_1;
hence  rng (c ^\ n) c= N2 by TARSKI:def_3; ::_thesis: rng ((h + c) ^\ n) c= N2
now__::_thesis:_for_y_being_set_st_y_in_rng_((h_+_c)_^\_n)_holds_
y_in_N2
let y be set ; ::_thesis: ( y in rng ((h + c) ^\ n) implies y in N2 )
assume  y in rng ((h + c) ^\ n) ; ::_thesis: y in N2
then consider m being Element of NAT  such that
A17: y = ((h + c) ^\ n) . m by FUNCT_2:113;
reconsider z0 = 0 as Nat ;
 n + z0 <= n + m by XREAL_1:7;
then A18: abs (((h + c) . (n + m)) - x0) < g by A15;
then  ((h + c) . (m + n)) - x0 < g by SEQ_2:1;
then  (((h + c) ^\ n) . m) - x0 < g by NAT_1:def_3;
then A19: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19;
 - g < ((h + c) . (m + n)) - x0 by A18, SEQ_2:1;
then  - g < (((h + c) ^\ n) . m) - x0 by NAT_1:def_3;
then  x0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20;
hence  y in N2 by A10, A17, A19; ::_thesis: verum
end;
hence  rng ((h + c) ^\ n) c= N2 by TARSKI:def_3; ::_thesis: verum
end;
then consider n being Element of NAT  such that
 rng (c ^\ n) c= N2 and
A20: rng ((h + c) ^\ n) c= N2 ;
consider L being LinearFunc of F, R being RestFunc of F such that
A21: for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3;
now__::_thesis:_for_y_being_set_st_y_in_rng_(c_^\_n)_holds_
y_in_dom_f
let y be set ; ::_thesis: ( y in rng (c ^\ n) implies y in dom f )
assume A22: y in rng (c ^\ n) ; ::_thesis: y in dom f
 rng (c ^\ n) = rng c by VALUED_0:26;
then  y = x0 by A7, A22, TARSKI:def_1;
then  y in N by A4, A11;
hence  y in dom f by A2; ::_thesis: verum
end;
then A23: rng (c ^\ n) c= dom f by TARSKI:def_3;
A24: ( ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) is convergent & lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L . 1 )
proof
deffunc H1( Element of NAT ) ->  Element of the carrier of F = (L . 1) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . $1);
consider s1 being sequence of the carrier of F such that
A25: for k being Element of NAT holds s1 . k = H1(k) from FUNCT_2:sch_4();
A26: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_n1_being_Element_of_NAT_st_
for_k_being_Element_of_NAT_st_n1_<=_k_holds_
||.((s1_._k)_-_(L_._1)).||_<_r
A27: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0. F ) by Def1;
let r be Real; ::_thesis: ( 0 < r implies ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
||.((s1 . k) - (L . 1)).|| < r )
assume  0 < r ; ::_thesis: ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
||.((s1 . k) - (L . 1)).|| < r
then consider m being Element of NAT  such that
A28: for k being Element of NAT st m <= k holds
||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - (0. F)).|| < r by A27, NORMSP_1:def_7;
take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds
||.((s1 . k) - (L . 1)).|| < r
let k be Element of NAT ; ::_thesis: ( n1 <= k implies ||.((s1 . k) - (L . 1)).|| < r )
assume A29: n1 <= k ; ::_thesis: ||.((s1 . k) - (L . 1)).|| < r
A30: ||.((s1 . k) - (L . 1)).|| = ||.(((L . 1) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . k)) - (L . 1)).|| by A25
.= ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) + ((L . 1) - (L . 1))).|| by RLVECT_1:28
.= ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) + (0. F)).|| by RLVECT_1:15
.= ||.((((h ^\ n) ") (#) (R /* (h ^\ n))) . k).|| by RLVECT_1:4 ;
 ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - (0. F)).|| < r by A28, A29;
hence  ||.((s1 . k) - (L . 1)).|| < r by A30, RLVECT_1:13; ::_thesis: verum
end;
consider s being Point of F such that
A31: for p1 being Real holds L . p1 = p1 * s by Def2;
A32: L . 1 = 1 * s by A31
.= s by RLVECT_1:def_8 ;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(((h_^\_n)_")_(#)_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n))))_._m_=_s1_._m
let m be Element of NAT ; ::_thesis: (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) . m = s1 . m
A33: (h ^\ n) . m <> 0 by SEQ_1:5;
thus (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) . m = ((((h ^\ n) ") (#) (L /* (h ^\ n))) + (((h ^\ n) ") (#) (R /* (h ^\ n)))) . m by NDIFF_1:9
.= ((((h ^\ n) ") (#) (L /* (h ^\ n))) . m) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by NORMSP_1:def_2
.= ((((h ^\ n) ") . m) * ((L /* (h ^\ n)) . m)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by NDIFF_1:def_2
.= ((((h ^\ n) ") . m) * (L . ((h ^\ n) . m))) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by FUNCT_2:115
.= ((((h ^\ n) ") . m) * (((h ^\ n) . m) * s)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by A31
.= ((((h ^\ n) . m) ") * (((h ^\ n) . m) * s)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by VALUED_1:10
.= (((((h ^\ n) . m) ") * ((h ^\ n) . m)) * s) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by RLVECT_1:def_7
.= (1 * s) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by A33, XCMPLX_0:def_7
.= s + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by RLVECT_1:def_8
.= s1 . m by A25, A32 ; ::_thesis: verum
end;
then A34: ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) = s1 by FUNCT_2:63;
hence  ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) is convergent by A26, NORMSP_1:def_6; ::_thesis: lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L . 1
hence  lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L . 1 by A34, A26, NORMSP_1:def_7; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in_rng_((h_+_c)_^\_n)_holds_
y_in_dom_f
let y be set ; ::_thesis: ( y in rng ((h + c) ^\ n) implies y in dom f )
assume  y in rng ((h + c) ^\ n) ; ::_thesis: y in dom f
then  y in N2 by A20;
then  y in N by A4;
hence  y in dom f by A2; ::_thesis: verum
end;
then A35: rng ((h + c) ^\ n) c= dom f by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_rng_(h_+_c)_holds_
y_in_dom_f
let y be set ; ::_thesis: ( y in rng (h + c) implies y in dom f )
assume  y in rng (h + c) ; ::_thesis: y in dom f
then  y in N by A8;
hence  y in dom f by A2; ::_thesis: verum
end;
then A36: rng (h + c) c= dom f by TARSKI:def_3;
A37: for k being Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
 ((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;
then A38: ((h + c) ^\ n) . k in N2 by A20;
 ( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;
then A39: (c ^\ n) . k = x0 by A7, TARSKI:def_1;
(((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7
.= (h ^\ n) . k ;
hence  (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A21, A5, A38, A39; ::_thesis: verum
end;
A40: R is total by Def1;
now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_/*_((h_+_c)_^\_n))_-_(f_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k
let k be Element of NAT ; ::_thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
 dom R = REAL by A40, FUNCT_2:def_1;
then A41: rng (h ^\ n) c= dom R ;
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by NORMSP_1:def_3
.= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A35, FUNCT_2:109
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A23, FUNCT_2:109
.= (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A37
.= ((L /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A41, FUNCT_2:109
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def_2 ; ::_thesis: verum
end;
then  (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
then A42: ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) = ((h ^\ n) ") (#) (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) by A36, VALUED_0:27
.= ((h ^\ n) ") (#) (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) by A12, VALUED_0:27
.= ((h ^\ n) ") (#) (((f /* (h + c)) - (f /* c)) ^\ n) by NDIFF_1:16
.= ((h ") ^\ n) (#) (((f /* (h + c)) - (f /* c)) ^\ n) by SEQM_3:18
.= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n by Th2 ;
then A43: L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A24, LOPBAN_3:11;
thus  (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A24, A42, LOPBAN_3:10; ::_thesis: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
 for x being Real st x in N2 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A21, A5;
hence  diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A1, A6, A43, Def4; ::_thesis: verum
end;

theorem Th14: :: NDIFF_3:14
for F being non trivial RealNormSpace
for x0 being Real
for f1, f2 being PartFunc of REAL, the carrier of F 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 F be non trivial RealNormSpace; ::_thesis: for x0 being Real
for f1, f2 being PartFunc of REAL, the carrier of F 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 x0 be Real; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of F 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, the carrier of F; ::_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 that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3;
consider L1 being LinearFunc of F, R1 being RestFunc of F such that
A5: for x being Real st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def3;
consider L2 being LinearFunc of F, R2 being RestFunc of F such that
A8: for x being Real st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 + R2 as RestFunc of F by Th7;
reconsider L = L1 + L2 as LinearFunc of F by Th3;
A9: ( dom L1 = REAL & dom L2 = REAL ) by FUNCT_2:def_1;
consider N being Neighbourhood of x0 such that
A10: N c= N1 and
A11: N c= N2 by RCOMP_1:17;
A12: N c= dom f2 by A6, A11, XBOOLE_1:1;
 N c= dom f1 by A3, A10, XBOOLE_1:1;
then  N /\ N c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:27;
then A13: N c= dom (f1 + f2) by VFUNCT_1:def_1;
 ( R1 is total & R2 is total ) by Def1;
then  R1 + R2 is total by VFUNCT_1:32;
then A14: dom (R1 + R2) = REAL by FUNCT_2:def_1;
 L1 + L2 is total by VFUNCT_1:32;
then A15: dom (L1 + L2) = REAL by FUNCT_2:def_1;
A16: now__::_thesis:_for_x_being_Real_st_x_in_N_holds_
((f1_+_f2)_/._x)_-_((f1_+_f2)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Real; ::_thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A17: x0 in N by RCOMP_1:16;
assume A18: x in N ; ::_thesis: ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0) by A13, VFUNCT_1:def_1
.= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A13, A17, VFUNCT_1:def_1
.= (f1 /. x) + ((f2 /. x) - ((f1 /. x0) + (f2 /. x0))) by RLVECT_1:28
.= (f1 /. x) + (((f2 /. x) - (f2 /. x0)) - (f1 /. x0)) by RLVECT_1:27
.= ((f1 /. x) + ((f2 /. x) - (f2 /. x0))) - (f1 /. x0) by RLVECT_1:28
.= ((f2 /. x) - (f2 /. x0)) + ((f1 /. x) - (f1 /. x0)) by RLVECT_1:28
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A10, A18
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A11, A18
.= (((L1 . (x - x0)) + (R1 /. (x - x0))) + (L2 . (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3
.= (((L1 . (x - x0)) + (L2 . (x - x0))) + (R1 /. (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3
.= ((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by RLVECT_1:def_3
.= (L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by A15, VFUNCT_1:def_1
.= (L . (x - x0)) + (R /. (x - x0)) by A14, VFUNCT_1:def_1 ;
::_thesis: verum
end;
hence  f1 + f2 is_differentiable_in x0 by A13, Def3; ::_thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0))
hence  diff ((f1 + f2),x0) = L . 1 by A13, A16, Def4
.= L /. 1 by A15, PARTFUN1:def_6
.= (L1 /. 1) + (L2 /. 1) by A15, VFUNCT_1:def_1
.= (L1 . 1) + (L2 /. 1) by A9, PARTFUN1:def_6
.= (L1 . 1) + (L2 . 1) by A9, PARTFUN1:def_6
.= (diff (f1,x0)) + (L2 . 1) by A1, A3, A5, Def4
.= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def4 ;
::_thesis: verum
end;

theorem Th15: :: NDIFF_3:15
for F being non trivial RealNormSpace
for x0 being Real
for f1, f2 being PartFunc of REAL, the carrier of F 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 F be non trivial RealNormSpace; ::_thesis: for x0 being Real
for f1, f2 being PartFunc of REAL, the carrier of F 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 x0 be Real; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of F 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, the carrier of F; ::_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 that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3;
consider L1 being LinearFunc of F, R1 being RestFunc of F such that
A5: for x being Real st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def3;
consider L2 being LinearFunc of F, R2 being RestFunc of F such that
A8: for x being Real st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 - R2 as RestFunc of F by Th7;
reconsider L = L1 - L2 as LinearFunc of F by Th3;
A9: ( dom L1 = REAL & dom L2 = REAL ) by FUNCT_2:def_1;
consider N being Neighbourhood of x0 such that
A10: N c= N1 and
A11: N c= N2 by RCOMP_1:17;
A12: N c= dom f2 by A6, A11, XBOOLE_1:1;
 N c= dom f1 by A3, A10, XBOOLE_1:1;
then  N /\ N c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:27;
then A13: N c= dom (f1 - f2) by VFUNCT_1:def_2;
 ( R1 is total & R2 is total ) by Def1;
then  R1 - R2 is total by VFUNCT_1:32;
then A14: dom (R1 - R2) = REAL by FUNCT_2:def_1;
 L1 - L2 is total by VFUNCT_1:32;
then A15: dom (L1 - L2) = REAL by FUNCT_2:def_1;
A16: now__::_thesis:_for_x_being_Real_st_x_in_N_holds_
((f1_-_f2)_/._x)_-_((f1_-_f2)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Real; ::_thesis: ( x in N implies ((f1 - f2) /. x) - ((f1 - f2) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A17: x0 in N by RCOMP_1:16;
assume A18: x in N ; ::_thesis: ((f1 - f2) /. x) - ((f1 - f2) /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0) by A13, VFUNCT_1:def_2
.= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A13, A17, VFUNCT_1:def_2
.= (f1 /. x) - ((f2 /. x) + ((f1 /. x0) - (f2 /. x0))) by RLVECT_1:27
.= (f1 /. x) - (((f2 /. x) + (f1 /. x0)) - (f2 /. x0)) by RLVECT_1:28
.= (f1 /. x) - ((f1 /. x0) + ((f2 /. x) - (f2 /. x0))) by RLVECT_1:28
.= ((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0)) by RLVECT_1:27
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0)) by A5, A10, A18
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A11, A18
.= (L1 . (x - x0)) + ((R1 /. (x - x0)) - ((L2 . (x - x0)) + (R2 /. (x - x0)))) by RLVECT_1:28
.= (L1 . (x - x0)) + (((R1 /. (x - x0)) - (R2 /. (x - x0))) - (L2 . (x - x0))) by RLVECT_1:27
.= ((L1 . (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) - (L2 . (x - x0)) by RLVECT_1:28
.= ((L1 /. (x - x0)) - (L2 /. (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by RLVECT_1:28
.= (L /. (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by A15, VFUNCT_1:def_2
.= (L . (x - x0)) + (R /. (x - x0)) by A14, VFUNCT_1:def_2 ;
::_thesis: verum
end;
hence  f1 - f2 is_differentiable_in x0 by A13, Def3; ::_thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))
hence  diff ((f1 - f2),x0) = L . 1 by A13, A16, Def4
.= L /. 1 by A15, PARTFUN1:def_6
.= (L1 /. 1) - (L2 /. 1) by A15, VFUNCT_1:def_2
.= (L1 . 1) - (L2 /. 1) by A9, PARTFUN1:def_6
.= (L1 . 1) - (L2 . 1) by A9, PARTFUN1:def_6
.= (diff (f1,x0)) - (L2 . 1) by A1, A3, A5, Def4
.= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def4 ;
::_thesis: verum
end;

theorem Th16: :: NDIFF_3:16
for F being non trivial RealNormSpace
for x0 being Real
for f being PartFunc of REAL, the carrier of F
for r being Real st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
proof
let F be non trivial RealNormSpace; ::_thesis: for x0 being Real
for f being PartFunc of REAL, the carrier of F
for r being Real st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let x0 be Real; ::_thesis: for f being PartFunc of REAL, the carrier of F
for r being Real 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, the carrier of F; ::_thesis: for r being Real st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let r be Real; ::_thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) )
assume A1: f is_differentiable_in x0 ; ::_thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
then consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
consider L1 being LinearFunc of F, R1 being RestFunc of F such that
A4: for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A3;
reconsider R = r (#) R1 as RestFunc of F by Th8;
reconsider L = r (#) L1 as LinearFunc of F by Th4;
A5: dom L1 = REAL by FUNCT_2:def_1;
A6: N1 c= dom (r (#) f) by A2, VFUNCT_1:def_4;
 R1 is total by Def1;
then  r (#) R1 is total by VFUNCT_1:34;
then A7: dom (r (#) R1) = REAL by FUNCT_2:def_1;
 r (#) L1 is total by VFUNCT_1:34;
then A8: dom (r (#) L1) = REAL by FUNCT_2:def_1;
A9: now__::_thesis:_for_x_being_Real_st_x_in_N1_holds_
((r_(#)_f)_/._x)_-_((r_(#)_f)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Real; ::_thesis: ( x in N1 implies ((r (#) f) /. x) - ((r (#) f) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A10: x0 in N1 by RCOMP_1:16;
assume A11: x in N1 ; ::_thesis: ((r (#) f) /. x) - ((r (#) f) /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence ((r (#) f) /. x) - ((r (#) f) /. x0) = (r * (f /. x)) - ((r (#) f) /. x0) by A6, VFUNCT_1:def_4
.= (r * (f /. x)) - (r * (f /. x0)) by A6, A10, VFUNCT_1:def_4
.= r * ((f /. x) - (f /. x0)) by RLVECT_1:34
.= r * ((L1 . (x - x0)) + (R1 /. (x - x0))) by A4, A11
.= (r * (L1 /. (x - x0))) + (r * (R1 /. (x - x0))) by RLVECT_1:def_5
.= (L /. (x - x0)) + (r * (R1 /. (x - x0))) by A8, VFUNCT_1:def_4
.= (L . (x - x0)) + (R /. (x - x0)) by A7, VFUNCT_1:def_4 ;
::_thesis: verum
end;
hence  r (#) f is_differentiable_in x0 by A6, Def3; ::_thesis: diff ((r (#) f),x0) = r * (diff (f,x0))
hence  diff ((r (#) f),x0) = L . 1 by A6, A9, Def4
.= L /. 1 by A8, PARTFUN1:def_6
.= r * (L1 /. 1) by A8, VFUNCT_1:def_4
.= r * (L1 . 1) by A5, PARTFUN1:def_6
.= r * (diff (f,x0)) by A1, A2, A4, Def4 ;
::_thesis: verum
end;

theorem :: NDIFF_3:17
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F 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 F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F 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, the carrier of F 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, the carrier of F; ::_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)) ) )
now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
f1_+_f2_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies f1 + f2 is_differentiable_in x0 )
assume  x0 in Z ; ::_thesis: f1 + f2 is_differentiable_in x0
then  ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th10;
hence  f1 + f2 is_differentiable_in x0 by Th14; ::_thesis: verum
end;
hence A3: f1 + f2 is_differentiable_on Z by A1, Th10; ::_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 A4: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th10;
thus ((f1 + f2) `| Z) . x = diff ((f1 + f2),x) by A3, A4, Def6
.= (diff (f1,x)) + (diff (f2,x)) by A5, Th14 ; ::_thesis: verum
end;

theorem :: NDIFF_3:18
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F 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 F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F 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, the carrier of F 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, the carrier of F; ::_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)) ) )
now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
f1_-_f2_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies f1 - f2 is_differentiable_in x0 )
assume  x0 in Z ; ::_thesis: f1 - f2 is_differentiable_in x0
then  ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th10;
hence  f1 - f2 is_differentiable_in x0 by Th15; ::_thesis: verum
end;
hence A3: f1 - f2 is_differentiable_on Z by A1, Th10; ::_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 A4: x in Z ; ::_thesis: ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x))
then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th10;
thus ((f1 - f2) `| Z) . x = diff ((f1 - f2),x) by A3, A4, Def6
.= (diff (f1,x)) - (diff (f2,x)) by A5, Th15 ; ::_thesis: verum
end;

theorem :: NDIFF_3:19
for F being non trivial RealNormSpace
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) 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 F be non trivial RealNormSpace; ::_thesis: for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) 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 r be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) 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, the carrier of F st Z c= dom (r (#) 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, the carrier of F; ::_thesis: ( Z c= dom (r (#) 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 (r (#) 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)) ) )
now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
r_(#)_f_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies r (#) f is_differentiable_in x0 )
assume  x0 in Z ; ::_thesis: r (#) f is_differentiable_in x0
then  f is_differentiable_in x0 by A2, Th10;
hence  r (#) f is_differentiable_in x0 by Th16; ::_thesis: verum
end;
hence A3: r (#) f is_differentiable_on Z by A1, Th10; ::_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 A4: x in Z ; ::_thesis: ((r (#) f) `| Z) . x = r * (diff (f,x))
then A5: f is_differentiable_in x by A2, Th10;
thus ((r (#) f) `| Z) . x = diff ((r (#) f),x) by A3, A4, Def6
.= r * (diff (f,x)) by A5, Th16 ; ::_thesis: verum
end;

theorem :: NDIFF_3:20
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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. F ) )
proof
let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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. F ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F 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. F ) )
let f be PartFunc of REAL, the carrier of F; ::_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. F ) ) )
set R = REAL --> (0. F);
A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F
let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) by A1;
A3: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
::_thesis: verum
end;
then  ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18;
hence  ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum
end;
then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
set L = REAL --> (0. F);
now__::_thesis:_for_p_being_Real_holds_(REAL_-->_(0._F))_._p_=_p_*_(0._F)
let p be Real; ::_thesis: (REAL --> (0. F)) . p = p * (0. F)
thus (REAL --> (0. F)) . p = 0. F by FUNCOP_1:7
.= p * (0. F) by RLVECT_1:10 ; ::_thesis: verum
end;
then reconsider L = REAL --> (0. F) as LinearFunc of F by Def2;
assume that
A4: Z c= dom f and
A5: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0. F ) )
consider r being Point of F such that
A6: for x being Real st x in Z /\ (dom f) holds
f . x = r by A5, PARTFUN2:57;
A7: now__::_thesis:_for_x_being_Real_st_x_in_Z_/\_(dom_f)_holds_
f_/._x_=_r
let x be Real; ::_thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A8: x in Z /\ (dom f) ; ::_thesis: f /. x = r
then  x in dom f by XBOOLE_0:def_4;
hence f /. x = f . x by PARTFUN1:def_6
.= r by A8, A6 ;
::_thesis: verum
end;
A9: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A10: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A11: N c= Z by RCOMP_1:18;
A12: N c= dom f by A4, A11, XBOOLE_1:1;
A13: x0 in Z /\ (dom f) by A4, A10, XBOOLE_0:def_4;
 for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A14: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6
.= 0. F by FUNCOP_1:7 ;
assume  x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then  x in Z /\ (dom f) by A11, A12, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A7
.= r - r by A7, A13
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A14, RLVECT_1:4 ;
::_thesis: verum
end;
hence  f is_differentiable_in x0 by A12, Def3; ::_thesis: verum
end;
hence A15: f is_differentiable_on Z by A4, Th10; ::_thesis: for x being Real st x in Z holds
(f `| Z) . x = 0. F
let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) . x0 = 0. F )
assume A16: x0 in Z ; ::_thesis: (f `| Z) . x0 = 0. F
then consider N being Neighbourhood of x0 such that
A17: N c= Z by RCOMP_1:18;
A18: N c= dom f by A4, A17, XBOOLE_1:1;
A19: x0 in Z /\ (dom f) by A4, A16, XBOOLE_0:def_4;
A20: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A21: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6
.= 0. F by FUNCOP_1:7 ;
assume  x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then  x in Z /\ (dom f) by A17, A18, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A7
.= r - r by A7, A19
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A21, RLVECT_1:4 ;
::_thesis: verum
end;
A22: f is_differentiable_in x0 by A9, A16;
thus (f `| Z) . x0 = diff (f,x0) by A15, A16, Def6
.= L . 1 by A22, A18, A20, Def4
.= 0. F by FUNCOP_1:7 ; ::_thesis: verum
end;

theorem Th21: :: NDIFF_3:21
for F being non trivial RealNormSpace
for r, p being Point of F
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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 F be non trivial RealNormSpace; ::_thesis: for r, p being Point of F
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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 Point of F; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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, the carrier of F 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, the carrier of F; ::_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 ) ) )
set R = REAL --> (0. F);
defpred S1[ set ] means $1 in REAL ;
A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F
let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) by A1;
A3: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
::_thesis: verum
end;
then  ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18;
hence  ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum
end;
then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
assume that
A4: Z c= dom f and
A5: 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 ) )
deffunc H1( Real) ->  Element of the carrier of F = $1 * r;
consider L being PartFunc of REAL, the carrier of F such that
A6: ( ( for x being Real holds
( x in dom L iff S1[x] ) ) & ( for x being Real st x in dom L holds
L . x = H1(x) ) ) from SEQ_1:sch_3();
 dom L = REAL by A6, FDIFF_1:1;
then A7: L is total by PARTFUN1:def_2;
A8: now__::_thesis:_for_x_being_Real_holds_L_._x_=_x_*_r
let x be Real; ::_thesis: L . x = x * r
thus  L . x = x * r by A6; ::_thesis: verum
end;
then reconsider L = L as LinearFunc of F by A7, Def2;
A9: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A10: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A11: N c= Z by RCOMP_1:18;
A12: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A13: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6
.= 0. F by FUNCOP_1:7 ;
assume  x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((x * r) + p) - (f /. x0) by A5, A11
.= ((x * r) + p) - ((x0 * r) + p) by A5, A10
.= (((x * r) + p) - (x0 * r)) - p by RLVECT_1:27
.= (p + ((x * r) - (x0 * r))) - p by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (p - p) by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (0. F) by RLVECT_1:15
.= ((x - x0) * r) + (0. F) by RLVECT_1:35
.= (L . (x - x0)) + (R /. (x - x0)) by A13, A8 ;
::_thesis: verum
end;
 N c= dom f by A4, A11, XBOOLE_1:1;
hence  f is_differentiable_in x0 by A12, Def3; ::_thesis: verum
end;
hence A14: f is_differentiable_on Z by A4, Th10; ::_thesis: for x being Real st x in Z holds
(f `| Z) . x = r
let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) . x0 = r )
assume A15: x0 in Z ; ::_thesis: (f `| Z) . x0 = r
then consider N being Neighbourhood of x0 such that
A16: N c= Z by RCOMP_1:18;
A17: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A18: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6
.= 0. F by FUNCOP_1:7 ;
assume  x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((x * r) + p) - (f /. x0) by A5, A16
.= ((x * r) + p) - ((x0 * r) + p) by A5, A15
.= (((x * r) + p) - (x0 * r)) - p by RLVECT_1:27
.= (p + ((x * r) - (x0 * r))) - p by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (p - p) by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (0. F) by RLVECT_1:15
.= ((x - x0) * r) + (0. F) by RLVECT_1:35
.= (L . (x - x0)) + (R /. (x - x0)) by A18, A8 ;
::_thesis: verum
end;
A19: N c= dom f by A4, A16, XBOOLE_1:1;
A20: f is_differentiable_in x0 by A9, A15;
thus (f `| Z) . x0 = diff (f,x0) by A14, A15, Def6
.= L . 1 by A20, A19, A17, Def4
.= 1 * r by A8
.= r by RLVECT_1:def_8 ; ::_thesis: verum
end;

theorem Th22: :: NDIFF_3:22
for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
proof
let F be non trivial RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of F
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let f be PartFunc of REAL, the carrier of F; ::_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 A1: f is_differentiable_in x0 ; ::_thesis: f is_continuous_in x0
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
 ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
A3: x0 in N by RCOMP_1:16;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_=_x0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_x0_)_holds_
(_f_/*_s1_is_convergent_&_f_/._x0_=_lim_(f_/*_s1)_)
consider g being real number  such that
A4: 0 < g and
A5: N = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
reconsider s2 = NAT --> x0 as Real_Sequence ;
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Element of NAT holds s1 . n <> x0 ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
consider l being Element of NAT  such that
A10: for m being Element of NAT st l <= m holds
abs ((s1 . m) - x0) < g by A7, A8, A4, SEQ_2:def_7;
reconsider c = s2 ^\ l as constant Real_Sequence ;
deffunc H1( Real) ->  Element of REAL = (s1 . $1) - (s2 . $1);
consider s3 being Real_Sequence such that
A11: for n being Element of NAT holds s3 . n = H1(n) from SEQ_1:sch_1();
A12: s3 = s1 - s2 by A11, RFUNCT_2:1;
then A13: s3 is convergent by A7, SEQ_2:11;
A14: rng c = {x0}
proof
thus  rng c c= {x0} :: according to XBOOLE_0:def_10 ::_thesis: {x0} c= rng c
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in {x0} )
assume  y in rng c ; ::_thesis: y in {x0}
then consider n being Element of NAT  such that
A15: y = (s2 ^\ l) . n by FUNCT_2:113;
 y = s2 . (n + l) by A15, NAT_1:def_3;
then  y = x0 by FUNCOP_1:7;
hence  y in {x0} by TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x0} or y in rng c )
assume  y in {x0} ; ::_thesis: y in rng c
then A16: y = x0 by TARSKI:def_1;
reconsider z0 = 0 as Element of NAT ;
c . z0 = s2 . (z0 + l) by NAT_1:def_3
.= y by A16, FUNCOP_1:7 ;
hence  y in rng c by VALUED_0:28; ::_thesis: verum
end;
A17: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((f_/*_c)_._m)_-_(f_/._x0)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p )
assume A18: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p )
assume  n <= m ; ::_thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p
 x0 in N by RCOMP_1:16;
then  rng c c= dom f by A2, A14, ZFMISC_1:31;
then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109
.= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def_3
.= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1:7
.= ||.(0. F).|| by RLVECT_1:15
.= 0 ;
hence  ||.(((f /* c) . m) - (f /. x0)).|| < p by A18; ::_thesis: verum
end;
then A19: f /* c is convergent by NORMSP_1:def_6;
lim s2 = s2 . 0 by SEQ_4:26
.= x0 by FUNCOP_1:7 ;
then  lim s3 = x0 - x0 by A7, A8, A12, SEQ_2:12
.= 0 ;
then A20: lim (s3 ^\ l) = 0 by A13, SEQ_4:20;
A21: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s3_._n_=_0
given n being Element of NAT  such that A22: s3 . n = 0 ; ::_thesis: contradiction
 (s1 . n) - (s2 . n) = 0 by A11, A22;
hence  contradiction by A9, FUNCOP_1:7; ::_thesis: verum
end;
A23: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(s3_^\_l)_._n_=_0
given n being Element of NAT  such that A24: (s3 ^\ l) . n = 0 ; ::_thesis: contradiction
 s3 . (n + l) = 0 by A24, NAT_1:def_3;
hence  contradiction by A21; ::_thesis: verum
end;
then  s3 ^\ l is non-zero by SEQ_1:5;
then reconsider h = s3 ^\ l as non-zero 0 -convergent Real_Sequence by A13, A20, FDIFF_1:def_1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_/*_(h_+_c))_-_(f_/*_c))_+_(f_/*_c))_._n_=_(f_/*_(h_+_c))_._n
let n be Element of NAT ; ::_thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n
thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by NORMSP_1:def_2
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by NORMSP_1:def_3
.= ((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n)) by RLVECT_1:29
.= ((f /* (h + c)) . n) - (0. F) by RLVECT_1:15
.= (f /* (h + c)) . n by RLVECT_1:13 ; ::_thesis: verum
end;
then A25: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_+_c)_._n_=_(s1_^\_l)_._n
let n be Element of NAT ; ::_thesis: (h + c) . n = (s1 ^\ l) . n
thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A12, SEQM_3:15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by SEQ_1:7
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by RFUNCT_2:1
.= (s1 ^\ l) . n by NAT_1:def_3 ; ::_thesis: verum
end;
then A26: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A25, FUNCT_2:63
.= (f /* s1) ^\ l by A6, VALUED_0:27 ;
now__::_thesis:_for_y_being_set_st_y_in_rng_(h_+_c)_holds_
y_in_N
let y be set ; ::_thesis: ( y in rng (h + c) implies y in N )
assume  y in rng (h + c) ; ::_thesis: y in N
then consider n being Element of NAT  such that
A27: y = (h + c) . n by FUNCT_2:113;
(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A12, SEQM_3:15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by SEQ_1:7
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by RFUNCT_2:1
.= s1 . (l + n) ;
then  abs (((h + c) . n) - x0) < g by A10, NAT_1:12;
hence  y in N by A5, A27, RCOMP_1:1; ::_thesis: verum
end;
then A28: rng (h + c) c= N by TARSKI:def_3;
A29: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A20, A1, A2, A14, Th13, A28, NDIFF_1:14
.= 0. F by RLVECT_1:10 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_(#)_((h_")_(#)_((f_/*_(h_+_c))_-_(f_/*_c))))_._n_=_((f_/*_(h_+_c))_-_(f_/*_c))_._n
let n be Element of NAT ; ::_thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A30: h . n <> 0 by A23;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by NDIFF_1:def_2
.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by NDIFF_1:def_2
.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10
.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n) by RLVECT_1:def_7
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A30, XCMPLX_0:def_7
.= ((f /* (h + c)) - (f /* c)) . n by RLVECT_1:def_8 ; ::_thesis: verum
end;
then A31: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63;
then A32: (f /* (h + c)) - (f /* c) is convergent by A28, A1, A2, A14, Th13, NDIFF_1:13;
then  ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A19, NORMSP_1:19;
hence  f /* s1 is convergent by A26, LOPBAN_3:10; ::_thesis: f /. x0 = lim (f /* s1)
 lim (f /* c) = f /. x0 by A17, A19, NORMSP_1:def_7;
then  lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. F) + (f /. x0) by A29, A31, A32, A19, NORMSP_1:25
.= f /. x0 by RLVECT_1:4 ;
hence  f /. x0 = lim (f /* s1) by A32, A26, A19, LOPBAN_3:11, NORMSP_1:19; ::_thesis: verum
end;
hence  f is_continuous_in x0 by A3, A2, NFCONT_3:7; ::_thesis: verum
end;

theorem :: NDIFF_3:23
for F being non trivial RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
f | X is continuous
proof
let F be non trivial RealNormSpace; ::_thesis: for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
f | X is continuous
let X be set ; ::_thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
f | X is continuous
let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on X implies f | X is continuous )
assume A1: f is_differentiable_on X ; ::_thesis: f | X is continuous
now__::_thesis:_for_x_being_real_number_st_x_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x
let x be real number ; ::_thesis: ( x in dom (f | X) implies f | X is_continuous_in x )
assume  x in dom (f | X) ; ::_thesis: f | X is_continuous_in x
then  ( x is Real & x in X ) by XREAL_0:def_1;
then A2: f | X is_differentiable_in x by A1, Def5;
 x is Real by XREAL_0:def_1;
hence  f | X is_continuous_in x by A2, Th22; ::_thesis: verum
end;
hence  f | X is continuous by NFCONT_3:def_2; ::_thesis: verum
end;

theorem Th24: :: NDIFF_3:24
for F being non trivial RealNormSpace
for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
proof
let F be non trivial RealNormSpace; ::_thesis: for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let X be set ; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )
assume that
A1: f is_differentiable_on X and
A2: Z c= X ; ::_thesis: f is_differentiable_on Z
 X c= dom f by A1, Def5;
then A3: Z c= dom f by A2, XBOOLE_1:1;
now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
f_|_Z_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A4: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0
then  f | X is_differentiable_in x0 by A1, A2, Def5;
then consider N being Neighbourhood of x0 such that
A5: N c= dom (f | X) and
A6: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
consider N1 being Neighbourhood of x0 such that
A7: N1 c= Z by A4, RCOMP_1:18;
consider N2 being Neighbourhood of x0 such that
A8: N2 c= N and
A9: N2 c= N1 by RCOMP_1:17;
A10: N2 c= Z by A7, A9, XBOOLE_1:1;
 dom (f | X) = (dom f) /\ X by RELAT_1:61;
then  dom (f | X) c= dom f by XBOOLE_1:17;
then  N c= dom f by A5, XBOOLE_1:1;
then  N2 c= dom f by A8, XBOOLE_1:1;
then  N2 c= (dom f) /\ Z by A10, XBOOLE_1:19;
then A11: N2 c= dom (f | Z) by RELAT_1:61;
A12: N2 c= dom (f | X) by A8, A5, XBOOLE_1:1;
consider L being LinearFunc of F, R being RestFunc of F such that
A13: for x being Real st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6;
 for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A14: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then A15: ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8, A13;
A16: x0 in N2 by RCOMP_1:16;
 ((f | X) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A15, A16, A12, PARTFUN2:15;
then  (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A14, A12, PARTFUN2:15;
then  (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A16, A11, PARTFUN2:15;
hence  ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A14, A11, PARTFUN2:15; ::_thesis: verum
end;
hence  f | Z is_differentiable_in x0 by Def3, A11; ::_thesis: verum
end;
hence  f is_differentiable_on Z by Def5, A3; ::_thesis: verum
end;

Lm1:  {} REAL is closed
proof
let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= {} REAL or not a is convergent or lim a in {} REAL )
assume  ( rng a c= {} REAL & a is convergent ) ; ::_thesis: lim a in {} REAL
hence  lim a in {} REAL ; ::_thesis: verum
end;

theorem :: NDIFF_3:25
for F being non trivial RealNormSpace ex R being RestFunc of F st
( R /. 0 = 0. F & R is_continuous_in 0 )
proof
let F be non trivial RealNormSpace; ::_thesis: ex R being RestFunc of F st
( R /. 0 = 0. F & R is_continuous_in 0 )
 ( ([#] REAL) ` = {} REAL & REAL c= REAL & [#] REAL = REAL ) by XBOOLE_1:37;
then reconsider Z = [#] REAL as open Subset of REAL by Lm1, RCOMP_1:def_5;
set R = REAL --> (0. F);
reconsider f = REAL --> (0. F) as PartFunc of REAL, the carrier of F ;
A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F
let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) by A1;
A3: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
::_thesis: verum
end;
then  ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18;
hence  ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum
end;
then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
set L = REAL --> (0. F);
now__::_thesis:_for_p_being_Real_holds_(REAL_-->_(0._F))_._p_=_p_*_(0._F)
let p be Real; ::_thesis: (REAL --> (0. F)) . p = p * (0. F)
thus (REAL --> (0. F)) . p = 0. F by FUNCOP_1:7
.= p * (0. F) by RLVECT_1:10 ; ::_thesis: verum
end;
then reconsider L = REAL --> (0. F) as LinearFunc of F by Def2;
A4: Z c= dom f by FUNCOP_1:13;
A5: f | Z is constant ;
consider r being Point of F such that
A6: for x being Real st x in Z /\ (dom f) holds
f . x = r by A5, PARTFUN2:57;
A7: now__::_thesis:_for_x_being_Real_st_x_in_Z_/\_(dom_f)_holds_
f_/._x_=_r
let x be Real; ::_thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A8: x in Z /\ (dom f) ; ::_thesis: f /. x = r
then  x in dom f by XBOOLE_0:def_4;
hence f /. x = f . x by PARTFUN1:def_6
.= r by A8, A6 ;
::_thesis: verum
end;
A9: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume  x0 in Z ; ::_thesis: f is_differentiable_in x0
set N = the Neighbourhood of x0;
A10: the Neighbourhood of x0 c= dom f by A4, XBOOLE_1:1;
 for x being Real st x in the Neighbourhood of x0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in the Neighbourhood of x0 implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A11: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6
.= 0. F by FUNCOP_1:7 ;
assume  x in the Neighbourhood of x0 ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then  x in Z /\ (dom f) by A10, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A7
.= r - r by A7, A1
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A11, RLVECT_1:4 ;
::_thesis: verum
end;
hence  f is_differentiable_in x0 by A10, Def3; ::_thesis: verum
end;
set x0 = the Real;
 f is_differentiable_in the Real by A9;
then consider N being Neighbourhood of the Real such that
 N c= dom f and
A12: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. the Real) = (L . (x - the Real)) + (R /. (x - the Real)) by Def3;
consider L being LinearFunc of F, R being RestFunc of F such that
A13: for x being Real st x in N holds
(f /. x) - (f /. the Real) = (L . (x - the Real)) + (R /. (x - the Real)) by A12;
take  R ; ::_thesis: ( R /. 0 = 0. F & R is_continuous_in 0 )
consider p being Point of F such that
A14: for r being Real holds L . r = r * p by Def2;
 (f /. the Real) - (f /. the Real) = (L . ( the Real - the Real)) + (R /. ( the Real - the Real)) by A13, RCOMP_1:16;
then  0. F = (L . ( the Real - the Real)) + (R /. ( the Real - the Real)) by RLVECT_1:15;
then  0. F = (0 * p) + (R /. 0) by A14;
then  0. F = (0. F) + (R /. 0) by RLVECT_1:10;
hence A15: R /. 0 = 0. F by RLVECT_1:4; ::_thesis: R is_continuous_in 0
A16: now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_R_/*_h_is_convergent_&_lim_(R_/*_h)_=_R_/._0_)
set s3 = cs;
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( R /* h is convergent & lim (R /* h) = R /. 0 )
A17: cs . 1 = 0 by FUNCOP_1:7;
 ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. F ) by Def1;
then  ||.((h ") (#) (R /* h)).|| is bounded by LOPBAN_1:20, SEQ_2:13;
then consider M being real number  such that
 M > 0 and
A18: for n being Element of NAT holds abs (||.((h ") (#) (R /* h)).|| . n) < M by SEQ_2:3;
A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(((h_")_(#)_(R_/*_h))_._n).||_<_M
let n be Element of NAT ; ::_thesis: ||.(((h ") (#) (R /* h)) . n).|| < M
 abs (||.((h ") (#) (R /* h)).|| . n) < M by A18;
then  abs ||.(((h ") (#) (R /* h)) . n).|| < M by NORMSP_0:def_4;
hence  ||.(((h ") (#) (R /* h)) . n).|| < M by ABSVALUE:def_1; ::_thesis: verum
end;
reconsider z0 = 0 as Real ;
A20: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((R_/*_h)_._n).||_<=_(M_(#)_(abs_h))_._n
let n be Element of NAT ; ::_thesis: ||.((R /* h) . n).|| <= (M (#) (abs h)) . n
||.(((h ") (#) (R /* h)) . n).|| = ||.(((h ") . n) * ((R /* h) . n)).|| by NDIFF_1:def_2
.= ||.(((h . n) ") * ((R /* h) . n)).|| by VALUED_1:10 ;
then A21: ||.(((h . n) ") * ((R /* h) . n)).|| <= M by A19;
 abs (h . n) >= 0 by COMPLEX1:46;
then  (abs (h . n)) * ||.(((h . n) ") * ((R /* h) . n)).|| <= M * (abs (h . n)) by A21, XREAL_1:64;
then  ||.((h . n) * (((h . n) ") * ((R /* h) . n))).|| <= M * (abs (h . n)) by NORMSP_1:def_1;
then A22: ||.(((h . n) * ((h . n) ")) * ((R /* h) . n)).|| <= M * (abs (h . n)) by RLVECT_1:def_7;
 h . n <> 0 by SEQ_1:5;
then  ||.(1 * ((R /* h) . n)).|| <= M * (abs (h . n)) by A22, XCMPLX_0:def_7;
then  ||.((R /* h) . n).|| <= M * (abs (h . n)) by RLVECT_1:def_8;
then  ||.((R /* h) . n).|| <= M * ((abs h) . n) by SEQ_1:12;
hence  ||.((R /* h) . n).|| <= (M (#) (abs h)) . n by SEQ_1:9; ::_thesis: verum
end;
 lim h = z0 ;
then  lim (abs h) = abs z0 by SEQ_4:14
.= z0 by ABSVALUE:2 ;
then A23: lim (M (#) (abs h)) = M * z0 by SEQ_2:8
.= lim cs by A17, SEQ_4:25 ;
A24: M (#) (abs h) is convergent by SEQ_2:7;
reconsider z0 = 0 as Real ;
 lim (M (#) (abs h)) = 0 by A23, A17, SEQ_4:25;
hence  ( R /* h is convergent & lim (R /* h) = R /. 0 ) by A15, A24, A20, Th1; ::_thesis: verum
end;
 R is total by Def1;
then A25: dom R = REAL by FUNCT_2:def_1;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_R_&_s1_is_convergent_&_lim_s1_=_0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_0_)_holds_
(_R_/*_s1_is_convergent_&_R_/._0_=_lim_(R_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Element of NAT holds s1 . n <> 0 ) implies ( R /* s1 is convergent & R /. 0 = lim (R /* s1) ) )
assume that
 rng s1 c= dom R and
A26: ( s1 is convergent & lim s1 = 0 ) and
A27: for n being Element of NAT holds s1 . n <> 0 ; ::_thesis: ( R /* s1 is convergent & R /. 0 = lim (R /* s1) )
 s1 is non-zero by A27, SEQ_1:5;
then  s1 is non-zero 0 -convergent Real_Sequence by A26, FDIFF_1:def_1;
hence  ( R /* s1 is convergent & R /. 0 = lim (R /* s1) ) by A16; ::_thesis: verum
end;
hence  R is_continuous_in 0 by A25, NFCONT_3:7; ::_thesis: verum
end;

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
attrf is differentiable  means :Def7: :: NDIFF_3:def 7
f is_differentiable_on dom f;
end;

:: deftheorem Def7 defines differentiable NDIFF_3:def_7_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F holds
( f is differentiable iff f is_differentiable_on dom f );

Lm2:  [#] REAL is open
proof
 ([#] REAL) ` = {} REAL by XBOOLE_1:37;
hence  [#] REAL is open by Lm1, RCOMP_1:def_5; ::_thesis: verum
end;

registration
let F be non trivial RealNormSpace;
clusterV1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total differentiable for Element of K6(K7(REAL, the carrier of F));
existence
 ex b1 being Function of REAL, the carrier of F st b1 is differentiable
proof
reconsider Z = REAL as open Subset of REAL by Lm2;
reconsider f = REAL --> (0. F) as Function of REAL, the carrier of F ;
take  f ; ::_thesis: f is differentiable
A1: Z = dom f by FUNCT_2:def_1;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_/._x_=_(x_*_(0._F))_+_(0._F)
let x be Real; ::_thesis: ( x in Z implies f /. x = (x * (0. F)) + (0. F) )
assume  x in Z ; ::_thesis: f /. x = (x * (0. F)) + (0. F)
thus f /. x = 0. F by FUNCOP_1:7
.= x * (0. F) by RLVECT_1:10
.= (x * (0. F)) + (0. F) by RLVECT_1:4 ; ::_thesis: verum
end;
then  f is_differentiable_on Z by A1, Th21;
hence  f is differentiable by A1, Def7; ::_thesis: verum
end;
end;

theorem :: NDIFF_3:26
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds
f is_differentiable_on Z
proof
let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL
for f being differentiable PartFunc of REAL, the carrier of F 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, the carrier of F st Z c= dom f holds
f is_differentiable_on Z
let f be differentiable PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom f implies f is_differentiable_on Z )
assume A1: Z c= dom f ; ::_thesis: f is_differentiable_on Z
 f is_differentiable_on dom f by Def7;
hence  f is_differentiable_on Z by A1, Th24; ::_thesis: verum
end;