:: 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;