:: NDIFF_3 semantic presentation begin reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:45; theorem Th1: :: NDIFF_3:1 for G being RealNormSpace for s1 being Real_Sequence for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds ( seq is convergent & lim seq = 0. G ) proof let G be RealNormSpace; ::_thesis: for s1 being Real_Sequence for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds ( seq is convergent & lim seq = 0. G ) let s1 be Real_Sequence; ::_thesis: for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 holds ( seq is convergent & lim seq = 0. G ) let seq be sequence of G; ::_thesis: ( ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) & s1 is convergent & lim s1 = 0 implies ( seq is convergent & lim seq = 0. G ) ) assume that A1: for n being Element of NAT holds ||.(seq . n).|| <= s1 . n and A2: s1 is convergent and A3: lim s1 = 0 ; ::_thesis: ( seq is convergent & lim seq = 0. G ) now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(0._G)).||_<_p let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. G)).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. G)).|| < p then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds abs ((s1 . m) - 0) < p by A2, A3, SEQ_2:def_7; now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(0._G)).||_<_p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (0. G)).|| < p ) assume n <= m ; ::_thesis: ||.((seq . m) - (0. G)).|| < p then A5: abs ((s1 . m) - 0) < p by A4; A6: ||.((seq . m) - (0. G)).|| = ||.(seq . m).|| by RLVECT_1:13; A7: s1 . m <= abs (s1 . m) by ABSVALUE:4; ||.(seq . m).|| <= s1 . m by A1; then ||.((seq . m) - (0. G)).|| <= abs (s1 . m) by A6, A7, XXREAL_0:2; hence ||.((seq . m) - (0. G)).|| < p by A5, XXREAL_0:2; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. G)).|| < p ; ::_thesis: verum end; then A8: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. G)).|| < p ; hence seq is convergent by NORMSP_1:def_6; ::_thesis: lim seq = 0. G hence lim seq = 0. G by A8, NORMSP_1:def_7; ::_thesis: verum end; theorem Th2: :: NDIFF_3:2 for G being RealNormSpace for k being Element of NAT for s1 being Real_Sequence for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k proof let G be RealNormSpace; ::_thesis: for k being Element of NAT for s1 being Real_Sequence for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k let k be Element of NAT ; ::_thesis: for s1 being Real_Sequence for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k let s1 be Real_Sequence; ::_thesis: for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k let seq be sequence of G; ::_thesis: (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k now__::_thesis:_for_n_being_Element_of_NAT_holds_((s1_(#)_seq)_^\_k)_._n_=_((s1_^\_k)_(#)_(seq_^\_k))_._n let n be Element of NAT ; ::_thesis: ((s1 (#) seq) ^\ k) . n = ((s1 ^\ k) (#) (seq ^\ k)) . n thus ((s1 (#) seq) ^\ k) . n = (s1 (#) seq) . (n + k) by NAT_1:def_3 .= (s1 . (n + k)) * (seq . (n + k)) by NDIFF_1:def_2 .= ((s1 ^\ k) . n) * (seq . (n + k)) by NAT_1:def_3 .= ((s1 ^\ k) . n) * ((seq ^\ k) . n) by NAT_1:def_3 .= ((s1 ^\ k) (#) (seq ^\ k)) . n by NDIFF_1:def_2 ; ::_thesis: verum end; hence (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k by FUNCT_2:63; ::_thesis: verum end; definition let F be non trivial RealNormSpace; let IT be PartFunc of REAL, the carrier of F; attrIT is RestFunc-like means :Def1: :: NDIFF_3:def 1 ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) ); end; :: deftheorem Def1 defines RestFunc-like NDIFF_3:def_1_:_ for F being non trivial RealNormSpace for IT being PartFunc of REAL, the carrier of F holds ( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) ) ); registration let F be non trivial RealNormSpace; clusterV13() V16( REAL ) V17( the carrier of F) Function-like RestFunc-like for Element of K6(K7(REAL, the carrier of F)); existence ex b1 being PartFunc of REAL, the carrier of F st b1 is RestFunc-like proof take f = REAL --> (0. F); ::_thesis: f is RestFunc-like thus f is total ; :: according to NDIFF_3:def_1 ::_thesis: for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) A1: dom f = REAL by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_(f_/*_h)_is_convergent_&_lim_((h_")_(#)_(f_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(f_/*_h))_._n_=_0._F let n be Nat; ::_thesis: ((h ") (#) (f /* h)) . n = 0. F A2: rng h c= dom f by A1; A3: n in NAT by ORDINAL1:def_12; hence ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by NDIFF_1:def_2 .= ((h ") . n) * (f . (h . n)) by A3, A2, FUNCT_2:108 .= 0. F by FUNCOP_1:7, RLVECT_1:10 ; ::_thesis: verum end; then ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0. F ) by VALUED_0:def_18; hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum end; hence for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) ; ::_thesis: verum end; end; definition let F be non trivial RealNormSpace; mode RestFunc of F is RestFunc-like PartFunc of REAL, the carrier of F; end; definition let F be non trivial RealNormSpace; let IT be Function of REAL, the carrier of F; attrIT is linear means :Def2: :: NDIFF_3:def 2 ex r being Point of F st for p being Real holds IT . p = p * r; end; :: deftheorem Def2 defines linear NDIFF_3:def_2_:_ for F being non trivial RealNormSpace for IT being Function of REAL, the carrier of F holds ( IT is linear iff ex r being Point of F st for p being Real holds IT . p = p * r ); registration let F be non trivial RealNormSpace; clusterV1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total linear for Element of K6(K7(REAL, the carrier of F)); existence ex b1 being Function of REAL, the carrier of F st b1 is linear proof deffunc H1( Element of REAL ) -> Element of the carrier of F = F * (0. F); consider f being Function of REAL, the carrier of F such that A1: for x being Element of REAL holds f . x = H1(x) from FUNCT_2:sch_4(); take f ; ::_thesis: f is linear thus f is linear by Def2, A1; ::_thesis: verum end; end; definition let F be non trivial RealNormSpace; mode LinearFunc of F is linear Function of REAL, the carrier of F; end; theorem Th3: :: NDIFF_3:3 for F being non trivial RealNormSpace for L1, L2 being LinearFunc of F holds ( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F ) proof let F be non trivial RealNormSpace; ::_thesis: for L1, L2 being LinearFunc of F holds ( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F ) let L1, L2 be LinearFunc of F; ::_thesis: ( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F ) consider g1 being Point of F such that A1: for p being Real holds L1 . p = p * g1 by Def2; consider g2 being Point of F such that A2: for p being Real holds L2 . p = p * g2 by Def2; A3: L1 + L2 is total by VFUNCT_1:32; then A4: dom (L1 + L2) = REAL by FUNCT_2:def_1; now__::_thesis:_for_p_being_Real_holds_(L1_+_L2)_._p_=_p_*_(g1_+_g2) let p be Real; ::_thesis: (L1 + L2) . p = p * (g1 + g2) thus (L1 + L2) . p = (L1 + L2) /. p by A4, PARTFUN1:def_6 .= (L1 /. p) + (L2 /. p) by VFUNCT_1:37 .= (p * g1) + (L2 . p) by A1 .= (p * g1) + (p * g2) by A2 .= p * (g1 + g2) by RLVECT_1:def_5 ; ::_thesis: verum end; hence L1 + L2 is LinearFunc of F by A3, Def2; ::_thesis: L1 - L2 is LinearFunc of F A5: L1 - L2 is total by VFUNCT_1:32; then A6: dom (L1 - L2) = REAL by FUNCT_2:def_1; now__::_thesis:_for_p_being_Real_holds_(L1_-_L2)_._p_=_p_*_(g1_-_g2) let p be Real; ::_thesis: (L1 - L2) . p = p * (g1 - g2) thus (L1 - L2) . p = (L1 - L2) /. p by A6, PARTFUN1:def_6 .= (L1 /. p) - (L2 /. p) by VFUNCT_1:37 .= (p * g1) - (L2 . p) by A1 .= (p * g1) - (p * g2) by A2 .= p * (g1 - g2) by RLVECT_1:34 ; ::_thesis: verum end; hence L1 - L2 is LinearFunc of F by A5, Def2; ::_thesis: verum end; theorem Th4: :: NDIFF_3:4 for F being non trivial RealNormSpace for r being Real for L being LinearFunc of F holds r (#) L is LinearFunc of F proof let F be non trivial RealNormSpace; ::_thesis: for r being Real for L being LinearFunc of F holds r (#) L is LinearFunc of F let r be Real; ::_thesis: for L being LinearFunc of F holds r (#) L is LinearFunc of F let L be LinearFunc of F; ::_thesis: r (#) L is LinearFunc of F consider g being Point of F such that A1: for p being Real holds L . p = p * g by Def2; A2: r (#) L is total by VFUNCT_1:34; then A3: dom (r (#) L) = REAL by FUNCT_2:def_1; now__::_thesis:_for_p_being_Real_holds_(r_(#)_L)_._p_=_p_*_(r_*_g) let p be Real; ::_thesis: (r (#) L) . p = p * (r * g) thus (r (#) L) . p = (r (#) L) /. p by A3, PARTFUN1:def_6 .= r * (L /. p) by VFUNCT_1:39 .= r * (p * g) by A1 .= (r * p) * g by RLVECT_1:def_7 .= p * (r * g) by RLVECT_1:def_7 ; ::_thesis: verum end; hence r (#) L is LinearFunc of F by A2, Def2; ::_thesis: verum end; theorem Th5: :: NDIFF_3:5 for F being non trivial RealNormSpace for h1, h2 being PartFunc of REAL, the carrier of F for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) proof let F be non trivial RealNormSpace; ::_thesis: for h1, h2 being PartFunc of REAL, the carrier of F for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) let h1, h2 be PartFunc of REAL, the carrier of F; ::_thesis: for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) let seq be Real_Sequence; ::_thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) ) A1: (dom h1) /\ (dom h2) c= dom h1 by XBOOLE_1:17; A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17; assume A3: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) then A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def_1; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_+_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_+_((h2_/*_seq)_._n) let n be Element of NAT ; ::_thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n) A5: seq . n in rng seq by FUNCT_2:4; thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A4, FUNCT_2:109 .= (h1 /. (seq . n)) + (h2 /. (seq . n)) by A4, A5, VFUNCT_1:def_1 .= ((h1 /* seq) . n) + (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum end; hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NORMSP_1:def_2; ::_thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) A6: rng seq c= dom (h1 - h2) by A3, VFUNCT_1:def_2; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_-_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_-_((h2_/*_seq)_._n) let n be Element of NAT ; ::_thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n) A7: seq . n in rng seq by FUNCT_2:4; thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A6, FUNCT_2:109 .= (h1 /. (seq . n)) - (h2 /. (seq . n)) by A6, A7, VFUNCT_1:def_2 .= ((h1 /* seq) . n) - (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum end; hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by NORMSP_1:def_3; ::_thesis: verum end; theorem Th6: :: NDIFF_3:6 for F being non trivial RealNormSpace for h1, h2 being PartFunc of REAL, the carrier of F for seq being Real_Sequence st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) proof let F be non trivial RealNormSpace; ::_thesis: for h1, h2 being PartFunc of REAL, the carrier of F for seq being Real_Sequence st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) let h1, h2 be PartFunc of REAL, the carrier of F; ::_thesis: for seq being Real_Sequence st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) let seq be Real_Sequence; ::_thesis: ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) ) assume ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) then h1 + h2 is total by VFUNCT_1:32; then dom (h1 + h2) = REAL by PARTFUN1:def_2; then (dom h1) /\ (dom h2) = REAL by VFUNCT_1:def_1; then A1: rng seq c= (dom h1) /\ (dom h2) ; hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by Th5; ::_thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, Th5; ::_thesis: verum end; theorem Th7: :: NDIFF_3:7 for F being non trivial RealNormSpace for R1, R2 being RestFunc of F holds ( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F ) proof let F be non trivial RealNormSpace; ::_thesis: for R1, R2 being RestFunc of F holds ( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F ) let R1, R2 be RestFunc of F; ::_thesis: ( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F ) A1: ( R1 is total & R2 is total ) by Def1; A2: now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((R1_+_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_+_R2)_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R1 + R2) /* h) is convergent & lim ((h ") (#) ((R1 + R2) /* h)) = 0. F ) A3: (h ") (#) ((R1 + R2) /* h) = (h ") (#) ((R1 /* h) + (R2 /* h)) by A1, Th6 .= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by NDIFF_1:9 ; A4: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def1; hence (h ") (#) ((R1 + R2) /* h) is convergent by A3, NORMSP_1:19; ::_thesis: lim ((h ") (#) ((R1 + R2) /* h)) = 0. F ( lim ((h ") (#) (R1 /* h)) = 0. F & lim ((h ") (#) (R2 /* h)) = 0. F ) by Def1; hence lim ((h ") (#) ((R1 + R2) /* h)) = (0. F) + (0. F) by A4, A3, NORMSP_1:25 .= 0. F by RLVECT_1:def_4 ; ::_thesis: verum end; R1 + R2 is total by A1, VFUNCT_1:32; hence R1 + R2 is RestFunc of F by A2, Def1; ::_thesis: R1 - R2 is RestFunc of F A5: now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((R1_-_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_-_R2)_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((R1 - R2) /* h) is convergent & lim ((h ") (#) ((R1 - R2) /* h)) = 0. F ) A6: (h ") (#) ((R1 - R2) /* h) = (h ") (#) ((R1 /* h) - (R2 /* h)) by A1, Th6 .= ((h ") (#) (R1 /* h)) - ((h ") (#) (R2 /* h)) by NDIFF_1:12 ; A7: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def1; hence (h ") (#) ((R1 - R2) /* h) is convergent by A6, NORMSP_1:20; ::_thesis: lim ((h ") (#) ((R1 - R2) /* h)) = 0. F ( lim ((h ") (#) (R1 /* h)) = 0. F & lim ((h ") (#) (R2 /* h)) = 0. F ) by Def1; hence lim ((h ") (#) ((R1 - R2) /* h)) = (0. F) - (0. F) by A7, A6, NORMSP_1:26 .= 0. F by RLVECT_1:13 ; ::_thesis: verum end; R1 - R2 is total by A1, VFUNCT_1:32; hence R1 - R2 is RestFunc of F by A5, Def1; ::_thesis: verum end; theorem Th8: :: NDIFF_3:8 for F being non trivial RealNormSpace for r being Real for R being RestFunc of F holds r (#) R is RestFunc of F proof let F be non trivial RealNormSpace; ::_thesis: for r being Real for R being RestFunc of F holds r (#) R is RestFunc of F let r be Real; ::_thesis: for R being RestFunc of F holds r (#) R is RestFunc of F let R be RestFunc of F; ::_thesis: r (#) R is RestFunc of F A1: R is total by Def1; then A2: r (#) R is total by VFUNCT_1:34; now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((r_(#)_R)_/*_h)_is_convergent_&_lim_((h_")_(#)_((r_(#)_R)_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((r (#) R) /* h) is convergent & lim ((h ") (#) ((r (#) R) /* h)) = 0. F ) dom R = REAL by A1, FUNCT_2:def_1; then rng h c= dom R ; then A3: (h ") (#) ((r (#) R) /* h) = (h ") (#) (r * (R /* h)) by NFCONT_3:4 .= r * ((h ") (#) (R /* h)) by NDIFF_1:10 ; A4: (h ") (#) (R /* h) is convergent by Def1; hence (h ") (#) ((r (#) R) /* h) is convergent by A3, NORMSP_1:22; ::_thesis: lim ((h ") (#) ((r (#) R) /* h)) = 0. F lim ((h ") (#) (R /* h)) = 0. F by Def1; hence lim ((h ") (#) ((r (#) R) /* h)) = r * (0. F) by A4, A3, NORMSP_1:28 .= 0. F by RLVECT_1:10 ; ::_thesis: verum end; hence r (#) R is RestFunc of F by A2, Def1; ::_thesis: verum end; definition let F be non trivial RealNormSpace; let f be PartFunc of REAL, the carrier of F; let x0 be real number ; predf is_differentiable_in x0 means :Def3: :: NDIFF_3:def 3 ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ); end; :: deftheorem Def3 defines is_differentiable_in NDIFF_3:def_3_:_ for F being non trivial RealNormSpace for f being PartFunc of REAL, the carrier of F for x0 being real number holds ( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ); definition let F be non trivial RealNormSpace; let f be PartFunc of REAL, the carrier of F; let x0 be real number ; assume A1: f is_differentiable_in x0 ; func diff (f,x0) -> Point of F means :Def4: :: NDIFF_3:def 4 ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( it = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ); existence ex b1 being Point of F ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( b1 = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) proof consider N being Neighbourhood of x0 such that A2: N c= dom f and A3: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3; consider L being LinearFunc of F, R being RestFunc of F such that A4: for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3; consider r being Point of F such that A5: for p being Real holds L . p = p * r by Def2; take r ; ::_thesis: ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( r = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) L . 1 = 1 * r by A5 .= r by RLVECT_1:def_8 ; hence ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( r = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) by A2, A4; ::_thesis: verum end; uniqueness for b1, b2 being Point of F st ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( b1 = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( b2 = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) holds b1 = b2 proof let r, s be Point of F; ::_thesis: ( ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( r = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( s = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) implies r = s ) assume that A6: ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( r = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) and A7: ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( s = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) ; ::_thesis: r = s consider N being Neighbourhood of x0 such that N c= dom f and A8: ex L being LinearFunc of F ex R being RestFunc of F st ( r = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) by A6; consider L being LinearFunc of F, R being RestFunc of F such that A9: r = L . 1 and A10: for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8; consider r1 being Point of F such that A11: for p being Real holds L . p = p * r1 by Def2; consider N1 being Neighbourhood of x0 such that N1 c= dom f and A12: ex L being LinearFunc of F ex R being RestFunc of F st ( s = L . 1 & ( for x being Real st x in N1 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) by A7; consider L1 being LinearFunc of F, R1 being RestFunc of F such that A13: s = L1 . 1 and A14: for x being Real st x in N1 holds (f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A12; consider p1 being Point of F such that A15: for p being Real holds L1 . p = p * p1 by Def2; consider N0 being Neighbourhood of x0 such that A16: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17; consider g being real number such that A17: 0 < g and A18: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6; deffunc H1( Element of NAT ) -> Element of REAL = g / (\$1 + 2); consider s1 being Real_Sequence such that A19: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_s1_._n let n be Element of NAT ; ::_thesis: 0 <> s1 . n 0 <> g / (n + 2) by A17, XREAL_1:139; hence 0 <> s1 . n by A19; ::_thesis: verum end; then A20: s1 is non-zero by SEQ_1:5; ( s1 is convergent & lim s1 = 0 ) by A19, SEQ_4:31; then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A20, FDIFF_1:def_1; A21: for n being Element of NAT ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) proof let n be Element of NAT ; ::_thesis: ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) take x = x0 + (g / (n + 2)); ::_thesis: ( x in N & x in N1 & h . n = x - x0 ) reconsider z0 = 0 as Element of NAT ; z0 + 1 < (n + 1) + 1 by XREAL_1:6; then g / (n + 2) < g / 1 by A17, XREAL_1:76; then A22: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6; 0 < g / (n + 2) by A17, XREAL_1:139; then x0 + (- g) < x0 + (g / (n + 2)) by A17, XREAL_1:6; then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A22; hence ( x in N & x in N1 & h . n = x - x0 ) by A16, A18, A19; ::_thesis: verum end; A23: s = 1 * p1 by A13, A15; A24: r = 1 * r1 by A9, A11; A25: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_ ((x_-_x0)_*_r)_+_(R_/._(x_-_x0))_=_((x_-_x0)_*_s)_+_(R1_/._(x_-_x0)) let x be Real; ::_thesis: ( x in N & x in N1 implies ((x - x0) * r) + (R /. (x - x0)) = ((x - x0) * s) + (R1 /. (x - x0)) ) assume that A26: x in N and A27: x in N1 ; ::_thesis: ((x - x0) * r) + (R /. (x - x0)) = ((x - x0) * s) + (R1 /. (x - x0)) (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A10, A26; then (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A14, A27; then ((x - x0) * r1) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A11; then (((x - x0) * 1) * r1) + (R /. (x - x0)) = (((x - x0) * 1) * p1) + (R1 /. (x - x0)) by A15; then (((x - x0) * 1) * r) + (R /. (x - x0)) = (((x - x0) * 1) * p1) + (R1 /. (x - x0)) by A24, RLVECT_1:def_7; hence ((x - x0) * r) + (R /. (x - x0)) = ((x - x0) * s) + (R1 /. (x - x0)) by A23, RLVECT_1:def_7; ::_thesis: verum end; now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n R1 is total by Def1; then dom R1 = REAL by PARTFUN1:def_2; then A28: rng h c= dom R1 ; let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n R is total by Def1; then dom R = REAL by PARTFUN1:def_2; then A29: rng h c= dom R ; A30: n in NAT by ORDINAL1:def_12; then ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) by A21; then ((h . n) * r) + (R /. (h . n)) = ((h . n) * s) + (R1 /. (h . n)) by A25; then ((1 / (h . n)) * ((h . n) * r)) + ((1 / (h . n)) * (R /. (h . n))) = (1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n))) by RLVECT_1:def_5; then (((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n))) = (1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n))) by RLVECT_1:def_7; then A31: (((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n))) = ((1 / (h . n)) * ((h . n) * s)) + ((1 / (h . n)) * (R1 /. (h . n))) by RLVECT_1:def_5; A32: (1 / (h . n)) * (R /. (h . n)) = ((h . n) ") * (R /. (h . n)) by XCMPLX_1:215 .= ((h ") . n) * (R /. (h . n)) by VALUED_1:10 .= ((h ") . n) * ((R /* h) . n) by A30, A29, FUNCT_2:109 .= ((h ") (#) (R /* h)) . n by A30, NDIFF_1:def_2 ; A33: h . n <> 0 by A30, SEQ_1:5; A34: (1 / (h . n)) * (R1 /. (h . n)) = ((h . n) ") * (R1 /. (h . n)) by XCMPLX_1:215 .= ((h ") . n) * (R1 /. (h . n)) by VALUED_1:10 .= ((h ") . n) * ((R1 /* h) . n) by A30, A28, FUNCT_2:109 .= ((h ") (#) (R1 /* h)) . n by A30, NDIFF_1:def_2 ; A35: ((1 / (h . n)) * (h . n)) * s = 1 * s by A33, XCMPLX_1:106 .= s by RLVECT_1:def_8 ; ((1 / (h . n)) * (h . n)) * r = 1 * r by A33, XCMPLX_1:106 .= r by RLVECT_1:def_8 ; then r + (((h ") (#) (R /* h)) . n) = s + (((h ") (#) (R1 /* h)) . n) by A31, A35, A32, A34, RLVECT_1:def_7; then r + ((((h ") (#) (R /* h)) . n) - (((h ") (#) (R /* h)) . n)) = (s + (((h ") (#) (R1 /* h)) . n)) - (((h ") (#) (R /* h)) . n) by RLVECT_1:28; then r + ((((h ") (#) (R /* h)) . n) - (((h ") (#) (R /* h)) . n)) = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by RLVECT_1:28; then r + (0. F) = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by RLVECT_1:15; then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by RLVECT_1:4; then r - s = ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) + (s - s) by RLVECT_1:28; then r - s = ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) + (0. F) by RLVECT_1:15; then A36: r - s = (((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n) by RLVECT_1:4; n is Element of NAT by ORDINAL1:def_12; hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A36, NORMSP_1:def_3; ::_thesis: verum end; then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 0 = r - s ) by VALUED_0:def_18; then A37: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by NDIFF_1:18; A38: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. F ) by Def1; ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. F ) by Def1; then r - s = (0. F) - (0. F) by A37, A38, NORMSP_1:26; hence r = s by RLVECT_1:13, RLVECT_1:21; ::_thesis: verum end; end; :: deftheorem Def4 defines diff NDIFF_3:def_4_:_ for F being non trivial RealNormSpace for f being PartFunc of REAL, the carrier of F for x0 being real number st f is_differentiable_in x0 holds for b4 being Point of F holds ( b4 = diff (f,x0) iff ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st ( b4 = L . 1 & ( for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) ); definition let F be non trivial RealNormSpace; let f be PartFunc of REAL, the carrier of F; let X be set ; predf is_differentiable_on X means :Def5: :: NDIFF_3:def 5 ( X c= dom f & ( for x being Real st x in X holds f | X is_differentiable_in x ) ); end; :: deftheorem Def5 defines is_differentiable_on NDIFF_3:def_5_:_ for F being non trivial RealNormSpace for f being PartFunc of REAL, the carrier of F for X being set holds ( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds f | X is_differentiable_in x ) ) ); theorem Th9: :: NDIFF_3:9 for F being non trivial RealNormSpace for X being set for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds X is Subset of REAL proof let F be non trivial RealNormSpace; ::_thesis: for X being set for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds X is Subset of REAL let X be set ; ::_thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds X is Subset of REAL let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on X implies X is Subset of REAL ) assume f is_differentiable_on X ; ::_thesis: X is Subset of REAL then X c= dom f by Def5; hence X is Subset of REAL by XBOOLE_1:1; ::_thesis: verum end; theorem Th10: :: NDIFF_3:10 for F being non trivial RealNormSpace for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) proof let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) implies f is_differentiable_on Z ) proof assume A1: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) hence A2: Z c= dom f by Def5; ::_thesis: for x being Real st x in Z holds f is_differentiable_in x let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A3: x0 in Z ; ::_thesis: f is_differentiable_in x0 then f | Z is_differentiable_in x0 by A1, Def5; then consider N being Neighbourhood of x0 such that A4: N c= dom (f | Z) and A5: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3; take N ; :: according to NDIFF_3:def_3 ::_thesis: ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) dom (f | Z) = (dom f) /\ Z by RELAT_1:61; then dom (f | Z) c= dom f by XBOOLE_1:17; hence N c= dom f by A4, XBOOLE_1:1; ::_thesis: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) consider L being LinearFunc of F, R being RestFunc of F such that A6: for x being Real st x in N holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5; now__::_thesis:_for_x_being_Real_st_x_in_N_holds_ (f_/._x)_-_(f_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) assume A7: x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then A8: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6; (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8, A4, A7, PARTFUN2:15; hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, A3, PARTFUN2:17; ::_thesis: verum end; hence ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; ::_thesis: verum end; assume that A9: Z c= dom f and A10: for x being Real st x in Z holds f is_differentiable_in x ; ::_thesis: f is_differentiable_on Z thus Z c= dom f by A9; :: according to NDIFF_3:def_5 ::_thesis: for x being Real st x in Z holds f | Z is_differentiable_in x let x0 be Real; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 ) assume A11: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0 then consider N1 being Neighbourhood of x0 such that A12: N1 c= Z by RCOMP_1:18; f is_differentiable_in x0 by A10, A11; then consider N being Neighbourhood of x0 such that A13: N c= dom f and A14: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3; consider N2 being Neighbourhood of x0 such that A15: N2 c= N1 and A16: N2 c= N by RCOMP_1:17; A17: N2 c= Z by A12, A15, XBOOLE_1:1; take N2 ; :: according to NDIFF_3:def_3 ::_thesis: ( N2 c= dom (f | Z) & ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) N2 c= dom f by A13, A16, XBOOLE_1:1; then N2 c= (dom f) /\ Z by A17, XBOOLE_1:19; hence A18: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) consider L being LinearFunc of F, R being RestFunc of F such that A19: for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A14; A20: x0 in N2 by RCOMP_1:16; take L ; ::_thesis: ex R being RestFunc of F st for x being Real st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) take R ; ::_thesis: for x being Real st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) now__::_thesis:_for_x_being_Real_st_x_in_N2_holds_ ((f_|_Z)_/._x)_-_((f_|_Z)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Real; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) assume A21: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A16, A19; then ((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A21, A18, PARTFUN2:15; hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A20, A18, PARTFUN2:15; ::_thesis: verum end; hence for x being Real st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; ::_thesis: verum end; theorem :: NDIFF_3:11 for F being non trivial RealNormSpace for Y being Subset of REAL for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds Y is open proof let F be non trivial RealNormSpace; ::_thesis: for Y being Subset of REAL for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds Y is open let Y be Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds Y is open let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on Y implies Y is open ) assume A1: f is_differentiable_on Y ; ::_thesis: Y is open now__::_thesis:_for_x0_being_real_number_st_x0_in_Y_holds_ ex_N_being_Neighbourhood_of_x0_st_N_c=_Y let x0 be real number ; ::_thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y ) assume x0 in Y ; ::_thesis: ex N being Neighbourhood of x0 st N c= Y then f | Y is_differentiable_in x0 by A1, Def5; then consider N being Neighbourhood of x0 such that A2: N c= dom (f | Y) and ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds ((f | Y) /. x) - ((f | Y) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3; take N = N; ::_thesis: N c= Y thus N c= Y by A2, XBOOLE_1:1; ::_thesis: verum end; hence Y is open by RCOMP_1:20; ::_thesis: verum end; definition let F be non trivial RealNormSpace; let f be PartFunc of REAL, the carrier of F; let X be set ; assume A1: f is_differentiable_on X ; funcf `| X -> PartFunc of REAL, the carrier of F means :Def6: :: NDIFF_3:def 6 ( dom it = X & ( for x being Real st x in X holds it . x = diff (f,x) ) ); existence ex b1 being PartFunc of REAL, the carrier of F st ( dom b1 = X & ( for x being Real st x in X holds b1 . x = diff (f,x) ) ) proof deffunc H1( Real) -> Point of F = diff (f,\$1); defpred S1[ set ] means \$1 in X; consider F0 being PartFunc of REAL, the carrier of F such that A2: ( ( for x being Real holds ( x in dom F0 iff S1[x] ) ) & ( for x being Real st x in dom F0 holds F0 . x = H1(x) ) ) from SEQ_1:sch_3(); take F0 ; ::_thesis: ( dom F0 = X & ( for x being Real st x in X holds F0 . x = diff (f,x) ) ) now__::_thesis:_for_y_being_set_st_y_in_X_holds_ y_in_dom_F0 A3: X is Subset of REAL by A1, Th9; let y be set ; ::_thesis: ( y in X implies y in dom F0 ) assume y in X ; ::_thesis: y in dom F0 hence y in dom F0 by A2, A3; ::_thesis: verum end; then A4: X c= dom F0 by TARSKI:def_3; for y being set st y in dom F0 holds y in X by A2; then dom F0 c= X by TARSKI:def_3; hence dom F0 = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Real st x in X holds F0 . x = diff (f,x) now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ F0_._x_=_diff_(f,x) let x be Real; ::_thesis: ( x in X implies F0 . x = diff (f,x) ) assume x in X ; ::_thesis: F0 . x = diff (f,x) then x in dom F0 by A2; hence F0 . x = diff (f,x) by A2; ::_thesis: verum end; hence for x being Real st x in X holds F0 . x = diff (f,x) ; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of REAL, the carrier of F st dom b1 = X & ( for x being Real st x in X holds b1 . x = diff (f,x) ) & dom b2 = X & ( for x being Real st x in X holds b2 . x = diff (f,x) ) holds b1 = b2 proof let F0, G0 be PartFunc of REAL, the carrier of F; ::_thesis: ( dom F0 = X & ( for x being Real st x in X holds F0 . x = diff (f,x) ) & dom G0 = X & ( for x being Real st x in X holds G0 . x = diff (f,x) ) implies F0 = G0 ) assume that A5: dom F0 = X and A6: for x being Real st x in X holds F0 . x = diff (f,x) and A7: dom G0 = X and A8: for x being Real st x in X holds G0 . x = diff (f,x) ; ::_thesis: F0 = G0 now__::_thesis:_for_x_being_Real_st_x_in_dom_F0_holds_ F0_._x_=_G0_._x let x be Real; ::_thesis: ( x in dom F0 implies F0 . x = G0 . x ) assume A9: x in dom F0 ; ::_thesis: F0 . x = G0 . x then F0 . x = diff (f,x) by A5, A6; hence F0 . x = G0 . x by A5, A8, A9; ::_thesis: verum end; hence F0 = G0 by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def6 defines `| NDIFF_3:def_6_:_ for F being non trivial RealNormSpace for f being PartFunc of REAL, the carrier of F for X being set st f is_differentiable_on X holds for b4 being PartFunc of REAL, the carrier of F holds ( b4 = f `| X iff ( dom b4 = X & ( for x being Real st x in X holds b4 . x = diff (f,x) ) ) ); theorem :: NDIFF_3:12 for F being non trivial RealNormSpace for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0. F ) ) proof let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0. F ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0. F ) ) let f be PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom f & ex r being Point of F st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0. F ) ) ) set R = REAL --> (0. F); A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F A2: rng h c= dom (REAL --> (0. F)) by A1; A3: n in NAT by ORDINAL1:def_12; hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2 .= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108 .= 0. F by FUNCOP_1:7, RLVECT_1:10 ; ::_thesis: verum end; then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18; hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum end; then reconsider R = REAL --> (0. F) as RestFunc of F by Def1; reconsider L = REAL --> (0. F) as Function of REAL,F ; now__::_thesis:_for_p_being_Real_holds_L_._p_=_p_*_(0._F) let p be Real; ::_thesis: L . p = p * (0. F) thus L . p = 0. F by FUNCOP_1:7 .= p * (0. F) by RLVECT_1:10 ; ::_thesis: verum end; then reconsider L = L as LinearFunc of F by Def2; assume A4: Z c= dom f ; ::_thesis: ( for r being Point of F holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0. F ) ) ) given r being Point of F such that A5: rng f = {r} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0. F ) ) A6: now__::_thesis:_for_x0_being_Real_st_x0_in_dom_f_holds_ f_/._x0_=_r let x0 be Real; ::_thesis: ( x0 in dom f implies f /. x0 = r ) assume A7: x0 in dom f ; ::_thesis: f /. x0 = r then f /. x0 = f . x0 by PARTFUN1:def_6; then f /. x0 in {r} by A5, A7, FUNCT_1:def_3; hence f /. x0 = r by TARSKI:def_1; ::_thesis: verum end; A8: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A9: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A10: N c= Z by RCOMP_1:18; A11: N c= dom f by A4, A10, XBOOLE_1:1; for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A12: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6 .= 0. F by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = r - (f /. x0) by A6, A11 .= r - r by A4, A6, A9 .= 0. F by RLVECT_1:15 .= L . (x - x0) by FUNCOP_1:7 .= (L . (x - x0)) + (R /. (x - x0)) by A12, RLVECT_1:4 ; ::_thesis: verum end; hence f is_differentiable_in x0 by A11, Def3; ::_thesis: verum end; hence A13: f is_differentiable_on Z by A4, Th10; ::_thesis: for x being Real st x in Z holds (f `| Z) /. x = 0. F let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. F ) assume A14: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0. F then A15: f is_differentiable_in x0 by A8; then ex N being Neighbourhood of x0 st ( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by Def3; then consider N being Neighbourhood of x0 such that A16: N c= dom f ; A17: for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A18: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6 .= 0. F by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = r - (f /. x0) by A6, A16 .= r - r by A4, A6, A14 .= 0. F by RLVECT_1:15 .= L . (x - x0) by FUNCOP_1:7 .= (L . (x - x0)) + (R /. (x - x0)) by A18, RLVECT_1:4 ; ::_thesis: verum end; dom (f `| Z) = Z by A13, Def6; hence (f `| Z) /. x0 = (f `| Z) . x0 by A14, PARTFUN1:def_6 .= diff (f,x0) by A13, A14, Def6 .= L . 1 by A15, A16, A17, Def4 .= 0. F by FUNCOP_1:7 ; ::_thesis: verum end; theorem Th13: :: NDIFF_3:13 for F being non trivial RealNormSpace for f being PartFunc of REAL, the carrier of F for x0 being real number for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) proof let F be non trivial RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of F for x0 being real number for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) let f be PartFunc of REAL, the carrier of F; ::_thesis: for x0 being real number for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) let x0 be real number ; ::_thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) let N be Neighbourhood of x0; ::_thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) ) assume that A1: f is_differentiable_in x0 and A2: N c= dom f ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) consider N1 being Neighbourhood of x0 such that N1 c= dom f and A3: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N1 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3; consider N2 being Neighbourhood of x0 such that A4: N2 c= N and A5: N2 c= N1 by RCOMP_1:17; A6: N2 c= dom f by A2, A4, XBOOLE_1:1; let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) let c be constant Real_Sequence; ::_thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) ) assume that A7: rng c = {x0} and A8: rng (h + c) c= N ; ::_thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) consider g being real number such that A9: 0 < g and A10: N2 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6; reconsider z0 = 0 as Nat ; ( x0 + z0 < x0 + g & x0 - g < x0 - 0 ) by A9, XREAL_1:8, XREAL_1:15; then A11: x0 in N2 by A10; now__::_thesis:_for_y_being_set_st_y_in_rng_c_holds_ y_in_dom_f let y be set ; ::_thesis: ( y in rng c implies y in dom f ) assume y in rng c ; ::_thesis: y in dom f then y = x0 by A7, TARSKI:def_1; then y in N by A4, A11; hence y in dom f by A2; ::_thesis: verum end; then A12: rng c c= dom f by TARSKI:def_3; ex n being Element of NAT st ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) proof x0 in rng c by A7, TARSKI:def_1; then A13: lim c = x0 by SEQ_4:25; A14: h + c is convergent by SEQ_2:5; reconsider z0 = 0 as Real ; lim h = z0 ; then lim (h + c) = z0 + x0 by A13, SEQ_2:6 .= x0 ; then consider n being Element of NAT such that A15: for m being Element of NAT st n <= m holds abs (((h + c) . m) - x0) < g by A9, A14, SEQ_2:def_7; take n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) A16: rng (c ^\ n) = {x0} by A7, VALUED_0:26; for y being set st y in rng (c ^\ n) holds y in N2 by A11, A16, TARSKI:def_1; hence rng (c ^\ n) c= N2 by TARSKI:def_3; ::_thesis: rng ((h + c) ^\ n) c= N2 now__::_thesis:_for_y_being_set_st_y_in_rng_((h_+_c)_^\_n)_holds_ y_in_N2 let y be set ; ::_thesis: ( y in rng ((h + c) ^\ n) implies y in N2 ) assume y in rng ((h + c) ^\ n) ; ::_thesis: y in N2 then consider m being Element of NAT such that A17: y = ((h + c) ^\ n) . m by FUNCT_2:113; reconsider z0 = 0 as Nat ; n + z0 <= n + m by XREAL_1:7; then A18: abs (((h + c) . (n + m)) - x0) < g by A15; then ((h + c) . (m + n)) - x0 < g by SEQ_2:1; then (((h + c) ^\ n) . m) - x0 < g by NAT_1:def_3; then A19: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19; - g < ((h + c) . (m + n)) - x0 by A18, SEQ_2:1; then - g < (((h + c) ^\ n) . m) - x0 by NAT_1:def_3; then x0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20; hence y in N2 by A10, A17, A19; ::_thesis: verum end; hence rng ((h + c) ^\ n) c= N2 by TARSKI:def_3; ::_thesis: verum end; then consider n being Element of NAT such that rng (c ^\ n) c= N2 and A20: rng ((h + c) ^\ n) c= N2 ; consider L being LinearFunc of F, R being RestFunc of F such that A21: for x being Real st x in N1 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3; now__::_thesis:_for_y_being_set_st_y_in_rng_(c_^\_n)_holds_ y_in_dom_f let y be set ; ::_thesis: ( y in rng (c ^\ n) implies y in dom f ) assume A22: y in rng (c ^\ n) ; ::_thesis: y in dom f rng (c ^\ n) = rng c by VALUED_0:26; then y = x0 by A7, A22, TARSKI:def_1; then y in N by A4, A11; hence y in dom f by A2; ::_thesis: verum end; then A23: rng (c ^\ n) c= dom f by TARSKI:def_3; A24: ( ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) is convergent & lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L . 1 ) proof deffunc H1( Element of NAT ) -> Element of the carrier of F = (L . 1) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . \$1); consider s1 being sequence of the carrier of F such that A25: for k being Element of NAT holds s1 . k = H1(k) from FUNCT_2:sch_4(); A26: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_n1_being_Element_of_NAT_st_ for_k_being_Element_of_NAT_st_n1_<=_k_holds_ ||.((s1_._k)_-_(L_._1)).||_<_r A27: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0. F ) by Def1; let r be Real; ::_thesis: ( 0 < r implies ex n1 being Element of NAT st for k being Element of NAT st n1 <= k holds ||.((s1 . k) - (L . 1)).|| < r ) assume 0 < r ; ::_thesis: ex n1 being Element of NAT st for k being Element of NAT st n1 <= k holds ||.((s1 . k) - (L . 1)).|| < r then consider m being Element of NAT such that A28: for k being Element of NAT st m <= k holds ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - (0. F)).|| < r by A27, NORMSP_1:def_7; take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds ||.((s1 . k) - (L . 1)).|| < r let k be Element of NAT ; ::_thesis: ( n1 <= k implies ||.((s1 . k) - (L . 1)).|| < r ) assume A29: n1 <= k ; ::_thesis: ||.((s1 . k) - (L . 1)).|| < r A30: ||.((s1 . k) - (L . 1)).|| = ||.(((L . 1) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . k)) - (L . 1)).|| by A25 .= ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) + ((L . 1) - (L . 1))).|| by RLVECT_1:28 .= ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) + (0. F)).|| by RLVECT_1:15 .= ||.((((h ^\ n) ") (#) (R /* (h ^\ n))) . k).|| by RLVECT_1:4 ; ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - (0. F)).|| < r by A28, A29; hence ||.((s1 . k) - (L . 1)).|| < r by A30, RLVECT_1:13; ::_thesis: verum end; consider s being Point of F such that A31: for p1 being Real holds L . p1 = p1 * s by Def2; A32: L . 1 = 1 * s by A31 .= s by RLVECT_1:def_8 ; now__::_thesis:_for_m_being_Element_of_NAT_holds_(((h_^\_n)_")_(#)_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n))))_._m_=_s1_._m let m be Element of NAT ; ::_thesis: (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) . m = s1 . m A33: (h ^\ n) . m <> 0 by SEQ_1:5; thus (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) . m = ((((h ^\ n) ") (#) (L /* (h ^\ n))) + (((h ^\ n) ") (#) (R /* (h ^\ n)))) . m by NDIFF_1:9 .= ((((h ^\ n) ") (#) (L /* (h ^\ n))) . m) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by NORMSP_1:def_2 .= ((((h ^\ n) ") . m) * ((L /* (h ^\ n)) . m)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by NDIFF_1:def_2 .= ((((h ^\ n) ") . m) * (L . ((h ^\ n) . m))) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by FUNCT_2:115 .= ((((h ^\ n) ") . m) * (((h ^\ n) . m) * s)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by A31 .= ((((h ^\ n) . m) ") * (((h ^\ n) . m) * s)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by VALUED_1:10 .= (((((h ^\ n) . m) ") * ((h ^\ n) . m)) * s) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by RLVECT_1:def_7 .= (1 * s) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by A33, XCMPLX_0:def_7 .= s + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by RLVECT_1:def_8 .= s1 . m by A25, A32 ; ::_thesis: verum end; then A34: ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) = s1 by FUNCT_2:63; hence ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) is convergent by A26, NORMSP_1:def_6; ::_thesis: lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L . 1 hence lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L . 1 by A34, A26, NORMSP_1:def_7; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_((h_+_c)_^\_n)_holds_ y_in_dom_f let y be set ; ::_thesis: ( y in rng ((h + c) ^\ n) implies y in dom f ) assume y in rng ((h + c) ^\ n) ; ::_thesis: y in dom f then y in N2 by A20; then y in N by A4; hence y in dom f by A2; ::_thesis: verum end; then A35: rng ((h + c) ^\ n) c= dom f by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_rng_(h_+_c)_holds_ y_in_dom_f let y be set ; ::_thesis: ( y in rng (h + c) implies y in dom f ) assume y in rng (h + c) ; ::_thesis: y in dom f then y in N by A8; hence y in dom f by A2; ::_thesis: verum end; then A36: rng (h + c) c= dom f by TARSKI:def_3; A37: for k being Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) proof let k be Element of NAT ; ::_thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) ((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28; then A38: ((h + c) ^\ n) . k in N2 by A20; ( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28; then A39: (c ^\ n) . k = x0 by A7, TARSKI:def_1; (((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15 .= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7 .= (h ^\ n) . k ; hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A21, A5, A38, A39; ::_thesis: verum end; A40: R is total by Def1; now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_/*_((h_+_c)_^\_n))_-_(f_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k let k be Element of NAT ; ::_thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k dom R = REAL by A40, FUNCT_2:def_1; then A41: rng (h ^\ n) c= dom R ; thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by NORMSP_1:def_3 .= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A35, FUNCT_2:109 .= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A23, FUNCT_2:109 .= (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A37 .= ((L /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by FUNCT_2:115 .= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A41, FUNCT_2:109 .= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def_2 ; ::_thesis: verum end; then (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63; then A42: ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) = ((h ^\ n) ") (#) (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) by A36, VALUED_0:27 .= ((h ^\ n) ") (#) (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) by A12, VALUED_0:27 .= ((h ^\ n) ") (#) (((f /* (h + c)) - (f /* c)) ^\ n) by NDIFF_1:16 .= ((h ") ^\ n) (#) (((f /* (h + c)) - (f /* c)) ^\ n) by SEQM_3:18 .= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n by Th2 ; then A43: L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A24, LOPBAN_3:11; thus (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A24, A42, LOPBAN_3:10; ::_thesis: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) for x being Real st x in N2 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A21, A5; hence diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A1, A6, A43, Def4; ::_thesis: verum end; theorem Th14: :: NDIFF_3:14 for F being non trivial RealNormSpace for x0 being Real for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) proof let F be non trivial RealNormSpace; ::_thesis: for x0 being Real for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) let x0 be Real; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) let f1, f2 be PartFunc of REAL, the carrier of F; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) ) assume that A1: f1 is_differentiable_in x0 and A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) consider N1 being Neighbourhood of x0 such that A3: N1 c= dom f1 and A4: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N1 holds (f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3; consider L1 being LinearFunc of F, R1 being RestFunc of F such that A5: for x being Real st x in N1 holds (f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4; consider N2 being Neighbourhood of x0 such that A6: N2 c= dom f2 and A7: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N2 holds (f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def3; consider L2 being LinearFunc of F, R2 being RestFunc of F such that A8: for x being Real st x in N2 holds (f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7; reconsider R = R1 + R2 as RestFunc of F by Th7; reconsider L = L1 + L2 as LinearFunc of F by Th3; A9: ( dom L1 = REAL & dom L2 = REAL ) by FUNCT_2:def_1; consider N being Neighbourhood of x0 such that A10: N c= N1 and A11: N c= N2 by RCOMP_1:17; A12: N c= dom f2 by A6, A11, XBOOLE_1:1; N c= dom f1 by A3, A10, XBOOLE_1:1; then N /\ N c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:27; then A13: N c= dom (f1 + f2) by VFUNCT_1:def_1; ( R1 is total & R2 is total ) by Def1; then R1 + R2 is total by VFUNCT_1:32; then A14: dom (R1 + R2) = REAL by FUNCT_2:def_1; L1 + L2 is total by VFUNCT_1:32; then A15: dom (L1 + L2) = REAL by FUNCT_2:def_1; A16: now__::_thesis:_for_x_being_Real_st_x_in_N_holds_ ((f1_+_f2)_/._x)_-_((f1_+_f2)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Real; ::_thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A17: x0 in N by RCOMP_1:16; assume A18: x in N ; ::_thesis: ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0) by A13, VFUNCT_1:def_1 .= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A13, A17, VFUNCT_1:def_1 .= (f1 /. x) + ((f2 /. x) - ((f1 /. x0) + (f2 /. x0))) by RLVECT_1:28 .= (f1 /. x) + (((f2 /. x) - (f2 /. x0)) - (f1 /. x0)) by RLVECT_1:27 .= ((f1 /. x) + ((f2 /. x) - (f2 /. x0))) - (f1 /. x0) by RLVECT_1:28 .= ((f2 /. x) - (f2 /. x0)) + ((f1 /. x) - (f1 /. x0)) by RLVECT_1:28 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A10, A18 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A11, A18 .= (((L1 . (x - x0)) + (R1 /. (x - x0))) + (L2 . (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3 .= (((L1 . (x - x0)) + (L2 . (x - x0))) + (R1 /. (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3 .= ((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by RLVECT_1:def_3 .= (L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by A15, VFUNCT_1:def_1 .= (L . (x - x0)) + (R /. (x - x0)) by A14, VFUNCT_1:def_1 ; ::_thesis: verum end; hence f1 + f2 is_differentiable_in x0 by A13, Def3; ::_thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) hence diff ((f1 + f2),x0) = L . 1 by A13, A16, Def4 .= L /. 1 by A15, PARTFUN1:def_6 .= (L1 /. 1) + (L2 /. 1) by A15, VFUNCT_1:def_1 .= (L1 . 1) + (L2 /. 1) by A9, PARTFUN1:def_6 .= (L1 . 1) + (L2 . 1) by A9, PARTFUN1:def_6 .= (diff (f1,x0)) + (L2 . 1) by A1, A3, A5, Def4 .= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def4 ; ::_thesis: verum end; theorem Th15: :: NDIFF_3:15 for F being non trivial RealNormSpace for x0 being Real for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) proof let F be non trivial RealNormSpace; ::_thesis: for x0 being Real for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) let x0 be Real; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) let f1, f2 be PartFunc of REAL, the carrier of F; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) ) assume that A1: f1 is_differentiable_in x0 and A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) consider N1 being Neighbourhood of x0 such that A3: N1 c= dom f1 and A4: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N1 holds (f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3; consider L1 being LinearFunc of F, R1 being RestFunc of F such that A5: for x being Real st x in N1 holds (f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4; consider N2 being Neighbourhood of x0 such that A6: N2 c= dom f2 and A7: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N2 holds (f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def3; consider L2 being LinearFunc of F, R2 being RestFunc of F such that A8: for x being Real st x in N2 holds (f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7; reconsider R = R1 - R2 as RestFunc of F by Th7; reconsider L = L1 - L2 as LinearFunc of F by Th3; A9: ( dom L1 = REAL & dom L2 = REAL ) by FUNCT_2:def_1; consider N being Neighbourhood of x0 such that A10: N c= N1 and A11: N c= N2 by RCOMP_1:17; A12: N c= dom f2 by A6, A11, XBOOLE_1:1; N c= dom f1 by A3, A10, XBOOLE_1:1; then N /\ N c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:27; then A13: N c= dom (f1 - f2) by VFUNCT_1:def_2; ( R1 is total & R2 is total ) by Def1; then R1 - R2 is total by VFUNCT_1:32; then A14: dom (R1 - R2) = REAL by FUNCT_2:def_1; L1 - L2 is total by VFUNCT_1:32; then A15: dom (L1 - L2) = REAL by FUNCT_2:def_1; A16: now__::_thesis:_for_x_being_Real_st_x_in_N_holds_ ((f1_-_f2)_/._x)_-_((f1_-_f2)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Real; ::_thesis: ( x in N implies ((f1 - f2) /. x) - ((f1 - f2) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A17: x0 in N by RCOMP_1:16; assume A18: x in N ; ::_thesis: ((f1 - f2) /. x) - ((f1 - f2) /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0) by A13, VFUNCT_1:def_2 .= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A13, A17, VFUNCT_1:def_2 .= (f1 /. x) - ((f2 /. x) + ((f1 /. x0) - (f2 /. x0))) by RLVECT_1:27 .= (f1 /. x) - (((f2 /. x) + (f1 /. x0)) - (f2 /. x0)) by RLVECT_1:28 .= (f1 /. x) - ((f1 /. x0) + ((f2 /. x) - (f2 /. x0))) by RLVECT_1:28 .= ((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0)) by RLVECT_1:27 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0)) by A5, A10, A18 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A11, A18 .= (L1 . (x - x0)) + ((R1 /. (x - x0)) - ((L2 . (x - x0)) + (R2 /. (x - x0)))) by RLVECT_1:28 .= (L1 . (x - x0)) + (((R1 /. (x - x0)) - (R2 /. (x - x0))) - (L2 . (x - x0))) by RLVECT_1:27 .= ((L1 . (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) - (L2 . (x - x0)) by RLVECT_1:28 .= ((L1 /. (x - x0)) - (L2 /. (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by RLVECT_1:28 .= (L /. (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by A15, VFUNCT_1:def_2 .= (L . (x - x0)) + (R /. (x - x0)) by A14, VFUNCT_1:def_2 ; ::_thesis: verum end; hence f1 - f2 is_differentiable_in x0 by A13, Def3; ::_thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) hence diff ((f1 - f2),x0) = L . 1 by A13, A16, Def4 .= L /. 1 by A15, PARTFUN1:def_6 .= (L1 /. 1) - (L2 /. 1) by A15, VFUNCT_1:def_2 .= (L1 . 1) - (L2 /. 1) by A9, PARTFUN1:def_6 .= (L1 . 1) - (L2 . 1) by A9, PARTFUN1:def_6 .= (diff (f1,x0)) - (L2 . 1) by A1, A3, A5, Def4 .= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def4 ; ::_thesis: verum end; theorem Th16: :: NDIFF_3:16 for F being non trivial RealNormSpace for x0 being Real for f being PartFunc of REAL, the carrier of F for r being Real st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) proof let F be non trivial RealNormSpace; ::_thesis: for x0 being Real for f being PartFunc of REAL, the carrier of F for r being Real st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) let x0 be Real; ::_thesis: for f being PartFunc of REAL, the carrier of F for r being Real st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) let f be PartFunc of REAL, the carrier of F; ::_thesis: for r being Real st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) let r be Real; ::_thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) ) assume A1: f is_differentiable_in x0 ; ::_thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) then consider N1 being Neighbourhood of x0 such that A2: N1 c= dom f and A3: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N1 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3; consider L1 being LinearFunc of F, R1 being RestFunc of F such that A4: for x being Real st x in N1 holds (f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A3; reconsider R = r (#) R1 as RestFunc of F by Th8; reconsider L = r (#) L1 as LinearFunc of F by Th4; A5: dom L1 = REAL by FUNCT_2:def_1; A6: N1 c= dom (r (#) f) by A2, VFUNCT_1:def_4; R1 is total by Def1; then r (#) R1 is total by VFUNCT_1:34; then A7: dom (r (#) R1) = REAL by FUNCT_2:def_1; r (#) L1 is total by VFUNCT_1:34; then A8: dom (r (#) L1) = REAL by FUNCT_2:def_1; A9: now__::_thesis:_for_x_being_Real_st_x_in_N1_holds_ ((r_(#)_f)_/._x)_-_((r_(#)_f)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Real; ::_thesis: ( x in N1 implies ((r (#) f) /. x) - ((r (#) f) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A10: x0 in N1 by RCOMP_1:16; assume A11: x in N1 ; ::_thesis: ((r (#) f) /. x) - ((r (#) f) /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence ((r (#) f) /. x) - ((r (#) f) /. x0) = (r * (f /. x)) - ((r (#) f) /. x0) by A6, VFUNCT_1:def_4 .= (r * (f /. x)) - (r * (f /. x0)) by A6, A10, VFUNCT_1:def_4 .= r * ((f /. x) - (f /. x0)) by RLVECT_1:34 .= r * ((L1 . (x - x0)) + (R1 /. (x - x0))) by A4, A11 .= (r * (L1 /. (x - x0))) + (r * (R1 /. (x - x0))) by RLVECT_1:def_5 .= (L /. (x - x0)) + (r * (R1 /. (x - x0))) by A8, VFUNCT_1:def_4 .= (L . (x - x0)) + (R /. (x - x0)) by A7, VFUNCT_1:def_4 ; ::_thesis: verum end; hence r (#) f is_differentiable_in x0 by A6, Def3; ::_thesis: diff ((r (#) f),x0) = r * (diff (f,x0)) hence diff ((r (#) f),x0) = L . 1 by A6, A9, Def4 .= L /. 1 by A8, PARTFUN1:def_6 .= r * (L1 /. 1) by A8, VFUNCT_1:def_4 .= r * (L1 . 1) by A5, PARTFUN1:def_6 .= r * (diff (f,x0)) by A1, A2, A4, Def4 ; ::_thesis: verum end; theorem :: NDIFF_3:17 for F being non trivial RealNormSpace for Z being open Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) proof let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) let f1, f2 be PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) ) assume that A1: Z c= dom (f1 + f2) and A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ f1_+_f2_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies f1 + f2 is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: f1 + f2 is_differentiable_in x0 then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th10; hence f1 + f2 is_differentiable_in x0 by Th14; ::_thesis: verum end; hence A3: f1 + f2 is_differentiable_on Z by A1, Th10; ::_thesis: for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) assume A4: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th10; thus ((f1 + f2) `| Z) . x = diff ((f1 + f2),x) by A3, A4, Def6 .= (diff (f1,x)) + (diff (f2,x)) by A5, Th14 ; ::_thesis: verum end; theorem :: NDIFF_3:18 for F being non trivial RealNormSpace for Z being open Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) proof let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) let f1, f2 be PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) ) assume that A1: Z c= dom (f1 - f2) and A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ f1_-_f2_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies f1 - f2 is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: f1 - f2 is_differentiable_in x0 then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th10; hence f1 - f2 is_differentiable_in x0 by Th15; ::_thesis: verum end; hence A3: f1 - f2 is_differentiable_on Z by A1, Th10; ::_thesis: for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) let x be Real; ::_thesis: ( x in Z implies ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) assume A4: x in Z ; ::_thesis: ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th10; thus ((f1 - f2) `| Z) . x = diff ((f1 - f2),x) by A3, A4, Def6 .= (diff (f1,x)) - (diff (f2,x)) by A5, Th15 ; ::_thesis: verum end; theorem :: NDIFF_3:19 for F being non trivial RealNormSpace for r being Real for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) proof let F be non trivial RealNormSpace; ::_thesis: for r being Real for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) let r be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) let f be PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom (r (#) f) & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) ) assume that A1: Z c= dom (r (#) f) and A2: f is_differentiable_on Z ; ::_thesis: ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ r_(#)_f_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies r (#) f is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: r (#) f is_differentiable_in x0 then f is_differentiable_in x0 by A2, Th10; hence r (#) f is_differentiable_in x0 by Th16; ::_thesis: verum end; hence A3: r (#) f is_differentiable_on Z by A1, Th10; ::_thesis: for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) let x be Real; ::_thesis: ( x in Z implies ((r (#) f) `| Z) . x = r * (diff (f,x)) ) assume A4: x in Z ; ::_thesis: ((r (#) f) `| Z) . x = r * (diff (f,x)) then A5: f is_differentiable_in x by A2, Th10; thus ((r (#) f) `| Z) . x = diff ((r (#) f),x) by A3, A4, Def6 .= r * (diff (f,x)) by A5, Th16 ; ::_thesis: verum end; theorem :: NDIFF_3:20 for F being non trivial RealNormSpace for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0. F ) ) proof let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0. F ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0. F ) ) let f be PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0. F ) ) ) set R = REAL --> (0. F); A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F A2: rng h c= dom (REAL --> (0. F)) by A1; A3: n in NAT by ORDINAL1:def_12; hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2 .= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108 .= 0. F by FUNCOP_1:7, RLVECT_1:10 ; ::_thesis: verum end; then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18; hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum end; then reconsider R = REAL --> (0. F) as RestFunc of F by Def1; set L = REAL --> (0. F); now__::_thesis:_for_p_being_Real_holds_(REAL_-->_(0._F))_._p_=_p_*_(0._F) let p be Real; ::_thesis: (REAL --> (0. F)) . p = p * (0. F) thus (REAL --> (0. F)) . p = 0. F by FUNCOP_1:7 .= p * (0. F) by RLVECT_1:10 ; ::_thesis: verum end; then reconsider L = REAL --> (0. F) as LinearFunc of F by Def2; assume that A4: Z c= dom f and A5: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0. F ) ) consider r being Point of F such that A6: for x being Real st x in Z /\ (dom f) holds f . x = r by A5, PARTFUN2:57; A7: now__::_thesis:_for_x_being_Real_st_x_in_Z_/\_(dom_f)_holds_ f_/._x_=_r let x be Real; ::_thesis: ( x in Z /\ (dom f) implies f /. x = r ) assume A8: x in Z /\ (dom f) ; ::_thesis: f /. x = r then x in dom f by XBOOLE_0:def_4; hence f /. x = f . x by PARTFUN1:def_6 .= r by A8, A6 ; ::_thesis: verum end; A9: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A10: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A11: N c= Z by RCOMP_1:18; A12: N c= dom f by A4, A11, XBOOLE_1:1; A13: x0 in Z /\ (dom f) by A4, A10, XBOOLE_0:def_4; for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A14: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6 .= 0. F by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then x in Z /\ (dom f) by A11, A12, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = r - (f /. x0) by A7 .= r - r by A7, A13 .= 0. F by RLVECT_1:15 .= L . (x - x0) by FUNCOP_1:7 .= (L . (x - x0)) + (R /. (x - x0)) by A14, RLVECT_1:4 ; ::_thesis: verum end; hence f is_differentiable_in x0 by A12, Def3; ::_thesis: verum end; hence A15: f is_differentiable_on Z by A4, Th10; ::_thesis: for x being Real st x in Z holds (f `| Z) . x = 0. F let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) . x0 = 0. F ) assume A16: x0 in Z ; ::_thesis: (f `| Z) . x0 = 0. F then consider N being Neighbourhood of x0 such that A17: N c= Z by RCOMP_1:18; A18: N c= dom f by A4, A17, XBOOLE_1:1; A19: x0 in Z /\ (dom f) by A4, A16, XBOOLE_0:def_4; A20: for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A21: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6 .= 0. F by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then x in Z /\ (dom f) by A17, A18, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = r - (f /. x0) by A7 .= r - r by A7, A19 .= 0. F by RLVECT_1:15 .= L . (x - x0) by FUNCOP_1:7 .= (L . (x - x0)) + (R /. (x - x0)) by A21, RLVECT_1:4 ; ::_thesis: verum end; A22: f is_differentiable_in x0 by A9, A16; thus (f `| Z) . x0 = diff (f,x0) by A15, A16, Def6 .= L . 1 by A22, A18, A20, Def4 .= 0. F by FUNCOP_1:7 ; ::_thesis: verum end; theorem Th21: :: NDIFF_3:21 for F being non trivial RealNormSpace for r, p being Point of F for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) proof let F be non trivial RealNormSpace; ::_thesis: for r, p being Point of F for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) let r, p be Point of F; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) let f be PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) ) set R = REAL --> (0. F); defpred S1[ set ] means \$1 in REAL ; A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F A2: rng h c= dom (REAL --> (0. F)) by A1; A3: n in NAT by ORDINAL1:def_12; hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2 .= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108 .= 0. F by FUNCOP_1:7, RLVECT_1:10 ; ::_thesis: verum end; then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18; hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum end; then reconsider R = REAL --> (0. F) as RestFunc of F by Def1; assume that A4: Z c= dom f and A5: for x being Real st x in Z holds f /. x = (x * r) + p ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) deffunc H1( Real) -> Element of the carrier of F = \$1 * r; consider L being PartFunc of REAL, the carrier of F such that A6: ( ( for x being Real holds ( x in dom L iff S1[x] ) ) & ( for x being Real st x in dom L holds L . x = H1(x) ) ) from SEQ_1:sch_3(); dom L = REAL by A6, FDIFF_1:1; then A7: L is total by PARTFUN1:def_2; A8: now__::_thesis:_for_x_being_Real_holds_L_._x_=_x_*_r let x be Real; ::_thesis: L . x = x * r thus L . x = x * r by A6; ::_thesis: verum end; then reconsider L = L as LinearFunc of F by A7, Def2; A9: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A10: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A11: N c= Z by RCOMP_1:18; A12: for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A13: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6 .= 0. F by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = ((x * r) + p) - (f /. x0) by A5, A11 .= ((x * r) + p) - ((x0 * r) + p) by A5, A10 .= (((x * r) + p) - (x0 * r)) - p by RLVECT_1:27 .= (p + ((x * r) - (x0 * r))) - p by RLVECT_1:28 .= ((x * r) - (x0 * r)) + (p - p) by RLVECT_1:28 .= ((x * r) - (x0 * r)) + (0. F) by RLVECT_1:15 .= ((x - x0) * r) + (0. F) by RLVECT_1:35 .= (L . (x - x0)) + (R /. (x - x0)) by A13, A8 ; ::_thesis: verum end; N c= dom f by A4, A11, XBOOLE_1:1; hence f is_differentiable_in x0 by A12, Def3; ::_thesis: verum end; hence A14: f is_differentiable_on Z by A4, Th10; ::_thesis: for x being Real st x in Z holds (f `| Z) . x = r let x0 be Real; ::_thesis: ( x0 in Z implies (f `| Z) . x0 = r ) assume A15: x0 in Z ; ::_thesis: (f `| Z) . x0 = r then consider N being Neighbourhood of x0 such that A16: N c= Z by RCOMP_1:18; A17: for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A18: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6 .= 0. F by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = ((x * r) + p) - (f /. x0) by A5, A16 .= ((x * r) + p) - ((x0 * r) + p) by A5, A15 .= (((x * r) + p) - (x0 * r)) - p by RLVECT_1:27 .= (p + ((x * r) - (x0 * r))) - p by RLVECT_1:28 .= ((x * r) - (x0 * r)) + (p - p) by RLVECT_1:28 .= ((x * r) - (x0 * r)) + (0. F) by RLVECT_1:15 .= ((x - x0) * r) + (0. F) by RLVECT_1:35 .= (L . (x - x0)) + (R /. (x - x0)) by A18, A8 ; ::_thesis: verum end; A19: N c= dom f by A4, A16, XBOOLE_1:1; A20: f is_differentiable_in x0 by A9, A15; thus (f `| Z) . x0 = diff (f,x0) by A14, A15, Def6 .= L . 1 by A20, A19, A17, Def4 .= 1 * r by A8 .= r by RLVECT_1:def_8 ; ::_thesis: verum end; theorem Th22: :: NDIFF_3:22 for F being non trivial RealNormSpace for f being PartFunc of REAL, the carrier of F for x0 being Real st f is_differentiable_in x0 holds f is_continuous_in x0 proof let F be non trivial RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of F for x0 being Real st f is_differentiable_in x0 holds f is_continuous_in x0 let f be PartFunc of REAL, the carrier of F; ::_thesis: for x0 being Real st f is_differentiable_in x0 holds f is_continuous_in x0 let x0 be Real; ::_thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 ) assume A1: f is_differentiable_in x0 ; ::_thesis: f is_continuous_in x0 then consider N being Neighbourhood of x0 such that A2: N c= dom f and ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3; A3: x0 in N by RCOMP_1:16; now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_=_x0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_x0_)_holds_ (_f_/*_s1_is_convergent_&_f_/._x0_=_lim_(f_/*_s1)_) consider g being real number such that A4: 0 < g and A5: N = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6; reconsider s2 = NAT --> x0 as Real_Sequence ; let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) assume that A6: rng s1 c= dom f and A7: s1 is convergent and A8: lim s1 = x0 and A9: for n being Element of NAT holds s1 . n <> x0 ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) consider l being Element of NAT such that A10: for m being Element of NAT st l <= m holds abs ((s1 . m) - x0) < g by A7, A8, A4, SEQ_2:def_7; reconsider c = s2 ^\ l as constant Real_Sequence ; deffunc H1( Real) -> Element of REAL = (s1 . \$1) - (s2 . \$1); consider s3 being Real_Sequence such that A11: for n being Element of NAT holds s3 . n = H1(n) from SEQ_1:sch_1(); A12: s3 = s1 - s2 by A11, RFUNCT_2:1; then A13: s3 is convergent by A7, SEQ_2:11; A14: rng c = {x0} proof thus rng c c= {x0} :: according to XBOOLE_0:def_10 ::_thesis: {x0} c= rng c proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in {x0} ) assume y in rng c ; ::_thesis: y in {x0} then consider n being Element of NAT such that A15: y = (s2 ^\ l) . n by FUNCT_2:113; y = s2 . (n + l) by A15, NAT_1:def_3; then y = x0 by FUNCOP_1:7; hence y in {x0} by TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x0} or y in rng c ) assume y in {x0} ; ::_thesis: y in rng c then A16: y = x0 by TARSKI:def_1; reconsider z0 = 0 as Element of NAT ; c . z0 = s2 . (z0 + l) by NAT_1:def_3 .= y by A16, FUNCOP_1:7 ; hence y in rng c by VALUED_0:28; ::_thesis: verum end; A17: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((f_/*_c)_._m)_-_(f_/._x0)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((f /* c) . m) - (f /. x0)).|| < p ) assume A18: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((f /* c) . m) - (f /. x0)).|| < p take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds ||.(((f /* c) . m) - (f /. x0)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p ) assume n <= m ; ::_thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p x0 in N by RCOMP_1:16; then rng c c= dom f by A2, A14, ZFMISC_1:31; then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109 .= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def_3 .= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1:7 .= ||.(0. F).|| by RLVECT_1:15 .= 0 ; hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A18; ::_thesis: verum end; then A19: f /* c is convergent by NORMSP_1:def_6; lim s2 = s2 . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; then lim s3 = x0 - x0 by A7, A8, A12, SEQ_2:12 .= 0 ; then A20: lim (s3 ^\ l) = 0 by A13, SEQ_4:20; A21: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s3_._n_=_0 given n being Element of NAT such that A22: s3 . n = 0 ; ::_thesis: contradiction (s1 . n) - (s2 . n) = 0 by A11, A22; hence contradiction by A9, FUNCOP_1:7; ::_thesis: verum end; A23: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(s3_^\_l)_._n_=_0 given n being Element of NAT such that A24: (s3 ^\ l) . n = 0 ; ::_thesis: contradiction s3 . (n + l) = 0 by A24, NAT_1:def_3; hence contradiction by A21; ::_thesis: verum end; then s3 ^\ l is non-zero by SEQ_1:5; then reconsider h = s3 ^\ l as non-zero 0 -convergent Real_Sequence by A13, A20, FDIFF_1:def_1; now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_/*_(h_+_c))_-_(f_/*_c))_+_(f_/*_c))_._n_=_(f_/*_(h_+_c))_._n let n be Element of NAT ; ::_thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by NORMSP_1:def_2 .= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by NORMSP_1:def_3 .= ((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n)) by RLVECT_1:29 .= ((f /* (h + c)) . n) - (0. F) by RLVECT_1:15 .= (f /* (h + c)) . n by RLVECT_1:13 ; ::_thesis: verum end; then A25: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63; now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_+_c)_._n_=_(s1_^\_l)_._n let n be Element of NAT ; ::_thesis: (h + c) . n = (s1 ^\ l) . n thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A12, SEQM_3:15 .= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3 .= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by SEQ_1:7 .= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by RFUNCT_2:1 .= (s1 ^\ l) . n by NAT_1:def_3 ; ::_thesis: verum end; then A26: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A25, FUNCT_2:63 .= (f /* s1) ^\ l by A6, VALUED_0:27 ; now__::_thesis:_for_y_being_set_st_y_in_rng_(h_+_c)_holds_ y_in_N let y be set ; ::_thesis: ( y in rng (h + c) implies y in N ) assume y in rng (h + c) ; ::_thesis: y in N then consider n being Element of NAT such that A27: y = (h + c) . n by FUNCT_2:113; (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A12, SEQM_3:15 .= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3 .= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by SEQ_1:7 .= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by RFUNCT_2:1 .= s1 . (l + n) ; then abs (((h + c) . n) - x0) < g by A10, NAT_1:12; hence y in N by A5, A27, RCOMP_1:1; ::_thesis: verum end; then A28: rng (h + c) c= N by TARSKI:def_3; A29: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A20, A1, A2, A14, Th13, A28, NDIFF_1:14 .= 0. F by RLVECT_1:10 ; now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_(#)_((h_")_(#)_((f_/*_(h_+_c))_-_(f_/*_c))))_._n_=_((f_/*_(h_+_c))_-_(f_/*_c))_._n let n be Element of NAT ; ::_thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n A30: h . n <> 0 by A23; thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by NDIFF_1:def_2 .= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by NDIFF_1:def_2 .= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10 .= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n) by RLVECT_1:def_7 .= 1 * (((f /* (h + c)) - (f /* c)) . n) by A30, XCMPLX_0:def_7 .= ((f /* (h + c)) - (f /* c)) . n by RLVECT_1:def_8 ; ::_thesis: verum end; then A31: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63; then A32: (f /* (h + c)) - (f /* c) is convergent by A28, A1, A2, A14, Th13, NDIFF_1:13; then ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A19, NORMSP_1:19; hence f /* s1 is convergent by A26, LOPBAN_3:10; ::_thesis: f /. x0 = lim (f /* s1) lim (f /* c) = f /. x0 by A17, A19, NORMSP_1:def_7; then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. F) + (f /. x0) by A29, A31, A32, A19, NORMSP_1:25 .= f /. x0 by RLVECT_1:4 ; hence f /. x0 = lim (f /* s1) by A32, A26, A19, LOPBAN_3:11, NORMSP_1:19; ::_thesis: verum end; hence f is_continuous_in x0 by A3, A2, NFCONT_3:7; ::_thesis: verum end; theorem :: NDIFF_3:23 for F being non trivial RealNormSpace for X being set for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds f | X is continuous proof let F be non trivial RealNormSpace; ::_thesis: for X being set for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds f | X is continuous let X be set ; ::_thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds f | X is continuous let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on X implies f | X is continuous ) assume A1: f is_differentiable_on X ; ::_thesis: f | X is continuous now__::_thesis:_for_x_being_real_number_st_x_in_dom_(f_|_X)_holds_ f_|_X_is_continuous_in_x let x be real number ; ::_thesis: ( x in dom (f | X) implies f | X is_continuous_in x ) assume x in dom (f | X) ; ::_thesis: f | X is_continuous_in x then ( x is Real & x in X ) by XREAL_0:def_1; then A2: f | X is_differentiable_in x by A1, Def5; x is Real by XREAL_0:def_1; hence f | X is_continuous_in x by A2, Th22; ::_thesis: verum end; hence f | X is continuous by NFCONT_3:def_2; ::_thesis: verum end; theorem Th24: :: NDIFF_3:24 for F being non trivial RealNormSpace for X being set for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z proof let F be non trivial RealNormSpace; ::_thesis: for X being set for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let X be set ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let f be PartFunc of REAL, the carrier of F; ::_thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z ) assume that A1: f is_differentiable_on X and A2: Z c= X ; ::_thesis: f is_differentiable_on Z X c= dom f by A1, Def5; then A3: Z c= dom f by A2, XBOOLE_1:1; now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ f_|_Z_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 ) assume A4: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0 then f | X is_differentiable_in x0 by A1, A2, Def5; then consider N being Neighbourhood of x0 such that A5: N c= dom (f | X) and A6: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3; consider N1 being Neighbourhood of x0 such that A7: N1 c= Z by A4, RCOMP_1:18; consider N2 being Neighbourhood of x0 such that A8: N2 c= N and A9: N2 c= N1 by RCOMP_1:17; A10: N2 c= Z by A7, A9, XBOOLE_1:1; dom (f | X) = (dom f) /\ X by RELAT_1:61; then dom (f | X) c= dom f by XBOOLE_1:17; then N c= dom f by A5, XBOOLE_1:1; then N2 c= dom f by A8, XBOOLE_1:1; then N2 c= (dom f) /\ Z by A10, XBOOLE_1:19; then A11: N2 c= dom (f | Z) by RELAT_1:61; A12: N2 c= dom (f | X) by A8, A5, XBOOLE_1:1; consider L being LinearFunc of F, R being RestFunc of F such that A13: for x being Real st x in N holds ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6; for x being Real st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) assume A14: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) then A15: ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8, A13; A16: x0 in N2 by RCOMP_1:16; ((f | X) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A15, A16, A12, PARTFUN2:15; then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A14, A12, PARTFUN2:15; then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A16, A11, PARTFUN2:15; hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A14, A11, PARTFUN2:15; ::_thesis: verum end; hence f | Z is_differentiable_in x0 by Def3, A11; ::_thesis: verum end; hence f is_differentiable_on Z by Def5, A3; ::_thesis: verum end; Lm1: {} REAL is closed proof let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= {} REAL or not a is convergent or lim a in {} REAL ) assume ( rng a c= {} REAL & a is convergent ) ; ::_thesis: lim a in {} REAL hence lim a in {} REAL ; ::_thesis: verum end; theorem :: NDIFF_3:25 for F being non trivial RealNormSpace ex R being RestFunc of F st ( R /. 0 = 0. F & R is_continuous_in 0 ) proof let F be non trivial RealNormSpace; ::_thesis: ex R being RestFunc of F st ( R /. 0 = 0. F & R is_continuous_in 0 ) ( ([#] REAL) ` = {} REAL & REAL c= REAL & [#] REAL = REAL ) by XBOOLE_1:37; then reconsider Z = [#] REAL as open Subset of REAL by Lm1, RCOMP_1:def_5; set R = REAL --> (0. F); reconsider f = REAL --> (0. F) as PartFunc of REAL, the carrier of F ; A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((REAL_-->_(0._F))_/*_h)_is_convergent_&_lim_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_=_0._F_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_((REAL_-->_(0._F))_/*_h))_._n_=_0._F let n be Nat; ::_thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F A2: rng h c= dom (REAL --> (0. F)) by A1; A3: n in NAT by ORDINAL1:def_12; hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def_2 .= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108 .= 0. F by FUNCOP_1:7, RLVECT_1:10 ; ::_thesis: verum end; then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def_18; hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; ::_thesis: verum end; then reconsider R = REAL --> (0. F) as RestFunc of F by Def1; set L = REAL --> (0. F); now__::_thesis:_for_p_being_Real_holds_(REAL_-->_(0._F))_._p_=_p_*_(0._F) let p be Real; ::_thesis: (REAL --> (0. F)) . p = p * (0. F) thus (REAL --> (0. F)) . p = 0. F by FUNCOP_1:7 .= p * (0. F) by RLVECT_1:10 ; ::_thesis: verum end; then reconsider L = REAL --> (0. F) as LinearFunc of F by Def2; A4: Z c= dom f by FUNCOP_1:13; A5: f | Z is constant ; consider r being Point of F such that A6: for x being Real st x in Z /\ (dom f) holds f . x = r by A5, PARTFUN2:57; A7: now__::_thesis:_for_x_being_Real_st_x_in_Z_/\_(dom_f)_holds_ f_/._x_=_r let x be Real; ::_thesis: ( x in Z /\ (dom f) implies f /. x = r ) assume A8: x in Z /\ (dom f) ; ::_thesis: f /. x = r then x in dom f by XBOOLE_0:def_4; hence f /. x = f . x by PARTFUN1:def_6 .= r by A8, A6 ; ::_thesis: verum end; A9: now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: f is_differentiable_in x0 set N = the Neighbourhood of x0; A10: the Neighbourhood of x0 c= dom f by A4, XBOOLE_1:1; for x being Real st x in the Neighbourhood of x0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in the Neighbourhood of x0 implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A11: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def_6 .= 0. F by FUNCOP_1:7 ; assume x in the Neighbourhood of x0 ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then x in Z /\ (dom f) by A10, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = r - (f /. x0) by A7 .= r - r by A7, A1 .= 0. F by RLVECT_1:15 .= L . (x - x0) by FUNCOP_1:7 .= (L . (x - x0)) + (R /. (x - x0)) by A11, RLVECT_1:4 ; ::_thesis: verum end; hence f is_differentiable_in x0 by A10, Def3; ::_thesis: verum end; set x0 = the Real; f is_differentiable_in the Real by A9; then consider N being Neighbourhood of the Real such that N c= dom f and A12: ex L being LinearFunc of F ex R being RestFunc of F st for x being Real st x in N holds (f /. x) - (f /. the Real) = (L . (x - the Real)) + (R /. (x - the Real)) by Def3; consider L being LinearFunc of F, R being RestFunc of F such that A13: for x being Real st x in N holds (f /. x) - (f /. the Real) = (L . (x - the Real)) + (R /. (x - the Real)) by A12; take R ; ::_thesis: ( R /. 0 = 0. F & R is_continuous_in 0 ) consider p being Point of F such that A14: for r being Real holds L . r = r * p by Def2; (f /. the Real) - (f /. the Real) = (L . ( the Real - the Real)) + (R /. ( the Real - the Real)) by A13, RCOMP_1:16; then 0. F = (L . ( the Real - the Real)) + (R /. ( the Real - the Real)) by RLVECT_1:15; then 0. F = (0 * p) + (R /. 0) by A14; then 0. F = (0. F) + (R /. 0) by RLVECT_1:10; hence A15: R /. 0 = 0. F by RLVECT_1:4; ::_thesis: R is_continuous_in 0 A16: now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_R_/*_h_is_convergent_&_lim_(R_/*_h)_=_R_/._0_) set s3 = cs; let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( R /* h is convergent & lim (R /* h) = R /. 0 ) A17: cs . 1 = 0 by FUNCOP_1:7; ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. F ) by Def1; then ||.((h ") (#) (R /* h)).|| is bounded by LOPBAN_1:20, SEQ_2:13; then consider M being real number such that M > 0 and A18: for n being Element of NAT holds abs (||.((h ") (#) (R /* h)).|| . n) < M by SEQ_2:3; A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(((h_")_(#)_(R_/*_h))_._n).||_<_M let n be Element of NAT ; ::_thesis: ||.(((h ") (#) (R /* h)) . n).|| < M abs (||.((h ") (#) (R /* h)).|| . n) < M by A18; then abs ||.(((h ") (#) (R /* h)) . n).|| < M by NORMSP_0:def_4; hence ||.(((h ") (#) (R /* h)) . n).|| < M by ABSVALUE:def_1; ::_thesis: verum end; reconsider z0 = 0 as Real ; A20: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((R_/*_h)_._n).||_<=_(M_(#)_(abs_h))_._n let n be Element of NAT ; ::_thesis: ||.((R /* h) . n).|| <= (M (#) (abs h)) . n ||.(((h ") (#) (R /* h)) . n).|| = ||.(((h ") . n) * ((R /* h) . n)).|| by NDIFF_1:def_2 .= ||.(((h . n) ") * ((R /* h) . n)).|| by VALUED_1:10 ; then A21: ||.(((h . n) ") * ((R /* h) . n)).|| <= M by A19; abs (h . n) >= 0 by COMPLEX1:46; then (abs (h . n)) * ||.(((h . n) ") * ((R /* h) . n)).|| <= M * (abs (h . n)) by A21, XREAL_1:64; then ||.((h . n) * (((h . n) ") * ((R /* h) . n))).|| <= M * (abs (h . n)) by NORMSP_1:def_1; then A22: ||.(((h . n) * ((h . n) ")) * ((R /* h) . n)).|| <= M * (abs (h . n)) by RLVECT_1:def_7; h . n <> 0 by SEQ_1:5; then ||.(1 * ((R /* h) . n)).|| <= M * (abs (h . n)) by A22, XCMPLX_0:def_7; then ||.((R /* h) . n).|| <= M * (abs (h . n)) by RLVECT_1:def_8; then ||.((R /* h) . n).|| <= M * ((abs h) . n) by SEQ_1:12; hence ||.((R /* h) . n).|| <= (M (#) (abs h)) . n by SEQ_1:9; ::_thesis: verum end; lim h = z0 ; then lim (abs h) = abs z0 by SEQ_4:14 .= z0 by ABSVALUE:2 ; then A23: lim (M (#) (abs h)) = M * z0 by SEQ_2:8 .= lim cs by A17, SEQ_4:25 ; A24: M (#) (abs h) is convergent by SEQ_2:7; reconsider z0 = 0 as Real ; lim (M (#) (abs h)) = 0 by A23, A17, SEQ_4:25; hence ( R /* h is convergent & lim (R /* h) = R /. 0 ) by A15, A24, A20, Th1; ::_thesis: verum end; R is total by Def1; then A25: dom R = REAL by FUNCT_2:def_1; now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_R_&_s1_is_convergent_&_lim_s1_=_0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_0_)_holds_ (_R_/*_s1_is_convergent_&_R_/._0_=_lim_(R_/*_s1)_) let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Element of NAT holds s1 . n <> 0 ) implies ( R /* s1 is convergent & R /. 0 = lim (R /* s1) ) ) assume that rng s1 c= dom R and A26: ( s1 is convergent & lim s1 = 0 ) and A27: for n being Element of NAT holds s1 . n <> 0 ; ::_thesis: ( R /* s1 is convergent & R /. 0 = lim (R /* s1) ) s1 is non-zero by A27, SEQ_1:5; then s1 is non-zero 0 -convergent Real_Sequence by A26, FDIFF_1:def_1; hence ( R /* s1 is convergent & R /. 0 = lim (R /* s1) ) by A16; ::_thesis: verum end; hence R is_continuous_in 0 by A25, NFCONT_3:7; ::_thesis: verum end; definition let F be non trivial RealNormSpace; let f be PartFunc of REAL, the carrier of F; attrf is differentiable means :Def7: :: NDIFF_3:def 7 f is_differentiable_on dom f; end; :: deftheorem Def7 defines differentiable NDIFF_3:def_7_:_ for F being non trivial RealNormSpace for f being PartFunc of REAL, the carrier of F holds ( f is differentiable iff f is_differentiable_on dom f ); Lm2: [#] REAL is open proof ([#] REAL) ` = {} REAL by XBOOLE_1:37; hence [#] REAL is open by Lm1, RCOMP_1:def_5; ::_thesis: verum end; registration let F be non trivial RealNormSpace; clusterV1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total differentiable for Element of K6(K7(REAL, the carrier of F)); existence ex b1 being Function of REAL, the carrier of F st b1 is differentiable proof reconsider Z = REAL as open Subset of REAL by Lm2; reconsider f = REAL --> (0. F) as Function of REAL, the carrier of F ; take f ; ::_thesis: f is differentiable A1: Z = dom f by FUNCT_2:def_1; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ f_/._x_=_(x_*_(0._F))_+_(0._F) let x be Real; ::_thesis: ( x in Z implies f /. x = (x * (0. F)) + (0. F) ) assume x in Z ; ::_thesis: f /. x = (x * (0. F)) + (0. F) thus f /. x = 0. F by FUNCOP_1:7 .= x * (0. F) by RLVECT_1:10 .= (x * (0. F)) + (0. F) by RLVECT_1:4 ; ::_thesis: verum end; then f is_differentiable_on Z by A1, Th21; hence f is differentiable by A1, Def7; ::_thesis: verum end; end; theorem :: NDIFF_3:26 for F being non trivial RealNormSpace for Z being open Subset of REAL for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds f is_differentiable_on Z proof let F be non trivial RealNormSpace; ::_thesis: for Z being open Subset of REAL for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds f is_differentiable_on Z let Z be open Subset of REAL; ::_thesis: for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds f is_differentiable_on Z let f be differentiable PartFunc of REAL, the carrier of F; ::_thesis: ( Z c= dom f implies f is_differentiable_on Z ) assume A1: Z c= dom f ; ::_thesis: f is_differentiable_on Z f is_differentiable_on dom f by Def7; hence f is_differentiable_on Z by A1, Th24; ::_thesis: verum end;