:: FDIFF_1 semantic presentation

begin


theorem Th1: :: FDIFF_1:1
for Y being Subset of REAL holds
( ( for r being Real holds
( r in Y iff r in REAL ) ) iff Y = REAL )
proof
let Y be Subset of REAL; ::_thesis: ( ( for r being Real holds
( r in Y iff r in REAL ) ) iff Y = REAL )
thus  ( ( for r being Real holds
( r in Y iff r in REAL ) ) implies Y = REAL ) ::_thesis: ( Y = REAL implies for r being Real holds
( r in Y iff r in REAL ) )
proof
assume  for r being Real holds
( r in Y iff r in REAL ) ; ::_thesis: Y = REAL
then  for y being set holds
( y in Y iff y in REAL ) ;
hence  Y = REAL by TARSKI:1; ::_thesis: verum
end;
assume A1: Y = REAL ; ::_thesis: for r being Real holds
( r in Y iff r in REAL )
let r be Real; ::_thesis: ( r in Y iff r in REAL )
thus  ( r in Y implies r in REAL ) ; ::_thesis: ( r in REAL implies r in Y )
thus  ( r in REAL implies r in Y ) by A1; ::_thesis: verum
end;

definition
let x be real number ;
let IT be Real_Sequence;
attrIT is x -convergent  means :Def1: :: FDIFF_1:def 1
( IT is convergent & lim IT = x );
end;

:: deftheorem Def1 defines -convergent FDIFF_1:def_1_:_
 for x being real number
for IT being Real_Sequence holds
( IT is x -convergent iff ( IT is convergent & lim IT = x ) );

registration
clusterV1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent for Element of K19(K20(NAT,REAL));
existence
 ex b1 being Real_Sequence st
( b1 is 0 -convergent & b1 is non-zero )
proof
deffunc H1( Element of NAT ) ->  Element of REAL = 1 / (c1 + 1);
consider s1 being Real_Sequence such that
A1: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
take  s1 ; ::_thesis: ( s1 is 0 -convergent & s1 is non-zero )
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0
let n be Element of NAT ; ::_thesis: s1 . n <> 0
 (n + 1) " <> 0 ;
then  1 / (n + 1) <> 0 by XCMPLX_1:215;
hence  s1 . n <> 0 by A1; ::_thesis: verum
end;
then A2: s1 is non-zero by SEQ_1:5;
 ( lim s1 = 0 & s1 is convergent ) by A1, SEQ_4:30;
then  s1 is 0 -convergent by Def1;
hence  ( s1 is 0 -convergent & s1 is non-zero ) by A2; ::_thesis: verum
end;
end;

registration
let f be 0 -convergent Real_Sequence;
cluster lim f ->  empty ;
coherence
 lim f is empty
proof
thus  lim f is empty by Def1; ::_thesis: verum
end;
end;

registration
clusterV6() quasi_total 0 -convergent  ->  convergent for Element of K19(K20(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is 0 -convergent holds
b1 is convergent
proof
let f be Real_Sequence; ::_thesis: ( f is 0 -convergent implies f is convergent )
assume  f is 0 -convergent ; ::_thesis: f is convergent
then  f is 0 -convergent ;
hence  f is convergent by Def1; ::_thesis: verum
end;
end;

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


definition
let IT be PartFunc of REAL,REAL;
attrIT is RestFunc-like  means :Def2: :: FDIFF_1:def 2
( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) );
end;

:: deftheorem Def2 defines RestFunc-like FDIFF_1:def_2_:_
 for IT being PartFunc of REAL,REAL 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 ) ) ) );

reconsider cf = REAL --> 0 as Function of REAL,REAL by FUNCOP_1:45;

registration
clusterV1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued RestFunc-like for Element of K19(K20(REAL,REAL));
existence
 ex b1 being PartFunc of REAL,REAL st b1 is RestFunc-like
proof
take f = cf; ::_thesis: f is RestFunc-like
thus  f is total ; :: according to FDIFF_1:def_2 ::_thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )
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_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(f_/*_h))_._n_=_0
let n be Nat; ::_thesis: ((h ") (#) (f /* h)) . n = 0
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 SEQ_1:8
.= ((h ") . n) * (f . (h . n)) by A3, A2, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
::_thesis: verum
end;
then  ( (h ") (#) (f /* h) is V8() & ((h ") (#) (f /* h)) . 0 = 0 ) by VALUED_0:def_18;
hence  ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 ) by SEQ_4:25; ::_thesis: verum
end;
hence  for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 ) ; ::_thesis: verum
end;
end;

definition
mode RestFunc is RestFunc-like PartFunc of REAL,REAL;
end;

definition
let IT be PartFunc of REAL,REAL;
attrIT is linear  means :Def3: :: FDIFF_1:def 3
( IT is total & ex r being Real st
for p being Real holds IT . p = r * p );
end;

:: deftheorem Def3 defines linear FDIFF_1:def_3_:_
 for IT being PartFunc of REAL,REAL holds
( IT is linear iff ( IT is total & ex r being Real st
for p being Real holds IT . p = r * p ) );

registration
clusterV1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued linear for Element of K19(K20(REAL,REAL));
existence
 ex b1 being PartFunc of REAL,REAL st b1 is linear
proof
deffunc H1( Real) ->  Element of REAL = 1 * c1;
defpred S1[ set ] means c1 in REAL ;
consider f being PartFunc of REAL,REAL such that
A1: ( ( for r being Real holds
( r in dom f iff S1[r] ) ) & ( for r being Real st r in dom f holds
f . r = H1(r) ) ) from SEQ_1:sch_3();
take  f ; ::_thesis: f is linear
 for y being set st y in REAL holds
y in dom f by A1;
then  REAL c= dom f by TARSKI:def_3;
then  dom f = REAL by XBOOLE_0:def_10;
hence  f is total by PARTFUN1:def_2; :: according to FDIFF_1:def_3 ::_thesis: ex r being Real st
for p being Real holds f . p = r * p
 for p being Real holds f . p = 1 * p by A1;
hence  ex r being Real st
for p being Real holds f . p = r * p ; ::_thesis: verum
end;
end;

definition
mode LinearFunc is linear PartFunc of REAL,REAL;
end;


theorem Th2: :: FDIFF_1:2
for L1, L2 being LinearFunc holds
( L1 + L2 is LinearFunc & L1 - L2 is LinearFunc )
proof
let L1, L2 be LinearFunc; ::_thesis: ( L1 + L2 is LinearFunc & L1 - L2 is LinearFunc )
consider g1 being Real such that
A1: for p being Real holds L1 . p = g1 * p by Def3;
consider g2 being Real such that
A2: for p being Real holds L2 . p = g2 * p by Def3;
A3: ( L1 is total & L2 is total ) by Def3;
now__::_thesis:_for_p_being_Real_holds_(L1_+_L2)_._p_=_(g1_+_g2)_*_p
let p be Real; ::_thesis: (L1 + L2) . p = (g1 + g2) * p
thus (L1 + L2) . p = (L1 . p) + (L2 . p) by A3, RFUNCT_1:56
.= (g1 * p) + (L2 . p) by A1
.= (g1 * p) + (g2 * p) by A2
.= (g1 + g2) * p ; ::_thesis: verum
end;
hence  L1 + L2 is LinearFunc by A3, Def3; ::_thesis: L1 - L2 is LinearFunc
now__::_thesis:_for_p_being_Real_holds_(L1_-_L2)_._p_=_(g1_-_g2)_*_p
let p be Real; ::_thesis: (L1 - L2) . p = (g1 - g2) * p
thus (L1 - L2) . p = (L1 . p) - (L2 . p) by A3, RFUNCT_1:56
.= (g1 * p) - (L2 . p) by A1
.= (g1 * p) - (g2 * p) by A2
.= (g1 - g2) * p ; ::_thesis: verum
end;
hence  L1 - L2 is LinearFunc by A3, Def3; ::_thesis: verum
end;

theorem Th3: :: FDIFF_1:3
for r being Real
for L being LinearFunc holds r (#) L is LinearFunc
proof
let r be Real; ::_thesis: for L being LinearFunc holds r (#) L is LinearFunc
let L be LinearFunc; ::_thesis: r (#) L is LinearFunc
consider g being Real such that
A1: for p being Real holds L . p = g * p by Def3;
A2: L is total by Def3;
now__::_thesis:_for_p_being_Real_holds_(r_(#)_L)_._p_=_(r_*_g)_*_p
let p be Real; ::_thesis: (r (#) L) . p = (r * g) * p
thus (r (#) L) . p = r * (L . p) by A2, RFUNCT_1:57
.= r * (g * p) by A1
.= (r * g) * p ; ::_thesis: verum
end;
hence  r (#) L is LinearFunc by A2, Def3; ::_thesis: verum
end;

theorem Th4: :: FDIFF_1:4
for R1, R2 being RestFunc holds
( R1 + R2 is RestFunc & R1 - R2 is RestFunc & R1 (#) R2 is RestFunc )
proof
let R1, R2 be RestFunc; ::_thesis: ( R1 + R2 is RestFunc & R1 - R2 is RestFunc & R1 (#) R2 is RestFunc )
A1: ( R1 is total & R2 is total ) by Def2;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((R1_+_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_+_R2)_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R1 + R2) /* h) is convergent & lim ((h ") (#) ((R1 + R2) /* h)) = 0 )
A2: (h ") (#) ((R1 + R2) /* h) = (h ") (#) ((R1 /* h) + (R2 /* h)) by A1, RFUNCT_2:13
.= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by SEQ_1:16 ;
A3: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def2;
hence  (h ") (#) ((R1 + R2) /* h) is convergent by A2, SEQ_2:5; ::_thesis: lim ((h ") (#) ((R1 + R2) /* h)) = 0
 ( lim ((h ") (#) (R1 /* h)) = 0 & lim ((h ") (#) (R2 /* h)) = 0 ) by Def2;
hence  lim ((h ") (#) ((R1 + R2) /* h)) = 0 + 0 by A3, A2, SEQ_2:6
.= 0 ;
::_thesis: verum
end;
hence  R1 + R2 is RestFunc by A1, Def2; ::_thesis: ( R1 - R2 is RestFunc & R1 (#) R2 is RestFunc )
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((R1_-_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_-_R2)_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R1 - R2) /* h) is convergent & lim ((h ") (#) ((R1 - R2) /* h)) = 0 )
A4: (h ") (#) ((R1 - R2) /* h) = (h ") (#) ((R1 /* h) - (R2 /* h)) by A1, RFUNCT_2:13
.= ((h ") (#) (R1 /* h)) - ((h ") (#) (R2 /* h)) by SEQ_1:21 ;
A5: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def2;
hence  (h ") (#) ((R1 - R2) /* h) is convergent by A4, SEQ_2:11; ::_thesis: lim ((h ") (#) ((R1 - R2) /* h)) = 0
 ( lim ((h ") (#) (R1 /* h)) = 0 & lim ((h ") (#) (R2 /* h)) = 0 ) by Def2;
hence  lim ((h ") (#) ((R1 - R2) /* h)) = 0 - 0 by A5, A4, SEQ_2:12
.= 0 ;
::_thesis: verum
end;
hence  R1 - R2 is RestFunc by A1, Def2; ::_thesis: R1 (#) R2 is RestFunc
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((R1_(#)_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_(#)_R2)_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R1 (#) R2) /* h) is convergent & lim ((h ") (#) ((R1 (#) R2) /* h)) = 0 )
A6: (h ") (#) (R2 /* h) is convergent by Def2;
A7: h " is non-zero by SEQ_1:33;
A8: ( (h ") (#) (R1 /* h) is convergent & h is convergent ) by Def2;
then A9: h (#) ((h ") (#) (R1 /* h)) is convergent by SEQ_2:14;
 ( lim ((h ") (#) (R1 /* h)) = 0 & lim h = 0 ) by Def2;
then A10: lim (h (#) ((h ") (#) (R1 /* h))) = 0 * 0 by A8, SEQ_2:15
.= 0 ;
A11: (h ") (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by A1, RFUNCT_2:13
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) /" (h (#) (h ")) by SEQ_1:43, A7
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) (#) (((h ") ") (#) (h ")) by SEQ_1:36
.= (h (#) (h ")) (#) ((R1 /* h) (#) ((h ") (#) (R2 /* h))) by SEQ_1:14
.= ((h (#) (h ")) (#) (R1 /* h)) (#) ((h ") (#) (R2 /* h)) by SEQ_1:14
.= (h (#) ((h ") (#) (R1 /* h))) (#) ((h ") (#) (R2 /* h)) by SEQ_1:14 ;
hence  (h ") (#) ((R1 (#) R2) /* h) is convergent by A6, A9, SEQ_2:14; ::_thesis: lim ((h ") (#) ((R1 (#) R2) /* h)) = 0
 lim ((h ") (#) (R2 /* h)) = 0 by Def2;
hence  lim ((h ") (#) ((R1 (#) R2) /* h)) = 0 * 0 by A6, A9, A10, A11, SEQ_2:15
.= 0 ;
::_thesis: verum
end;
hence  R1 (#) R2 is RestFunc by A1, Def2; ::_thesis: verum
end;

theorem Th5: :: FDIFF_1:5
for r being Real
for R being RestFunc holds r (#) R is RestFunc
proof
let r be Real; ::_thesis: for R being RestFunc holds r (#) R is RestFunc
let R be RestFunc; ::_thesis: r (#) R is RestFunc
A1: R is total by Def2;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((r_(#)_R)_/*_h)_is_convergent_&_lim_((h_")_(#)_((r_(#)_R)_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((r (#) R) /* h) is convergent & lim ((h ") (#) ((r (#) R) /* h)) = 0 )
A2: (h ") (#) ((r (#) R) /* h) = (h ") (#) (r (#) (R /* h)) by A1, RFUNCT_2:14
.= r (#) ((h ") (#) (R /* h)) by SEQ_1:19 ;
A3: (h ") (#) (R /* h) is convergent by Def2;
hence  (h ") (#) ((r (#) R) /* h) is convergent by A2, SEQ_2:7; ::_thesis: lim ((h ") (#) ((r (#) R) /* h)) = 0
 lim ((h ") (#) (R /* h)) = 0 by Def2;
hence  lim ((h ") (#) ((r (#) R) /* h)) = r * 0 by A3, A2, SEQ_2:8
.= 0 ;
::_thesis: verum
end;
hence  r (#) R is RestFunc by A1, Def2; ::_thesis: verum
end;

theorem Th6: :: FDIFF_1:6
for L1, L2 being LinearFunc holds L1 (#) L2 is RestFunc-like
proof
let L1, L2 be LinearFunc; ::_thesis: L1 (#) L2 is RestFunc-like
consider x1 being Real such that
A1: for p being Real holds L1 . p = x1 * p by Def3;
A2: ( L1 is total & L2 is total ) by Def3;
hence  L1 (#) L2 is total ; :: according to FDIFF_1:def_2 ::_thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((L1 (#) L2) /* h) is convergent & lim ((h ") (#) ((L1 (#) L2) /* h)) = 0 )
consider x2 being Real such that
A3: for p being Real holds L2 . p = x2 * p by Def3;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((L1_(#)_L2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((L1_(#)_L2)_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((L1 (#) L2) /* h) is convergent & lim ((h ") (#) ((L1 (#) L2) /* h)) = 0 )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_")_(#)_((L1_(#)_L2)_/*_h))_._n_=_((x1_*_x2)_(#)_h)_._n
let n be Element of NAT ; ::_thesis: ((h ") (#) ((L1 (#) L2) /* h)) . n = ((x1 * x2) (#) h) . n
A4: h . n <> 0 by SEQ_1:5;
thus ((h ") (#) ((L1 (#) L2) /* h)) . n = ((h ") . n) * (((L1 (#) L2) /* h) . n) by SEQ_1:8
.= ((h ") . n) * ((L1 (#) L2) . (h . n)) by A2, FUNCT_2:115
.= ((h ") . n) * ((L1 . (h . n)) * (L2 . (h . n))) by A2, RFUNCT_1:56
.= (((h ") . n) * (L1 . (h . n))) * (L2 . (h . n))
.= (((h . n) ") * (L1 . (h . n))) * (L2 . (h . n)) by VALUED_1:10
.= (((h . n) ") * ((h . n) * x1)) * (L2 . (h . n)) by A1
.= ((((h . n) ") * (h . n)) * x1) * (L2 . (h . n))
.= (1 * x1) * (L2 . (h . n)) by A4, XCMPLX_0:def_7
.= x1 * (x2 * (h . n)) by A3
.= (x1 * x2) * (h . n)
.= ((x1 * x2) (#) h) . n by SEQ_1:9 ; ::_thesis: verum
end;
then A5: (h ") (#) ((L1 (#) L2) /* h) = (x1 * x2) (#) h by FUNCT_2:63;
thus  (h ") (#) ((L1 (#) L2) /* h) is convergent by A5, SEQ_2:7; ::_thesis: lim ((h ") (#) ((L1 (#) L2) /* h)) = 0
 lim h = 0 ;
hence  lim ((h ") (#) ((L1 (#) L2) /* h)) = (x1 * x2) * 0 by A5, SEQ_2:8
.= 0 ;
::_thesis: verum
end;
hence  for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((L1 (#) L2) /* h) is convergent & lim ((h ") (#) ((L1 (#) L2) /* h)) = 0 ) ; ::_thesis: verum
end;

theorem Th7: :: FDIFF_1:7
for R being RestFunc
for L being LinearFunc holds
( R (#) L is RestFunc & L (#) R is RestFunc )
proof
let R be RestFunc; ::_thesis: for L being LinearFunc holds
( R (#) L is RestFunc & L (#) R is RestFunc )
let L be LinearFunc; ::_thesis: ( R (#) L is RestFunc & L (#) R is RestFunc )
A1: L is total by Def3;
consider x1 being Real such that
A2: for p being Real holds L . p = x1 * p by Def3;
A3: R is total by Def2;
A4: now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_((R_(#)_L)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R_(#)_L)_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R (#) L) /* h) is convergent & lim ((h ") (#) ((R (#) L) /* h)) = 0 )
A5: (h ") (#) (R /* h) is convergent by Def2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(L_/*_h)_._n_=_(x1_(#)_h)_._n
let n be Element of NAT ; ::_thesis: (L /* h) . n = (x1 (#) h) . n
thus (L /* h) . n = L . (h . n) by A1, FUNCT_2:115
.= x1 * (h . n) by A2
.= (x1 (#) h) . n by SEQ_1:9 ; ::_thesis: verum
end;
then A6: L /* h = x1 (#) h by FUNCT_2:63;
A7: L /* h is convergent by A6, SEQ_2:7;
 lim h = 0 ;
then A8: lim (L /* h) = x1 * 0 by A6, SEQ_2:8
.= 0 ;
A9: (h ") (#) ((R (#) L) /* h) = (h ") (#) ((R /* h) (#) (L /* h)) by A3, A1, RFUNCT_2:13
.= ((h ") (#) (R /* h)) (#) (L /* h) by SEQ_1:14 ;
hence  (h ") (#) ((R (#) L) /* h) is convergent by A7, A5, SEQ_2:14; ::_thesis: lim ((h ") (#) ((R (#) L) /* h)) = 0
 lim ((h ") (#) (R /* h)) = 0 by Def2;
hence  lim ((h ") (#) ((R (#) L) /* h)) = 0 * 0 by A9, A7, A8, A5, SEQ_2:15
.= 0 ;
::_thesis: verum
end;
hence  R (#) L is RestFunc by A3, A1, Def2; ::_thesis: L (#) R is RestFunc
thus  L (#) R is RestFunc by A3, A1, A4, Def2; ::_thesis: verum
end;

definition
let f be PartFunc of REAL,REAL;
let x0 be real number ;
predf is_differentiable_in x0 means :Def4: :: FDIFF_1:def 4
 ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) );
end;

:: deftheorem Def4 defines is_differentiable_in FDIFF_1:def_4_:_
 for f being PartFunc of REAL,REAL
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 ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) );

definition
let f be PartFunc of REAL,REAL;
let x0 be real number ;
assume A1: f is_differentiable_in x0 ;
func diff (f,x0) ->  Real means :Def5: :: FDIFF_1:def 5
 ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 Real ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def4;
consider L being LinearFunc, R being RestFunc 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 Real such that
A5: for p being Real holds L . p = r * p by Def3;
take  r ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 = r * 1 by A5
.= r ;
hence  ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 Real st ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 ex R being RestFunc 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 Real; ::_thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 ex R being RestFunc 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 ex R being RestFunc 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 ex R being RestFunc 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 ex R being RestFunc 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, R being RestFunc 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 Real such that
A11: for p being Real holds L . p = r1 * p by Def3;
consider N1 being Neighbourhood of x0 such that
 N1 c= dom f and
A12: ex L being LinearFunc ex R being RestFunc 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, R1 being RestFunc 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 Real such that
A15: for p being Real holds L1 . p = p1 * p by Def3;
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  s1 is 0 -convergent by Def1;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A20;
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  x0 + (g / (n + 2)) ; ::_thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 )
 0 + 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  ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A16, A18, A19; ::_thesis: verum
end;
A23: s = p1 * 1 by A13, A15;
A24: r = r1 * 1 by A9, A11;
A25: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_
(r_*_(x_-_x0))_+_(R_._(x_-_x0))_=_(s_*_(x_-_x0))_+_(R1_._(x_-_x0))
let x be Real; ::_thesis: ( x in N & x in N1 implies (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) )
assume that
A26: x in N and
A27: x in N1 ; ::_thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (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  (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A11;
hence  (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) by A15, A24, A23; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n
 R1 is total by Def2;
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 Def2;
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  (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A25;
then A31: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;
A32: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A30, A29, FUNCT_2:108
.= ((h ") (#) (R /* h)) . n by A30, SEQ_1:8 ;
A33: h . n <> 0 by A30, SEQ_1:5;
A34: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A30, A28, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by A30, SEQ_1:8 ;
A35: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74
.= s * 1 by A33, XCMPLX_1:60
.= s ;
(r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74
.= r * 1 by A33, XCMPLX_1:60
.= r ;
then  r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A31, A35, XCMPLX_1:62;
then  r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A32, A34;
hence  r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A30, RFUNCT_2:1; ::_thesis: verum
end;
then  ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is V8() & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18;
then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25;
A37: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by Def2;
 ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by Def2;
then  r - s = 0 - 0 by A36, A37, SEQ_2:12;
hence  r = s ; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines diff FDIFF_1:def_5_:_
 for f being PartFunc of REAL,REAL
for x0 being real number st f is_differentiable_in x0 holds
for b3 being Real holds
( b3 = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
( b3 = 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 PartFunc of REAL,REAL;
let X be set ;
predf is_differentiable_on X means :Def6: :: FDIFF_1:def 6
( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def6 defines is_differentiable_on FDIFF_1:def_6_:_
 for f being PartFunc of REAL,REAL
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 Th8: :: FDIFF_1:8
for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
X is Subset of REAL
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
X is Subset of REAL
let f be PartFunc of REAL,REAL; ::_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 Def6;
hence  X is Subset of REAL by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th9: :: FDIFF_1:9
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL 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 Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
let f be PartFunc of REAL,REAL; ::_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  Z c= dom f by Def6; ::_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 A2: x0 in Z ; ::_thesis: f is_differentiable_in x0
then  f | Z is_differentiable_in x0 by A1, Def6;
then consider N being Neighbourhood of x0 such that
A3: N c= dom (f | Z) and
A4: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by Def4;
take  N ; :: according to FDIFF_1:def_4 ::_thesis: ( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 A3, XBOOLE_1:1; ::_thesis: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
consider L being LinearFunc, R being RestFunc such that
A5: for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;
take  L ; ::_thesis: ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
take  R ; ::_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 A6: x in N ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then  ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
then  (f . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3, A6, FUNCT_1:47;
hence  (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, FUNCT_1:49; ::_thesis: verum
end;
assume that
A7: Z c= dom f and
A8: 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 A7; :: according to FDIFF_1:def_6 ::_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 A9: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0
then consider N1 being Neighbourhood of x0 such that
A10: N1 c= Z by RCOMP_1:18;
 f is_differentiable_in x0 by A8, A9;
then consider N being Neighbourhood of x0 such that
A11: N c= dom f and
A12: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by Def4;
consider N2 being Neighbourhood of x0 such that
A13: N2 c= N1 and
A14: N2 c= N by RCOMP_1:17;
A15: N2 c= Z by A10, A13, XBOOLE_1:1;
take  N2 ; :: according to FDIFF_1:def_4 ::_thesis: ( N2 c= dom (f | Z) & ex L being LinearFunc ex R being RestFunc 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 A11, A14, XBOOLE_1:1;
then  N2 c= (dom f) /\ Z by A15, XBOOLE_1:19;
hence A16: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being LinearFunc ex R being RestFunc 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, R being RestFunc such that
A17: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A12;
A18: x0 in N2 by RCOMP_1:16;
take  L ; ::_thesis: ex R being RestFunc 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))
let x be Real; ::_thesis: ( x in N2 implies ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A19: 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 A14, A17;
then  ((f | Z) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A16, A19, FUNCT_1:47;
hence  ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A16, A18, FUNCT_1:47; ::_thesis: verum
end;

theorem :: FDIFF_1:10
for Y being Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Y holds
Y is open
proof
let Y be Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on Y holds
Y is open
let f be PartFunc of REAL,REAL; ::_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, Def6;
then consider N being Neighbourhood of x0 such that
A2: N c= dom (f | Y) and
 ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((f | Y) . x) - ((f | Y) . x0) = (L . (x - x0)) + (R . (x - x0)) by Def4;
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 PartFunc of REAL,REAL;
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X ->  PartFunc of REAL,REAL means :Def7: :: FDIFF_1:def 7
( dom it = X & ( for x being Real st x in X holds
it . x = diff (f,x) ) );
existence
 ex b1 being PartFunc of REAL,REAL st
( dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff (f,x) ) )
proof
deffunc H1( Real) ->  Real = diff (f,$1);
defpred S1[ set ] means $1 in X;
consider F being PartFunc of REAL,REAL such that
A2: ( ( for x being Real holds
( x in dom F iff S1[x] ) ) & ( for x being Real st x in dom F holds
F . x = H1(x) ) ) from SEQ_1:sch_3();
take  F ; ::_thesis: ( dom F = X & ( for x being Real st x in X holds
F . x = diff (f,x) ) )
now__::_thesis:_for_y_being_set_st_y_in_X_holds_
y_in_dom_F
A3: X is Subset of REAL by A1, Th8;
let y be set ; ::_thesis: ( y in X implies y in dom F )
assume  y in X ; ::_thesis: y in dom F
hence  y in dom F by A2, A3; ::_thesis: verum
end;
then A4: X c= dom F by TARSKI:def_3;
 for y being set st y in dom F holds
y in X by A2;
then  dom F c= X by TARSKI:def_3;
hence  dom F = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Real st x in X holds
F . x = diff (f,x)
now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
F_._x_=_diff_(f,x)
let x be Real; ::_thesis: ( x in X implies F . x = diff (f,x) )
assume  x in X ; ::_thesis: F . x = diff (f,x)
then  x in dom F by A2;
hence  F . x = diff (f,x) by A2; ::_thesis: verum
end;
hence  for x being Real st x in X holds
F . x = diff (f,x) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of REAL,REAL 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 F, G be PartFunc of REAL,REAL; ::_thesis: ( dom F = X & ( for x being Real st x in X holds
F . x = diff (f,x) ) & dom G = X & ( for x being Real st x in X holds
G . x = diff (f,x) ) implies F = G )
assume that
A5: dom F = X and
A6: for x being Real st x in X holds
F . x = diff (f,x) and
A7: dom G = X and
A8: for x being Real st x in X holds
G . x = diff (f,x) ; ::_thesis: F = G
now__::_thesis:_for_x_being_Real_st_x_in_dom_F_holds_
F_._x_=_G_._x
let x be Real; ::_thesis: ( x in dom F implies F . x = G . x )
assume A9: x in dom F ; ::_thesis: F . x = G . x
then  F . x = diff (f,x) by A5, A6;
hence  F . x = G . x by A5, A8, A9; ::_thesis: verum
end;
hence  F = G by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines `| FDIFF_1:def_7_:_
 for f being PartFunc of REAL,REAL
for X being set st f is_differentiable_on X holds
for b3 being PartFunc of REAL,REAL holds
( b3 = f `| X iff ( dom b3 = X & ( for x being Real st x in X holds
b3 . x = diff (f,x) ) ) );

theorem :: FDIFF_1:11
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ex r being Real st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
proof
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom f & ex r being Real st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom f & ex r being Real st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) ) )
set R = cf;
A1: dom cf = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )
A2: now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0
A3: rng h c= dom cf by A1;
A4: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A4, A3, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
::_thesis: verum
end;
then A5: (h ") (#) (cf /* h) is V8() by VALUED_0:def_18;
hence  (h ") (#) (cf /* h) is convergent ; ::_thesis: lim ((h ") (#) (cf /* h)) = 0
 ((h ") (#) (cf /* h)) . 0 = 0 by A2;
hence  lim ((h ") (#) (cf /* h)) = 0 by A5, SEQ_4:25; ::_thesis: verum
end;
then reconsider R = cf as RestFunc by Def2;
set L = cf;
 for p being Real holds cf . p = 0 * p by FUNCOP_1:7;
then reconsider L = cf as LinearFunc by Def3;
assume A6: Z c= dom f ; ::_thesis: ( for r being Real holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) ) )
given r being Real such that A7: rng f = {r} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
A8: 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  x0 in dom f ; ::_thesis: f . x0 = r
then  f . x0 in {r} by A7, FUNCT_1:def_3;
hence  f . x0 = r by TARSKI:def_1; ::_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 A6, A11, 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)) )
assume  x in N ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
hence (f . x) - (f . x0) = r - (f . x0) by A8, A12
.= r - r by A6, A8, A10
.= (L . (x - x0)) + 0 by FUNCOP_1:7
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
hence  f is_differentiable_in x0 by A12, Def4; ::_thesis: verum
end;
hence A13: f is_differentiable_on Z by A6, Th9; ::_thesis: for x being Real st x in Z holds
(f `| Z) . x = 0
let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) . x0 = 0 )
assume A14: x0 in Z ; ::_thesis: (f `| Z) . x0 = 0
then A15: f is_differentiable_in x0 by A9;
then  ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Def4;
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)) )
assume  x in N ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
hence (f . x) - (f . x0) = r - (f . x0) by A8, A16
.= r - r by A6, A8, A14
.= (L . (x - x0)) + 0 by FUNCOP_1:7
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
thus (f `| Z) . x0 = diff (f,x0) by A13, A14, Def7
.= L . 1 by A15, A16, A17, Def5
.= 0 by FUNCOP_1:7 ; ::_thesis: verum
end;

registration
let h be non-zero 0 -convergent Real_Sequence;
let n be Element of NAT ;
clusterh ^\ n ->  non-zero 0 -convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = h ^\ n holds
( b1 is non-zero & b1 is 0 -convergent )
proof
 lim h = 0 ;
then  lim (h ^\ n) = 0 by SEQ_4:20;
then  h ^\ n is 0 -convergent by Def1;
hence  for b1 being Real_Sequence st b1 = h ^\ n holds
( b1 is non-zero & b1 is 0 -convergent ) ; ::_thesis: verum
end;
end;

theorem Th12: :: FDIFF_1:12
for f being PartFunc of REAL,REAL
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 V8() 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 PartFunc of REAL,REAL; ::_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 V8() 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 V8() 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 V8() 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 V8() 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 ex R being RestFunc st
for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def4;
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 V8() 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 V8() 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;
 ( x0 + 0 < x0 + g & x0 - g < x0 - 0 ) by A9, XREAL_1:8, XREAL_1:15;
then A11: x0 in N2 by A10;
A12: rng c c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or 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;
 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;
 lim h = 0 ;
then  lim (h + c) = 0 + 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;
thus  rng (c ^\ n) c= N2 ::_thesis: rng ((h + c) ^\ n) c= N2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in N2 )
assume  y in rng (c ^\ n) ; ::_thesis: y in N2
hence  y in N2 by A11, A16, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or 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;
 n + 0 <= 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;
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, R being RestFunc such that
A21: for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
A22: rng (c ^\ n) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom f )
assume A23: y in rng (c ^\ n) ; ::_thesis: y in dom f
 rng (c ^\ n) = rng c by VALUED_0:26;
then  y = x0 by A7, A23, TARSKI:def_1;
then  y in N by A4, A11;
hence  y in dom f by A2; ::_thesis: verum
end;
A24: L is total by Def3;
A25: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Real_Sequence such that
A26: for k being Element of NAT holds s1 . k = H1(k) from SEQ_1:sch_1();
A27: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_n1_being_Element_of_NAT_st_
for_k_being_Element_of_NAT_st_n1_<=_k_holds_
abs_((s1_._k)_-_(L_._1))_<_r
A28: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by Def2;
let r be real number ; ::_thesis: ( 0 < r implies ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((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
abs ((s1 . k) - (L . 1)) < r
then consider m being Element of NAT  such that
A29: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) < r by A28, SEQ_2:def_7;
take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
let k be Element of NAT ; ::_thesis: ( n1 <= k implies abs ((s1 . k) - (L . 1)) < r )
assume A30: n1 <= k ; ::_thesis: abs ((s1 . k) - (L . 1)) < r
abs ((s1 . k) - (L . 1)) = abs (((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)) by A26
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) ;
hence  abs ((s1 . k) - (L . 1)) < r by A29, A30; ::_thesis: verum
end;
consider s being Real such that
A31: for p1 being Real holds L . p1 = s * p1 by Def3;
A32: L . 1 = s * 1 by A31
.= s ;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_(#)_((h_^\_n)_"))_._m_=_s1_._m
let m be Element of NAT ; ::_thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m
A33: (h ^\ n) . m <> 0 by SEQ_1:5;
thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10
.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A24, FUNCT_2:115
.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A31
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A33, XCMPLX_0:def_7
.= s1 . m by A26, A32 ; ::_thesis: verum
end;
then A34: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;
hence  ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A27, SEQ_2:def_6; ::_thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1
hence  lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A34, A27, SEQ_2:def_7; ::_thesis: verum
end;
A35: rng ((h + c) ^\ n) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or 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;
A36: rng (h + c) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or 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;
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 Def2;
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
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by RFUNCT_2:1
.= (f . (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A35, FUNCT_2:108
.= (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) by A22, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A37
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A24, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A40, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; ::_thesis: verum
end;
then  (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
then A41: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by A36, VALUED_0:27
.= (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) ") by A12, VALUED_0:27
.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17
.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18
.= (((f /* (h + c)) - (f /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;
then A42: L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A25, SEQ_4:22;
thus  (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A25, A41, SEQ_4:21; ::_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, A42, Def5; ::_thesis: verum
end;

theorem Th13: :: FDIFF_1:13
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
proof
let x0 be Real; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
let f1, f2 be PartFunc of REAL,REAL; ::_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 ex R being RestFunc st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def4;
consider L1 being LinearFunc, R1 being RestFunc 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 ex R being RestFunc st
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, Def4;
consider L2 being LinearFunc, R2 being RestFunc 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 by Th4;
reconsider L = L1 + L2 as LinearFunc by Th2;
A9: ( L1 is total & L2 is total ) by Def3;
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 VALUED_1:def_1;
A14: ( R1 is total & R2 is total ) by Def2;
A15: 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)) )
A16: x0 in N by RCOMP_1:16;
assume A17: 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, VALUED_1:def_1
.= ((f1 . x) + (f2 . x)) - ((f1 . x0) + (f2 . x0)) by A13, A16, VALUED_1:def_1
.= ((f1 . x) - (f1 . x0)) + ((f2 . x) - (f2 . x0))
.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((f2 . x) - (f2 . x0)) by A5, A10, A17
.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((L2 . (x - x0)) + (R2 . (x - x0))) by A8, A11, A17
.= ((L1 . (x - x0)) + (L2 . (x - x0))) + ((R1 . (x - x0)) + (R2 . (x - x0)))
.= (L . (x - x0)) + ((R1 . (x - x0)) + (R2 . (x - x0))) by A9, RFUNCT_1:56
.= (L . (x - x0)) + (R . (x - x0)) by A14, RFUNCT_1:56 ;
::_thesis: verum
end;
hence  f1 + f2 is_differentiable_in x0 by A13, Def4; ::_thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0))
hence  diff ((f1 + f2),x0) = L . 1 by A13, A15, Def5
.= (L1 . 1) + (L2 . 1) by A9, RFUNCT_1:56
.= (diff (f1,x0)) + (L2 . 1) by A1, A3, A5, Def5
.= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def5 ;
::_thesis: verum
end;

theorem Th14: :: FDIFF_1:14
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
proof
let x0 be Real; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
let f1, f2 be PartFunc of REAL,REAL; ::_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 ex R being RestFunc st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def4;
consider L1 being LinearFunc, R1 being RestFunc 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 ex R being RestFunc st
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, Def4;
consider L2 being LinearFunc, R2 being RestFunc 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 by Th4;
reconsider L = L1 - L2 as LinearFunc by Th2;
A9: ( L1 is total & L2 is total ) by Def3;
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 VALUED_1:12;
A14: ( R1 is total & R2 is total ) by Def2;
A15: 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)) )
A16: x0 in N by RCOMP_1:16;
assume A17: 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, VALUED_1:13
.= ((f1 . x) - (f2 . x)) - ((f1 . x0) - (f2 . x0)) by A13, A16, VALUED_1:13
.= ((f1 . x) - (f1 . x0)) - ((f2 . x) - (f2 . x0))
.= ((L1 . (x - x0)) + (R1 . (x - x0))) - ((f2 . x) - (f2 . x0)) by A5, A10, A17
.= ((L1 . (x - x0)) + (R1 . (x - x0))) - ((L2 . (x - x0)) + (R2 . (x - x0))) by A8, A11, A17
.= ((L1 . (x - x0)) - (L2 . (x - x0))) + ((R1 . (x - x0)) - (R2 . (x - x0)))
.= (L . (x - x0)) + ((R1 . (x - x0)) - (R2 . (x - x0))) by A9, RFUNCT_1:56
.= (L . (x - x0)) + (R . (x - x0)) by A14, RFUNCT_1:56 ;
::_thesis: verum
end;
hence  f1 - f2 is_differentiable_in x0 by A13, Def4; ::_thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))
hence  diff ((f1 - f2),x0) = L . 1 by A13, A15, Def5
.= (L1 . 1) - (L2 . 1) by A9, RFUNCT_1:56
.= (diff (f1,x0)) - (L2 . 1) by A1, A3, A5, Def5
.= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def5 ;
::_thesis: verum
end;

theorem Th15: :: FDIFF_1:15
for x0, r being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
proof
let x0, r be Real; ::_thesis: for f being PartFunc of REAL,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,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 ex R being RestFunc st
for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by Def4;
consider L1 being LinearFunc, R1 being RestFunc 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 by Th5;
reconsider L = r (#) L1 as LinearFunc by Th3;
A5: L1 is total by Def3;
A6: N1 c= dom (r (#) f) by A2, VALUED_1:def_5;
A7: R1 is total by Def2;
A8: 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)) )
A9: x0 in N1 by RCOMP_1:16;
assume A10: 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, VALUED_1:def_5
.= (r * (f . x)) - (r * (f . x0)) by A6, A9, VALUED_1:def_5
.= r * ((f . x) - (f . x0))
.= r * ((L1 . (x - x0)) + (R1 . (x - x0))) by A4, A10
.= (r * (L1 . (x - x0))) + (r * (R1 . (x - x0)))
.= (L . (x - x0)) + (r * (R1 . (x - x0))) by A5, RFUNCT_1:57
.= (L . (x - x0)) + (R . (x - x0)) by A7, RFUNCT_1:57 ;
::_thesis: verum
end;
hence  r (#) f is_differentiable_in x0 by A6, Def4; ::_thesis: diff ((r (#) f),x0) = r * (diff (f,x0))
hence  diff ((r (#) f),x0) = L . 1 by A6, A8, Def5
.= r * (L1 . 1) by A5, RFUNCT_1:57
.= r * (diff (f,x0)) by A1, A2, A4, Def5 ;
::_thesis: verum
end;

theorem Th16: :: FDIFF_1:16
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) )
proof
let x0 be Real; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((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) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) )
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def4;
consider L1 being LinearFunc, R1 being RestFunc 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 ex R being RestFunc st
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, Def4;
consider L2 being LinearFunc, R2 being RestFunc 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 R18 = R2 (#) L1 as RestFunc by Th7;
reconsider R17 = R1 (#) R2 as RestFunc by Th4;
A9: R18 is total by Def2;
reconsider R16 = R1 (#) L2 as RestFunc by Th7;
reconsider R14 = L1 (#) L2 as RestFunc by Th6;
reconsider R19 = R16 + R17 as RestFunc by Th4;
reconsider R20 = R19 + R18 as RestFunc by Th4;
A10: R14 is total by Def2;
reconsider R12 = (f1 . x0) (#) R2 as RestFunc by Th5;
A11: R2 is total by Def2;
reconsider L11 = (f2 . x0) (#) L1 as LinearFunc by Th3;
A12: L1 is total by Def3;
reconsider R11 = (f2 . x0) (#) R1 as RestFunc by Th5;
A13: R1 is total by Def2;
reconsider R13 = R11 + R12 as RestFunc by Th4;
reconsider R15 = R13 + R14 as RestFunc by Th4;
reconsider R = R15 + R20 as RestFunc by Th4;
consider N being Neighbourhood of x0 such that
A14: N c= N1 and
A15: N c= N2 by RCOMP_1:17;
A16: N c= dom f2 by A6, A15, XBOOLE_1:1;
 N c= dom f1 by A3, A14, XBOOLE_1:1;
then  N /\ N c= (dom f1) /\ (dom f2) by A16, XBOOLE_1:27;
then A17: N c= dom (f1 (#) f2) by VALUED_1:def_4;
reconsider L12 = (f1 . x0) (#) L2 as LinearFunc by Th3;
A18: L2 is total by Def3;
reconsider L = L11 + L12 as LinearFunc by Th2;
A19: R16 is total by Def2;
A20: ( L11 is total & L12 is total ) by Def3;
A21: 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)) )
assume A22: x in N ; ::_thesis: ((f1 (#) f2) . x) - ((f1 (#) f2) . x0) = (L . (x - x0)) + (R . (x - x0))
then A23: ((f1 . x) - (f1 . x0)) + (f1 . x0) = ((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0) by A5, A14;
thus ((f1 (#) f2) . x) - ((f1 (#) f2) . x0) = ((f1 . x) * (f2 . x)) - ((f1 (#) f2) . x0) by VALUED_1:5
.= ((((f1 . x) * (f2 . x)) + (- ((f1 . x) * (f2 . x0)))) + ((f1 . x) * (f2 . x0))) - ((f1 . x0) * (f2 . x0)) by VALUED_1:5
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + (((f1 . x) - (f1 . x0)) * (f2 . x0))
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * (f2 . x0)) by A5, A14, A22
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + (((f2 . x0) * (L1 . (x - x0))) + ((R1 . (x - x0)) * (f2 . x0)))
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + ((L11 . (x - x0)) + ((f2 . x0) * (R1 . (x - x0)))) by A12, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0)) * ((f2 . x) - (f2 . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A13, A23, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A8, A15, A22
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((f1 . x0) * (L2 . (x - x0))) + ((f1 . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((f1 . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A18, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (R12 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A11, RFUNCT_1:57
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + ((R11 . (x - x0)) + (R12 . (x - x0)))))
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + (R13 . (x - x0)))) by A13, A11, RFUNCT_1:56
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((L11 . (x - x0)) + (L12 . (x - x0))) + (R13 . (x - x0)))
.= ((((L1 . (x - x0)) * (L2 . (x - x0))) + ((L1 . (x - x0)) * (R2 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A20, RFUNCT_1:56
.= (((R14 . (x - x0)) + ((R2 . (x - x0)) * (L1 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A12, A18, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + (((R1 . (x - x0)) * (L2 . (x - x0))) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A12, A11, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A18, A13, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0))) by A13, A11, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0))) by A13, A11, A19, RFUNCT_1:56
.= ((R14 . (x - x0)) + ((R19 . (x - x0)) + (R18 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))
.= ((L . (x - x0)) + (R13 . (x - x0))) + ((R14 . (x - x0)) + (R20 . (x - x0))) by A13, A11, A19, A9, RFUNCT_1:56
.= (L . (x - x0)) + (((R13 . (x - x0)) + (R14 . (x - x0))) + (R20 . (x - x0)))
.= (L . (x - x0)) + ((R15 . (x - x0)) + (R20 . (x - x0))) by A13, A11, A10, RFUNCT_1:56
.= (L . (x - x0)) + (R . (x - x0)) by A13, A11, A10, A19, A9, RFUNCT_1:56 ; ::_thesis: verum
end;
hence  f1 (#) f2 is_differentiable_in x0 by A17, Def4; ::_thesis: diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0)))
hence  diff ((f1 (#) f2),x0) = L . 1 by A17, A21, Def5
.= (L11 . 1) + (L12 . 1) by A20, RFUNCT_1:56
.= ((f2 . x0) * (L1 . 1)) + (L12 . 1) by A12, RFUNCT_1:57
.= ((f2 . x0) * (L1 . 1)) + ((f1 . x0) * (L2 . 1)) by A18, RFUNCT_1:57
.= ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (L2 . 1)) by A1, A3, A5, Def5
.= ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) by A2, A6, A8, Def5 ;
::_thesis: verum
end;

theorem Th17: :: FDIFF_1:17
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
proof
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) ) )
set R = cf;
A1: dom cf = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )
A2: now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0
A3: rng h c= dom cf by A1;
A4: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A4, A3, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
::_thesis: verum
end;
then A5: (h ") (#) (cf /* h) is V8() by VALUED_0:def_18;
hence  (h ") (#) (cf /* h) is convergent ; ::_thesis: lim ((h ") (#) (cf /* h)) = 0
 ((h ") (#) (cf /* h)) . 0 = 0 by A2;
hence  lim ((h ") (#) (cf /* h)) = 0 by A5, SEQ_4:25; ::_thesis: verum
end;
then reconsider R = cf as RestFunc by Def2;
reconsider L = id REAL as PartFunc of REAL,REAL ;
 for p being Real holds L . p = 1 * p by FUNCT_1:18;
then reconsider L = L as LinearFunc by Def3;
assume that
A6: Z c= dom f and
A7: f | Z = id Z ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
A8: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f_._x_=_x
let x be Real; ::_thesis: ( x in Z implies f . x = x )
assume A9: x in Z ; ::_thesis: f . x = x
then  (f | Z) . x = x by A7, FUNCT_1:18;
hence  f . x = x by A9, FUNCT_1:49; ::_thesis: verum
end;
A10: 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 A11: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A12: N c= Z by RCOMP_1:18;
A13: 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)) )
assume  x in N ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
hence (f . x) - (f . x0) = x - (f . x0) by A8, A12
.= x - x0 by A8, A11
.= (L . (x - x0)) + 0 by FUNCT_1:18
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
 N c= dom f by A6, A12, XBOOLE_1:1;
hence  f is_differentiable_in x0 by A13, Def4; ::_thesis: verum
end;
hence A14: f is_differentiable_on Z by A6, Th9; ::_thesis: for x being Real st x in Z holds
(f `| Z) . x = 1
let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) . x0 = 1 )
assume A15: x0 in Z ; ::_thesis: (f `| Z) . x0 = 1
then consider N1 being Neighbourhood of x0 such that
A16: N1 c= Z by RCOMP_1:18;
A17: f is_differentiable_in x0 by A10, A15;
then  ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Def4;
then consider N being Neighbourhood of x0 such that
A18: N c= dom f ;
consider N2 being Neighbourhood of x0 such that
A19: N2 c= N1 and
A20: N2 c= N by RCOMP_1:17;
A21: N2 c= dom f by A18, A20, XBOOLE_1:1;
A22: for x being Real st x in N2 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
proof
let x be Real; ::_thesis: ( x in N2 implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume  x in N2 ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then  x in N1 by A19;
hence (f . x) - (f . x0) = x - (f . x0) by A8, A16
.= x - x0 by A8, A15
.= (L . (x - x0)) + 0 by FUNCT_1:18
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
thus (f `| Z) . x0 = diff (f,x0) by A14, A15, Def7
.= L . 1 by A17, A21, A22, Def5
.= 1 by FUNCT_1:18 ; ::_thesis: verum
end;

theorem :: FDIFF_1:18
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL 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 Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_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, Th9;
hence  f1 + f2 is_differentiable_in x0 by Th13; ::_thesis: verum
end;
hence A3: f1 + f2 is_differentiable_on Z by A1, Th9; ::_thesis: for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
now__::_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, Th9;
thus ((f1 + f2) `| Z) . x = diff ((f1 + f2),x) by A3, A4, Def7
.= (diff (f1,x)) + (diff (f2,x)) by A5, Th13 ; ::_thesis: verum
end;
hence  for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ; ::_thesis: verum
end;

theorem :: FDIFF_1:19
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL 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 Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_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, Th9;
hence  f1 - f2 is_differentiable_in x0 by Th14; ::_thesis: verum
end;
hence A3: f1 - f2 is_differentiable_on Z by A1, Th9; ::_thesis: for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x))
now__::_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, Th9;
thus ((f1 - f2) `| Z) . x = diff ((f1 - f2),x) by A3, A4, Def7
.= (diff (f1,x)) - (diff (f2,x)) by A5, Th14 ; ::_thesis: verum
end;
hence  for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ; ::_thesis: verum
end;

theorem :: FDIFF_1:20
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL 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 r be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL 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,REAL 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,REAL; ::_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, Th9;
hence  r (#) f is_differentiable_in x0 by Th15; ::_thesis: verum
end;
hence A3: r (#) f is_differentiable_on Z by A1, Th9; ::_thesis: for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x))
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((r_(#)_f)_`|_Z)_._x_=_r_*_(diff_(f,x))
let x be Real; ::_thesis: ( x in Z implies ((r (#) f) `| Z) . x = r * (diff (f,x)) )
assume A4: x in Z ; ::_thesis: ((r (#) f) `| Z) . x = r * (diff (f,x))
then A5: f is_differentiable_in x by A2, Th9;
thus ((r (#) f) `| Z) . x = diff ((r (#) f),x) by A3, A4, Def7
.= r * (diff (f,x)) by A5, Th15 ; ::_thesis: verum
end;
hence  for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ; ::_thesis: verum
end;

theorem :: FDIFF_1:21
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL 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 = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) ) )
proof
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL 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 = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_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 = ((f2 . x) * (diff (f1,x))) + ((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 = ((f2 . x) * (diff (f1,x))) + ((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, Th9;
hence  f1 (#) f2 is_differentiable_in x0 by Th16; ::_thesis: verum
end;
hence A3: f1 (#) f2 is_differentiable_on Z by A1, Th9; ::_thesis: for x being Real st x in Z holds
((f1 (#) f2) `| Z) . x = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x)))
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((f1_(#)_f2)_`|_Z)_._x_=_((f2_._x)_*_(diff_(f1,x)))_+_((f1_._x)_*_(diff_(f2,x)))
let x be Real; ::_thesis: ( x in Z implies ((f1 (#) f2) `| Z) . x = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) )
assume A4: x in Z ; ::_thesis: ((f1 (#) f2) `| Z) . x = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x)))
then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th9;
thus ((f1 (#) f2) `| Z) . x = diff ((f1 (#) f2),x) by A3, A4, Def7
.= ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) by A5, Th16 ; ::_thesis: verum
end;
hence  for x being Real st x in Z holds
((f1 (#) f2) `| Z) . x = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) ; ::_thesis: verum
end;

theorem :: FDIFF_1:22
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & f | Z is V8() holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
proof
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom f & f | Z is V8() holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom f & f | Z is V8() implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) ) )
set R = cf;
A1: dom cf = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )
A2: now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0
A3: rng h c= dom cf by A1;
A4: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A4, A3, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
::_thesis: verum
end;
then A5: (h ") (#) (cf /* h) is V8() by VALUED_0:def_18;
hence  (h ") (#) (cf /* h) is convergent ; ::_thesis: lim ((h ") (#) (cf /* h)) = 0
 ((h ") (#) (cf /* h)) . 0 = 0 by A2;
hence  lim ((h ") (#) (cf /* h)) = 0 by A5, SEQ_4:25; ::_thesis: verum
end;
then reconsider R = cf as RestFunc by Def2;
set L = cf;
 for p being Real holds cf . p = 0 * p by FUNCOP_1:7;
then reconsider L = cf as LinearFunc by Def3;
assume that
A6: Z c= dom f and
A7: f | Z is V8() ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
consider r being Real such that
A8: for x being Real st x in Z /\ (dom f) holds
f . x = r by A7, PARTFUN2:57;
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 A6, A11, XBOOLE_1:1;
A13: x0 in Z /\ (dom f) by A6, 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)) )
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 A8
.= r - r by A8, A13
.= (L . (x - x0)) + 0 by FUNCOP_1:7
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
hence  f is_differentiable_in x0 by A12, Def4; ::_thesis: verum
end;
hence A14: f is_differentiable_on Z by A6, Th9; ::_thesis: for x being Real st x in Z holds
(f `| Z) . x = 0
let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) . x0 = 0 )
assume A15: x0 in Z ; ::_thesis: (f `| Z) . x0 = 0
then consider N being Neighbourhood of x0 such that
A16: N c= Z by RCOMP_1:18;
A17: N c= dom f by A6, A16, XBOOLE_1:1;
A18: x0 in Z /\ (dom f) by A6, A15, XBOOLE_0:def_4;
A19: 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)) )
assume  x in N ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then  x in Z /\ (dom f) by A16, A17, XBOOLE_0:def_4;
hence (f . x) - (f . x0) = r - (f . x0) by A8
.= r - r by A8, A18
.= (L . (x - x0)) + 0 by FUNCOP_1:7
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
A20: f is_differentiable_in x0 by A9, A15;
thus (f `| Z) . x0 = diff (f,x0) by A14, A15, Def7
.= L . 1 by A20, A17, A19, Def5
.= 0 by FUNCOP_1:7 ; ::_thesis: verum
end;

theorem :: FDIFF_1:23
for r, p being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
proof
let r, p be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) ) )
set R = cf;
defpred S1[ set ] means $1 in REAL ;
A1: dom cf = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )
A2: now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0
A3: rng h c= dom cf by A1;
A4: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A4, A3, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
::_thesis: verum
end;
then A5: (h ") (#) (cf /* h) is V8() by VALUED_0:def_18;
hence  (h ") (#) (cf /* h) is convergent ; ::_thesis: lim ((h ") (#) (cf /* h)) = 0
 ((h ") (#) (cf /* h)) . 0 = 0 by A2;
hence  lim ((h ") (#) (cf /* h)) = 0 by A5, SEQ_4:25; ::_thesis: verum
end;
then reconsider R = cf as RestFunc by Def2;
assume that
A6: Z c= dom f and
A7: for x being Real st x in Z holds
f . x = (r * x) + 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 REAL = r * $1;
consider L being PartFunc of REAL,REAL such that
A8: ( ( 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 A8, Th1;
then A9: L is total by PARTFUN1:def_2;
A10: now__::_thesis:_for_x_being_Real_holds_L_._x_=_r_*_x
let x be Real; ::_thesis: L . x = r * x
thus  L . x = r * x by A8; ::_thesis: verum
end;
then reconsider L = L as LinearFunc by A9, Def3;
A11: 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 A12: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A13: N c= Z by RCOMP_1:18;
A14: 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)) )
assume  x in N ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
hence (f . x) - (f . x0) = ((r * x) + p) - (f . x0) by A7, A13
.= ((r * x) + p) - ((r * x0) + p) by A7, A12
.= (r * (x - x0)) + 0
.= (L . (x - x0)) + 0 by A10
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
 N c= dom f by A6, A13, XBOOLE_1:1;
hence  f is_differentiable_in x0 by A14, Def4; ::_thesis: verum
end;
hence A15: f is_differentiable_on Z by A6, Th9; ::_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 A16: x0 in Z ; ::_thesis: (f `| Z) . x0 = r
then consider N being Neighbourhood of x0 such that
A17: N c= Z by RCOMP_1:18;
A18: 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)) )
assume  x in N ; ::_thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
hence (f . x) - (f . x0) = ((r * x) + p) - (f . x0) by A7, A17
.= ((r * x) + p) - ((r * x0) + p) by A7, A16
.= (r * (x - x0)) + 0
.= (L . (x - x0)) + 0 by A10
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
A19: N c= dom f by A6, A17, XBOOLE_1:1;
A20: f is_differentiable_in x0 by A11, A16;
thus (f `| Z) . x0 = diff (f,x0) by A15, A16, Def7
.= L . 1 by A20, A19, A18, Def5
.= r * 1 by A10
.= r ; ::_thesis: verum
end;

theorem Th24: :: FDIFF_1:24
for f being PartFunc of REAL,REAL
for x0 being real number st f is_differentiable_in x0 holds
f is_continuous_in x0
proof
let f be PartFunc of REAL,REAL; ::_thesis: for x0 being real number st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be real number ; ::_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 ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by Def4;
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
A3: 0 < g and
A4: N = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
 x0 in REAL by XREAL_0:def_1;
then reconsider s2 = NAT --> x0 as Real_Sequence by FUNCOP_1:45;
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
A5: rng s1 c= dom f and
A6: s1 is convergent and
A7: lim s1 = x0 and
A8: 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
A9: for m being Element of NAT st l <= m holds
abs ((s1 . m) - x0) < g by A6, A7, A3, SEQ_2:def_7;
reconsider c = s2 ^\ l as V8() Real_Sequence ;
deffunc H1( Real) ->  Element of REAL = (s1 . $1) - (s2 . $1);
consider s3 being Real_Sequence such that
A10: for n being Element of NAT holds s3 . n = H1(n) from SEQ_1:sch_1();
A11: s3 = s1 - s2 by A10, RFUNCT_2:1;
then A12: s3 is convergent by A6, SEQ_2:11;
A13: 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
A14: y = (s2 ^\ l) . n by FUNCT_2:113;
 y = s2 . (n + l) by A14, 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 A15: y = x0 by TARSKI:def_1;
c . 0 = s2 . (0 + l) by NAT_1:def_3
.= y by A15, FUNCOP_1:7 ;
hence  y in rng c by VALUED_0:28; ::_thesis: verum
end;
A16: 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_
abs_(((f_/*_c)_._m)_-_(f_._x0))_<_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
abs (((f /* c) . m) - (f . x0)) < p )
assume A17: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((f /* c) . m) - (f . x0)) < p )
assume  n <= m ; ::_thesis: abs (((f /* c) . m) - (f . x0)) < p
 x0 in N by RCOMP_1:16;
then  rng c c= dom f by A2, A13, ZFMISC_1:31;
then  abs (((f /* c) . m) - (f . x0)) = abs ((f . (c . m)) - (f . x0)) by FUNCT_2:108
.= abs ((f . (s2 . (m + l))) - (f . x0)) by NAT_1:def_3
.= abs ((f . x0) - (f . x0)) by FUNCOP_1:7
.= 0 by ABSVALUE:2 ;
hence  abs (((f /* c) . m) - (f . x0)) < p by A17; ::_thesis: verum
end;
then A18: f /* c is convergent by SEQ_2:def_6;
lim s2 = s2 . 0 by SEQ_4:26
.= x0 by FUNCOP_1:7 ;
then  lim s3 = x0 - x0 by A6, A7, A11, SEQ_2:12
.= 0 ;
then A19: lim (s3 ^\ l) = 0 by A12, SEQ_4:20;
A20: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s3_._n_=_0
given n being Element of NAT  such that A21: s3 . n = 0 ; ::_thesis: contradiction
 (s1 . n) - (s2 . n) = 0 by A10, A21;
hence  contradiction by A8, FUNCOP_1:7; ::_thesis: verum
end;
A22: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(s3_^\_l)_._n_=_0
given n being Element of NAT  such that A23: (s3 ^\ l) . n = 0 ; ::_thesis: contradiction
 s3 . (n + l) = 0 by A23, NAT_1:def_3;
hence  contradiction by A20; ::_thesis: verum
end;
 s3 ^\ l is 0 -convergent by A12, A19, Def1;
then reconsider h = s3 ^\ l as non-zero 0 -convergent Real_Sequence by A22, SEQ_1:5;
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 SEQ_1:7
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by RFUNCT_2:1
.= (f /* (h + c)) . n ; ::_thesis: verum
end;
then A24: ((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 A11, 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 A25: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A24, FUNCT_2:63
.= (f /* s1) ^\ l by A5, VALUED_0:27 ;
 rng (h + c) c= N
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in N )
assume  y in rng (h + c) ; ::_thesis: y in N
then consider n being Element of NAT  such that
A26: y = (h + c) . n by FUNCT_2:113;
(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A11, 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 A9, NAT_1:12;
hence  y in N by A4, A26, RCOMP_1:1; ::_thesis: verum
end;
then A27: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A2, A13, Th12;
then A28: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A19, SEQ_2:15
.= 0 ;
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
A29: h . n <> 0 by A22;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by SEQ_1:8
.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by SEQ_1:8
.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10
.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n)
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A29, XCMPLX_0:def_7
.= ((f /* (h + c)) - (f /* c)) . n ; ::_thesis: verum
end;
then A30: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63;
then A31: (f /* (h + c)) - (f /* c) is convergent by A27, SEQ_2:14;
then A32: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A18, SEQ_2:5;
hence  f /* s1 is convergent by A25, SEQ_4:21; ::_thesis: f . x0 = lim (f /* s1)
 lim (f /* c) = f . x0 by A16, A18, SEQ_2:def_7;
then  lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0 + (f . x0) by A28, A30, A31, A18, SEQ_2:6
.= f . x0 ;
hence  f . x0 = lim (f /* s1) by A32, A25, SEQ_4:22; ::_thesis: verum
end;
hence  f is_continuous_in x0 by FCONT_1:2; ::_thesis: verum
end;

theorem :: FDIFF_1:25
for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on X implies f | X is continuous )
assume A1: f is_differentiable_on X ; ::_thesis: f | X is continuous
let x be real number ; :: according to FCONT_1:def_2 ::_thesis: ( not x in dom (f | X) or 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  f | X is_differentiable_in x by A1, Def6;
hence  f | X is_continuous_in x by Th24; ::_thesis: verum
end;

theorem Th26: :: FDIFF_1:26
for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
proof
let X be set ; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of REAL,REAL; ::_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, Def6;
hence  Z c= dom f by A2, XBOOLE_1:1; :: according to FDIFF_1:def_6 ::_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 A3: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0
then  f | X is_differentiable_in x0 by A1, A2, Def6;
then consider N being Neighbourhood of x0 such that
A4: N c= dom (f | X) and
A5: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((f | X) . x) - ((f | X) . x0) = (L . (x - x0)) + (R . (x - x0)) by Def4;
consider N1 being Neighbourhood of x0 such that
A6: N1 c= Z by A3, RCOMP_1:18;
consider N2 being Neighbourhood of x0 such that
A7: N2 c= N and
A8: N2 c= N1 by RCOMP_1:17;
A9: N2 c= Z by A6, A8, XBOOLE_1:1;
take  N2 ; :: according to FDIFF_1:def_4 ::_thesis: ( N2 c= dom (f | Z) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
 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 A4, XBOOLE_1:1;
then  N2 c= dom f by A7, XBOOLE_1:1;
then  N2 c= (dom f) /\ Z by A9, XBOOLE_1:19;
hence A10: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being LinearFunc ex R being RestFunc 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, R being RestFunc such that
A11: for x being Real st x in N holds
((f | X) . x) - ((f | X) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
take  L ; ::_thesis: ex R being RestFunc 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))
let x be Real; ::_thesis: ( x in N2 implies ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A12: x in N2 ; ::_thesis: ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
then  ((f | X) . x) - ((f | X) . x0) = (L . (x - x0)) + (R . (x - x0)) by A7, A11;
then A13: ((f | X) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, A3, FUNCT_1:49;
 x in N by A7, A12;
then  (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A4, A13, FUNCT_1:47;
then  (f . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3, FUNCT_1:49;
hence  ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A12, FUNCT_1:47; ::_thesis: verum
end;

theorem :: FDIFF_1:27
ex R being RestFunc st
( R . 0 = 0 & R is_continuous_in 0 )
proof
A1: {} REAL is closed
proof
let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not K87(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 by XBOOLE_1:3; ::_thesis: verum
end;
 ( ([#] REAL) ` = {} REAL & REAL c= REAL & [#] REAL = REAL ) by XBOOLE_1:37;
then reconsider Z = [#] REAL as open Subset of REAL by A1, RCOMP_1:def_5;
set R = cf;
reconsider f = cf as PartFunc of REAL,REAL ;
A2: dom cf = REAL by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0_)
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )
A3: now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0
A4: rng h c= dom cf by A2;
A5: n in NAT by ORDINAL1:def_12;
hence ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A5, A4, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
::_thesis: verum
end;
then A6: (h ") (#) (cf /* h) is V8() by VALUED_0:def_18;
hence  (h ") (#) (cf /* h) is convergent ; ::_thesis: lim ((h ") (#) (cf /* h)) = 0
 ((h ") (#) (cf /* h)) . 0 = 0 by A3;
hence  lim ((h ") (#) (cf /* h)) = 0 by A6, SEQ_4:25; ::_thesis: verum
end;
then reconsider R = cf as RestFunc by Def2;
set L = cf;
 for p being Real holds cf . p = 0 * p by FUNCOP_1:7;
then reconsider L = cf as LinearFunc by Def3;
 f | Z is V8() ;
then consider r being Real such that
A7: for x being Real st x in Z /\ (dom f) holds
f . x = r by PARTFUN2:57;
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  x0 in Z ; ::_thesis: f is_differentiable_in x0
set N = the Neighbourhood of x0;
A9: the Neighbourhood of x0 c= dom f by A2;
A10: x0 in Z /\ (dom f) by A2;
 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)) )
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 A9, XBOOLE_0:def_4;
hence (f . x) - (f . x0) = r - (f . x0) by A7
.= r - r by A7, A10
.= (L . (x - x0)) + 0 by FUNCOP_1:7
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
hence  f is_differentiable_in x0 by A9, Def4; ::_thesis: verum
end;
set x0 = the Real;
 f is_differentiable_in the Real by A8;
then consider N being Neighbourhood of the Real such that
 N c= dom f and
A11: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . the Real) = (L . (x - the Real)) + (R . (x - the Real)) by Def4;
consider L being LinearFunc, R being RestFunc such that
A12: for x being Real st x in N holds
(f . x) - (f . the Real) = (L . (x - the Real)) + (R . (x - the Real)) by A11;
take  R ; ::_thesis: ( R . 0 = 0 & R is_continuous_in 0 )
consider p being Real such that
A13: for r being Real holds L . r = p * r by Def3;
 (f . the Real) - (f . the Real) = (L . ( the Real - the Real)) + (R . ( the Real - the Real)) by A12, RCOMP_1:16;
then A14: 0 = (p * 0) + (R . 0) by A13;
hence  R . 0 = 0 ; ::_thesis: R is_continuous_in 0
A15: 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 )
A16: cs . 1 = 0 by FUNCOP_1:7;
 (h ") (#) (R /* h) is convergent by Def2;
then  (h ") (#) (R /* h) is bounded by SEQ_2:13;
then consider M being real number  such that
 M > 0 and
A17: for n being Element of NAT holds abs (((h ") (#) (R /* h)) . n) < M by SEQ_2:3;
A18: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_cs_._n_<=_(abs_(R_/*_h))_._n_&_(abs_(R_/*_h))_._n_<=_(M_(#)_(abs_h))_._n_)
let n be Element of NAT ; ::_thesis: ( cs . n <= (abs (R /* h)) . n & (abs (R /* h)) . n <= (M (#) (abs h)) . n )
abs (((h ") (#) (R /* h)) . n) = abs (((h ") . n) * ((R /* h) . n)) by SEQ_1:8
.= abs (((h . n) ") * ((R /* h) . n)) by VALUED_1:10 ;
then A19: abs (((h . n) ") * ((R /* h) . n)) <= M by A17;
 0 <= abs ((R /* h) . n) by COMPLEX1:46;
then  0 <= (abs (R /* h)) . n by SEQ_1:12;
hence  cs . n <= (abs (R /* h)) . n by FUNCOP_1:7; ::_thesis: (abs (R /* h)) . n <= (M (#) (abs h)) . n
 abs (h . n) >= 0 by COMPLEX1:46;
then  (abs (h . n)) * (abs (((h . n) ") * ((R /* h) . n))) <= M * (abs (h . n)) by A19, XREAL_1:64;
then  abs ((h . n) * (((h . n) ") * ((R /* h) . n))) <= M * (abs (h . n)) by COMPLEX1:65;
then A20: abs (((h . n) * ((h . n) ")) * ((R /* h) . n)) <= M * (abs (h . n)) ;
 h . n <> 0 by SEQ_1:5;
then  abs (1 * ((R /* h) . n)) <= M * (abs (h . n)) by A20, XCMPLX_0:def_7;
then  abs ((R /* h) . n) <= M * ((abs h) . n) by SEQ_1:12;
then  abs ((R /* h) . n) <= (M (#) (abs h)) . n by SEQ_1:9;
hence  (abs (R /* h)) . n <= (M (#) (abs h)) . n by SEQ_1:12; ::_thesis: verum
end;
 lim h = 0 ;
then  lim (abs h) = abs 0 by SEQ_4:14
.= 0 by ABSVALUE:2 ;
then A21: lim (M (#) (abs h)) = M * 0 by SEQ_2:8
.= lim cs by A16, SEQ_4:25 ;
A22: M (#) (abs h) is convergent by SEQ_2:7;
then A23: abs (R /* h) is convergent by A21, A18, SEQ_2:19;
 lim cs = 0 by A16, SEQ_4:25;
then  lim (abs (R /* h)) = 0 by A22, A21, A18, SEQ_2:20;
hence  ( R /* h is convergent & lim (R /* h) = R . 0 ) by A14, A23, SEQ_4:15; ::_thesis: verum
end;
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_&_lim_(R_/*_s1)_=_R_._0_)
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 & lim (R /* s1) = R . 0 ) )
assume that
 rng s1 c= dom R and
A24: ( s1 is convergent & lim s1 = 0 ) and
A25: for n being Element of NAT holds s1 . n <> 0 ; ::_thesis: ( R /* s1 is convergent & lim (R /* s1) = R . 0 )
 s1 is 0 -convergent by A24, Def1;
then  s1 is non-zero 0 -convergent Real_Sequence by SEQ_1:5, A25;
hence  ( R /* s1 is convergent & lim (R /* s1) = R . 0 ) by A15; ::_thesis: verum
end;
hence  R is_continuous_in 0 by FCONT_1:2; ::_thesis: verum
end;

definition
let f be PartFunc of REAL,REAL;
attrf is differentiable  means :Def8: :: FDIFF_1:def 8
f is_differentiable_on dom f;
end;

:: deftheorem Def8 defines differentiable FDIFF_1:def_8_:_
 for f being PartFunc of REAL,REAL holds
( f is differentiable iff f is_differentiable_on dom f );

Lm1:  {} REAL is closed
proof
let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not K87(a) c= {} REAL or not a is convergent or lim a in {} REAL )
assume that
A1: rng a c= {} REAL and
 a is convergent ; ::_thesis: lim a in {} REAL
 rng a = {} by A1, XBOOLE_1:3;
hence  lim a in {} REAL ; ::_thesis: verum
end;

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
clusterV1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued differentiable for Element of K19(K20(REAL,REAL));
existence
 ex b1 being Function of REAL,REAL st b1 is differentiable
proof
reconsider Z = REAL as open Subset of REAL by Lm2;
reconsider f = id REAL as Function of REAL,REAL ;
take  f ; ::_thesis: f is differentiable
A1: Z = dom f by FUNCT_2:def_1;
then  f | Z = id Z by RELAT_1:68;
then  f is_differentiable_on Z by A1, Th17;
hence  f is differentiable by A1, Def8; ::_thesis: verum
end;
end;

theorem :: FDIFF_1:28
for Z being open Subset of REAL
for f being differentiable PartFunc of REAL,REAL st Z c= dom f holds
f is_differentiable_on Z
proof
let Z be open Subset of REAL; ::_thesis: for f being differentiable PartFunc of REAL,REAL st Z c= dom f holds
f is_differentiable_on Z
let f be differentiable PartFunc of REAL,REAL; ::_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 Def8;
hence  f is_differentiable_on Z by A1, Th26; ::_thesis: verum
end;