:: CFDIFF_1 semantic presentation begin definition let x be real number ; let IT be Complex_Sequence; attrIT is x -convergent means :Def1: :: CFDIFF_1:def 1 ( IT is convergent & lim IT = x ); end; :: deftheorem Def1 defines -convergent CFDIFF_1:def_1_:_ for x being real number for IT being Complex_Sequence holds ( IT is x -convergent iff ( IT is convergent & lim IT = x ) ); theorem :: CFDIFF_1:1 for rs being Real_Sequence for cs being Complex_Sequence st rs = cs & rs is convergent holds cs is convergent ; definition let r be real number ; func InvShift r -> Complex_Sequence means :Def2: :: CFDIFF_1:def 2 for n being Element of NAT holds it . n = 1 / (n + r); existence ex b1 being Complex_Sequence st for n being Element of NAT holds b1 . n = 1 / (n + r) proof deffunc H1( real number ) -> Element of REAL = 1 / ($1 + r); ex seq being Complex_Sequence st for n being Element of NAT holds seq . n = H1(n) from COMSEQ_1:sch_1(); hence ex b1 being Complex_Sequence st for n being Element of NAT holds b1 . n = 1 / (n + r) ; ::_thesis: verum end; uniqueness for b1, b2 being Complex_Sequence st ( for n being Element of NAT holds b1 . n = 1 / (n + r) ) & ( for n being Element of NAT holds b2 . n = 1 / (n + r) ) holds b1 = b2 proof let f, g be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds f . n = 1 / (n + r) ) & ( for n being Element of NAT holds g . n = 1 / (n + r) ) implies f = g ) assume that A1: for n being Element of NAT holds f . n = 1 / (n + r) and A2: for n being Element of NAT holds g . n = 1 / (n + r) ; ::_thesis: f = g let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: f . n = g . n thus f . n = 1 / (n + r) by A1 .= g . n by A2 ; ::_thesis: verum end; end; :: deftheorem Def2 defines InvShift CFDIFF_1:def_2_:_ for r being real number for b2 being Complex_Sequence holds ( b2 = InvShift r iff for n being Element of NAT holds b2 . n = 1 / (n + r) ); theorem Th2: :: CFDIFF_1:2 for r being real number st 0 < r holds InvShift r is convergent proof let r be real number ; ::_thesis: ( 0 < r implies InvShift r is convergent ) assume A1: 0 < r ; ::_thesis: InvShift r is convergent set seq = InvShift r; take g = 0c ; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= |.(((InvShift r) . b3) - g).| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= |.(((InvShift r) . b2) - g).| ) ) assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= |.(((InvShift r) . b2) - g).| ) consider k1 being Element of NAT such that A3: p " < k1 by SEQ_4:3; take n = k1; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= |.(((InvShift r) . b1) - g).| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.(((InvShift r) . m) - g).| ) assume n <= m ; ::_thesis: not p <= |.(((InvShift r) . m) - g).| then n + r <= m + r by XREAL_1:6; then A4: 1 / (m + r) <= 1 / (n + r) by A1, XREAL_1:118; A5: (InvShift r) . m = 1 / (m + r) by Def2; (p ") + 0 < k1 + r by A1, A3, XREAL_1:8; then 1 / (k1 + r) < 1 / (p ") by A2, XREAL_1:76; then 1 / (m + r) < p by A4, XXREAL_0:2; hence abs (((InvShift r) . m) - g) < p by A1, A5, ABSVALUE:def_1; ::_thesis: verum end; registration let r be real positive number ; cluster InvShift r -> convergent ; coherence InvShift r is convergent by Th2; end; theorem Th3: :: CFDIFF_1:3 for r being real number st 0 < r holds lim (InvShift r) = 0 proof let r be real number ; ::_thesis: ( 0 < r implies lim (InvShift r) = 0 ) set seq = InvShift r; assume A1: 0 < r ; ::_thesis: lim (InvShift r) = 0 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_ abs_(((InvShift_r)_._m)_-_0c)_<_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 abs (((InvShift r) . m) - 0c) < p ) assume A2: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((InvShift r) . m) - 0c) < p consider k1 being Element of NAT such that A3: p " < k1 by SEQ_4:3; take n = k1; ::_thesis: for m being Element of NAT st n <= m holds abs (((InvShift r) . m) - 0c) < p let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((InvShift r) . m) - 0c) < p ) assume n <= m ; ::_thesis: abs (((InvShift r) . m) - 0c) < p then n + r <= m + r by XREAL_1:6; then A4: 1 / (m + r) <= 1 / (n + r) by A1, XREAL_1:118; A5: (InvShift r) . m = 1 / (m + r) by Def2; (p ") + 0 < k1 + r by A1, A3, XREAL_1:8; then 1 / (k1 + r) < 1 / (p ") by A2, XREAL_1:76; then 1 / (m + r) < p by A4, XXREAL_0:2; hence abs (((InvShift r) . m) - 0c) < p by A1, A5, ABSVALUE:def_1; ::_thesis: verum end; hence lim (InvShift r) = 0 by A1, COMSEQ_2:def_6; ::_thesis: verum end; registration let r be real positive number ; cluster InvShift r -> non-zero 0 -convergent ; coherence ( InvShift r is non-empty & InvShift r is 0 -convergent ) proof set s = InvShift r; now__::_thesis:_for_n_being_Element_of_NAT_holds_(InvShift_r)_._n_<>_0c let n be Element of NAT ; ::_thesis: (InvShift r) . n <> 0c 1 / (n + r) <> 0 ; hence (InvShift r) . n <> 0c by Def2; ::_thesis: verum end; hence InvShift r is non-zero by COMSEQ_1:4; ::_thesis: InvShift r is 0 -convergent lim (InvShift r) = 0 by Th3; hence InvShift r is 0 -convergent by Def1; ::_thesis: verum end; end; registration clusterV1() non-zero V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued 0 -convergent for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st ( b1 is 0 -convergent & b1 is non-zero ) proof take InvShift 1 ; ::_thesis: ( InvShift 1 is 0 -convergent & InvShift 1 is non-zero ) thus ( InvShift 1 is 0 -convergent & InvShift 1 is non-zero ) ; ::_thesis: verum end; end; registration cluster non-zero Function-like quasi_total 0 -convergent -> convergent for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st b1 is 0 -convergent & b1 is non-zero holds b1 is convergent by Def1; end; reconsider cs = NAT --> 0c as Complex_Sequence ; registration clusterV1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is constant proof take cs ; ::_thesis: cs is constant thus cs is constant ; ::_thesis: verum end; end; theorem :: CFDIFF_1:4 for seq being Complex_Sequence holds ( seq is constant iff for n, m being Element of NAT holds seq . n = seq . m ) proof let seq be Complex_Sequence; ::_thesis: ( seq is constant iff for n, m being Element of NAT holds seq . n = seq . m ) thus ( seq is constant implies for n, m being Element of NAT holds seq . n = seq . m ) by VALUED_0:23; ::_thesis: ( ( for n, m being Element of NAT holds seq . n = seq . m ) implies seq is constant ) assume that A1: for n, m being Element of NAT holds seq . n = seq . m and A2: not seq is constant ; ::_thesis: contradiction now__::_thesis:_for_n_being_Nat_holds_contradiction let n be Nat; ::_thesis: contradiction consider n1 being Nat such that A3: seq . n1 <> seq . n by A2, VALUED_0:def_18; ( n1 in NAT & n in NAT ) by ORDINAL1:def_12; hence contradiction by A1, A3; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; theorem :: CFDIFF_1:5 for seq being Complex_Sequence for Nseq being V37() sequence of NAT for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n) proof let seq be Complex_Sequence; ::_thesis: for Nseq being V37() sequence of NAT for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n) let Nseq be V37() sequence of NAT; ::_thesis: for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n) let n be Element of NAT ; ::_thesis: (seq * Nseq) . n = seq . (Nseq . n) dom (seq * Nseq) = NAT by FUNCT_2:def_1; hence (seq * Nseq) . n = seq . (Nseq . n) by FUNCT_1:12; ::_thesis: verum end; definition let IT be PartFunc of COMPLEX,COMPLEX; attrIT is RestFunc-like means :Def3: :: CFDIFF_1:def 3 for h being non-zero 0 -convergent Complex_Sequence holds ( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ); end; :: deftheorem Def3 defines RestFunc-like CFDIFF_1:def_3_:_ for IT being PartFunc of COMPLEX,COMPLEX holds ( IT is RestFunc-like iff for h being non-zero 0 -convergent Complex_Sequence holds ( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ); reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ; registration clusterV1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued RestFunc-like for Element of K19(K20(COMPLEX,COMPLEX)); existence ex b1 being PartFunc of COMPLEX,COMPLEX st ( b1 is total & b1 is RestFunc-like ) proof take f = cf; ::_thesis: ( f is total & f is RestFunc-like ) thus f is total ; ::_thesis: f is RestFunc-like let h be non-zero 0 -convergent Complex_Sequence; :: according to CFDIFF_1:def_3 ::_thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(f_/*_h))_._n_=_0c let n be Nat; ::_thesis: ((h ") (#) (f /* h)) . n = 0c dom f = COMPLEX by PARTFUN1:def_2; then A1: ( n in NAT & rng h c= dom f ) by ORDINAL1:def_12; thus ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by VALUED_1:5 .= ((h ") . n) * (f /. (h . n)) by A1, FUNCT_2:108 .= ((h ") . n) * 0c by FUNCOP_1:7 .= 0c ; ::_thesis: verum end; then ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0c ) by VALUED_0:def_18; hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum end; end; definition mode C_RestFunc is total RestFunc-like PartFunc of COMPLEX,COMPLEX; end; definition let IT be PartFunc of COMPLEX,COMPLEX; attrIT is linear means :Def4: :: CFDIFF_1:def 4 ex a being Element of COMPLEX st for z being Element of COMPLEX holds IT /. z = a * z; end; :: deftheorem Def4 defines linear CFDIFF_1:def_4_:_ for IT being PartFunc of COMPLEX,COMPLEX holds ( IT is linear iff ex a being Element of COMPLEX st for z being Element of COMPLEX holds IT /. z = a * z ); registration clusterV1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued linear for Element of K19(K20(COMPLEX,COMPLEX)); existence ex b1 being PartFunc of COMPLEX,COMPLEX st ( b1 is total & b1 is linear ) proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = 1r * c1; defpred S1[ set ] means c1 in COMPLEX ; consider f being PartFunc of COMPLEX,COMPLEX such that A1: ( ( for a being Element of COMPLEX holds ( a in dom f iff S1[a] ) ) & ( for a being Element of COMPLEX st a in dom f holds f . a = H1(a) ) ) from SEQ_1:sch_3(); take f ; ::_thesis: ( f is total & f is linear ) for y being set st y in COMPLEX holds y in dom f by A1; then COMPLEX c= dom f by TARSKI:def_3; then A2: dom f = COMPLEX by XBOOLE_0:def_10; hence f is total by PARTFUN1:def_2; ::_thesis: f is linear take 1r ; :: according to CFDIFF_1:def_4 ::_thesis: for z being Element of COMPLEX holds f /. z = 1r * z let z be Element of COMPLEX ; ::_thesis: f /. z = 1r * z thus f /. z = f . z by A2, PARTFUN1:def_6 .= 1r * z by A1 ; ::_thesis: verum end; end; definition mode C_LinearFunc is total linear PartFunc of COMPLEX,COMPLEX; end; registration let L1, L2 be C_LinearFunc; clusterL1 + L2 -> total linear for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 + L2 holds ( b1 is total & b1 is linear ) proof consider a2 being Element of COMPLEX such that A1: for z being Element of COMPLEX holds L2 /. z = a2 * z by Def4; consider a1 being Element of COMPLEX such that A2: for z being Element of COMPLEX holds L1 /. z = a1 * z by Def4; now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_(L1_+_L2)_/._z_=_(a1_+_a2)_*_z let z be Element of COMPLEX ; ::_thesis: (L1 + L2) /. z = (a1 + a2) * z thus (L1 + L2) /. z = (L1 /. z) + (L2 /. z) by CFUNCT_1:64 .= (a1 * z) + (L2 /. z) by A2 .= (a1 * z) + (a2 * z) by A1 .= (a1 + a2) * z ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 + L2 holds ( b1 is total & b1 is linear ) by Def4; ::_thesis: verum end; clusterL1 - L2 -> total linear for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 - L2 holds ( b1 is total & b1 is linear ) proof consider a2 being Element of COMPLEX such that A3: for z being Element of COMPLEX holds L2 /. z = a2 * z by Def4; consider a1 being Element of COMPLEX such that A4: for z being Element of COMPLEX holds L1 /. z = a1 * z by Def4; now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_(L1_-_L2)_/._z_=_(a1_-_a2)_*_z let z be Element of COMPLEX ; ::_thesis: (L1 - L2) /. z = (a1 - a2) * z thus (L1 - L2) /. z = (L1 /. z) - (L2 /. z) by CFUNCT_1:64 .= (a1 * z) - (L2 /. z) by A4 .= (a1 * z) - (a2 * z) by A3 .= (a1 - a2) * z ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 - L2 holds ( b1 is total & b1 is linear ) by Def4; ::_thesis: verum end; end; registration let a be Element of COMPLEX ; let L be C_LinearFunc; clustera (#) L -> total linear for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) L holds ( b1 is total & b1 is linear ) proof consider b being Element of COMPLEX such that A1: for z being Element of COMPLEX holds L /. z = b * z by Def4; now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_(a_(#)_L)_/._z_=_(a_*_b)_*_z let z be Element of COMPLEX ; ::_thesis: (a (#) L) /. z = (a * b) * z thus (a (#) L) /. z = a * (L /. z) by CFUNCT_1:65 .= a * (b * z) by A1 .= (a * b) * z ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) L holds ( b1 is total & b1 is linear ) by Def4; ::_thesis: verum end; end; registration let R1, R2 be C_RestFunc; clusterR1 + R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 + R2 holds ( b1 is total & b1 is RestFunc-like ) proof now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_((R1_+_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_+_R2)_/*_h))_=_0_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R1 + R2) /* h) is convergent & lim ((h ") (#) ((R1 + R2) /* h)) = 0 ) A1: (h ") (#) ((R1 + R2) /* h) = (h ") (#) ((R1 /* h) + (R2 /* h)) by CFCONT_1:14 .= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by COMSEQ_1:10 ; A2: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def3; hence (h ") (#) ((R1 + R2) /* h) is convergent by A1; ::_thesis: lim ((h ") (#) ((R1 + R2) /* h)) = 0 A3: lim ((h ") (#) (R1 /* h)) = 0 by Def3; thus lim ((h ") (#) ((R1 + R2) /* h)) = (lim ((h ") (#) (R1 /* h))) + (lim ((h ") (#) (R2 /* h))) by A2, A1, COMSEQ_2:14 .= 0 by A3, Def3 ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 + R2 holds ( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum end; clusterR1 - R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 - R2 holds ( b1 is total & b1 is RestFunc-like ) proof now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_((R1_-_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_-_R2)_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R1 - R2) /* h) is convergent & lim ((h ") (#) ((R1 - R2) /* h)) = 0c ) A4: (h ") (#) ((R1 - R2) /* h) = (h ") (#) ((R1 /* h) - (R2 /* h)) by CFCONT_1:14 .= ((h ") (#) (R1 /* h)) - ((h ") (#) (R2 /* h)) by COMSEQ_1:15 ; A5: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def3; hence (h ") (#) ((R1 - R2) /* h) is convergent by A4; ::_thesis: lim ((h ") (#) ((R1 - R2) /* h)) = 0c ( lim ((h ") (#) (R1 /* h)) = 0c & lim ((h ") (#) (R2 /* h)) = 0c ) by Def3; hence lim ((h ") (#) ((R1 - R2) /* h)) = 0c - 0c by A5, A4, COMSEQ_2:26 .= 0c ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 - R2 holds ( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum end; clusterR1 (#) R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 (#) R2 holds ( b1 is total & b1 is RestFunc-like ) proof now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_((R1_(#)_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_(#)_R2)_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R1 (#) R2) /* h) is convergent & lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c ) for seq being Complex_Sequence st seq is non-zero holds seq " is non-zero proof let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies seq " is non-zero ) assume that A6: seq is non-zero and A7: not seq " is non-zero ; ::_thesis: contradiction consider n1 being Element of NAT such that A8: (seq ") . n1 = 0c by A7, COMSEQ_1:4; (seq . n1) " = (seq ") . n1 by VALUED_1:10; hence contradiction by A6, A8, COMSEQ_1:4, XCMPLX_1:202; ::_thesis: verum end; then A9: h " is non-zero ; A10: (h ") (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by CFCONT_1:14 .= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) /" (h (#) (h ")) by A9, COMSEQ_1:37 .= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) (#) (((h ") ") (#) (h ")) by COMSEQ_1:30 .= (h (#) (h ")) (#) ((R1 /* h) (#) ((h ") (#) (R2 /* h))) by COMSEQ_1:8 .= ((h (#) (h ")) (#) (R1 /* h)) (#) ((h ") (#) (R2 /* h)) by COMSEQ_1:8 .= (h (#) ((h ") (#) (R1 /* h))) (#) ((h ") (#) (R2 /* h)) by COMSEQ_1:8 ; A11: (h ") (#) (R1 /* h) is convergent by Def3; then A12: h (#) ((h ") (#) (R1 /* h)) is convergent ; ( lim ((h ") (#) (R1 /* h)) = 0c & lim h = 0c ) by Def1, Def3; then A13: lim (h (#) ((h ") (#) (R1 /* h))) = 0 * 0 by A11, COMSEQ_2:30 .= 0c ; A14: (h ") (#) (R2 /* h) is convergent by Def3; hence (h ") (#) ((R1 (#) R2) /* h) is convergent by A12, A10; ::_thesis: lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c lim ((h ") (#) (R2 /* h)) = 0c by Def3; hence lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c * 0c by A14, A12, A13, A10, COMSEQ_2:30 .= 0c ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 (#) R2 holds ( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum end; end; registration let a be Element of COMPLEX ; let R be C_RestFunc; clustera (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) R holds ( b1 is total & b1 is RestFunc-like ) proof now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_((a_(#)_R)_/*_h)_is_convergent_&_lim_((h_")_(#)_((a_(#)_R)_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((a (#) R) /* h) is convergent & lim ((h ") (#) ((a (#) R) /* h)) = 0c ) A1: (h ") (#) ((a (#) R) /* h) = (h ") (#) (a (#) (R /* h)) by CFCONT_1:15 .= a (#) ((h ") (#) (R /* h)) by COMSEQ_1:13 ; A2: (h ") (#) (R /* h) is convergent by Def3; hence (h ") (#) ((a (#) R) /* h) is convergent by A1; ::_thesis: lim ((h ") (#) ((a (#) R) /* h)) = 0c lim ((h ") (#) (R /* h)) = 0c by Def3; hence lim ((h ") (#) ((a (#) R) /* h)) = a * 0c by A2, A1, COMSEQ_2:18 .= 0c ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) R holds ( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum end; end; registration let L1, L2 be C_LinearFunc; clusterL1 (#) L2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 (#) L2 holds ( b1 is total & b1 is RestFunc-like ) proof reconsider LL = L1 (#) L2 as PartFunc of COMPLEX,COMPLEX ; LL is RestFunc-like proof let h be non-zero 0 -convergent Complex_Sequence; :: according to CFDIFF_1:def_3 ::_thesis: ( (h ") (#) (LL /* h) is convergent & lim ((h ") (#) (LL /* h)) = 0 ) consider b1 being Element of COMPLEX such that A1: for z being Element of COMPLEX holds L1 /. z = b1 * z by Def4; consider b2 being Element of COMPLEX such that A2: for z being Element of COMPLEX holds L2 /. z = b2 * z by Def4; A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_")_(#)_((L1_(#)_L2)_/*_h))_._n_=_((b1_*_b2)_(#)_h)_._n let n be Element of NAT ; ::_thesis: ((h ") (#) ((L1 (#) L2) /* h)) . n = ((b1 * b2) (#) h) . n A4: h . n <> 0c by COMSEQ_1:4; thus ((h ") (#) ((L1 (#) L2) /* h)) . n = ((h ") . n) * (((L1 (#) L2) /* h) . n) by VALUED_1:5 .= ((h ") . n) * ((L1 (#) L2) /. (h . n)) by FUNCT_2:115 .= ((h ") . n) * ((L1 /. (h . n)) * (L2 /. (h . n))) by CFUNCT_1:64 .= (((h ") . n) * (L1 /. (h . n))) * (L2 /. (h . n)) .= (((h . n) ") * (L1 /. (h . n))) * (L2 /. (h . n)) by VALUED_1:10 .= (((h . n) ") * ((h . n) * b1)) * (L2 /. (h . n)) by A1 .= ((((h . n) ") * (h . n)) * b1) * (L2 /. (h . n)) .= (1r * b1) * (L2 /. (h . n)) by A4, XCMPLX_0:def_7 .= b1 * (b2 * (h . n)) by A2 .= (b1 * b2) * (h . n) .= ((b1 * b2) (#) h) . n by VALUED_1:6 ; ::_thesis: verum end; then A5: (h ") (#) ((L1 (#) L2) /* h) = (b1 * b2) (#) h by FUNCT_2:63; thus (h ") (#) (LL /* h) is convergent by A3, FUNCT_2:63; ::_thesis: lim ((h ") (#) (LL /* h)) = 0 lim h = 0c by Def1; hence lim ((h ") (#) (LL /* h)) = (b1 * b2) * 0c by A5, COMSEQ_2:18 .= 0c ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 (#) L2 holds ( b1 is total & b1 is RestFunc-like ) ; ::_thesis: verum end; end; registration let R be C_RestFunc; let L be C_LinearFunc; clusterR (#) L -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R (#) L holds ( b1 is total & b1 is RestFunc-like ) proof consider b1 being Element of COMPLEX such that A1: for z being Element of COMPLEX holds L /. z = b1 * z by Def4; now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_((R_(#)_L)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R_(#)_L)_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R (#) L) /* h) is convergent & lim ((h ") (#) ((R (#) L) /* h)) = 0c ) A2: (h ") (#) ((R (#) L) /* h) = (h ") (#) ((R /* h) (#) (L /* h)) by CFCONT_1:14 .= ((h ") (#) (R /* h)) (#) (L /* h) by COMSEQ_1:8 ; now__::_thesis:_for_n_being_Element_of_NAT_holds_(L_/*_h)_._n_=_(b1_(#)_h)_._n let n be Element of NAT ; ::_thesis: (L /* h) . n = (b1 (#) h) . n thus (L /* h) . n = L /. (h . n) by FUNCT_2:115 .= b1 * (h . n) by A1 .= (b1 (#) h) . n by VALUED_1:6 ; ::_thesis: verum end; then A3: L /* h = b1 (#) h by FUNCT_2:63; lim h = 0c by Def1; then A4: lim (L /* h) = b1 * 0c by A3, COMSEQ_2:18 .= 0c ; A5: (h ") (#) (R /* h) is convergent by Def3; hence (h ") (#) ((R (#) L) /* h) is convergent by A2, A3; ::_thesis: lim ((h ") (#) ((R (#) L) /* h)) = 0c lim ((h ") (#) (R /* h)) = 0c by Def3; hence lim ((h ") (#) ((R (#) L) /* h)) = 0c * 0c by A2, A3, A4, A5, COMSEQ_2:30 .= 0c ; ::_thesis: verum end; hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R (#) L holds ( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum end; clusterL (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L (#) R holds ( b1 is total & b1 is RestFunc-like ) ; end; definition let z0 be Complex; mode Neighbourhood of z0 -> Subset of COMPLEX means :Def5: :: CFDIFF_1:def 5 ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= it ); existence ex b1 being Subset of COMPLEX ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b1 ) proof set N = { y where y is Complex : |.(y - z0).| < 1 } ; take { y where y is Complex : |.(y - z0).| < 1 } ; ::_thesis: ( { y where y is Complex : |.(y - z0).| < 1 } is Subset of COMPLEX & ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= { y where y is Complex : |.(y - z0).| < 1 } ) ) { y where y is Complex : |.(y - z0).| < 1 } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < 1 } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z0).| < 1 } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z0).| < 1 ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; hence ( { y where y is Complex : |.(y - z0).| < 1 } is Subset of COMPLEX & ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= { y where y is Complex : |.(y - z0).| < 1 } ) ) ; ::_thesis: verum end; end; :: deftheorem Def5 defines Neighbourhood CFDIFF_1:def_5_:_ for z0 being Complex for b2 being Subset of COMPLEX holds ( b2 is Neighbourhood of z0 iff ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b2 ) ); theorem Th6: :: CFDIFF_1:6 for z0 being Element of COMPLEX for g being real number st 0 < g holds { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 proof let z0 be Element of COMPLEX ; ::_thesis: for g being real number st 0 < g holds { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 let g be real number ; ::_thesis: ( 0 < g implies { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 ) assume A1: g > 0 ; ::_thesis: { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 set N = { y where y is Complex : |.(y - z0).| < g } ; A2: { y where y is Complex : |.(y - z0).| < g } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < g } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z0).| < g } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z0).| < g ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; g in REAL by XREAL_0:def_1; hence { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A1, A2, Def5; ::_thesis: verum end; theorem Th7: :: CFDIFF_1:7 for z0 being Element of COMPLEX for N being Neighbourhood of z0 holds z0 in N proof let z0 be Element of COMPLEX ; ::_thesis: for N being Neighbourhood of z0 holds z0 in N let N be Neighbourhood of z0; ::_thesis: z0 in N consider g being Real such that A1: 0 < g and A2: { z where z is Complex : |.(z - z0).| < g } c= N by Def5; |.(z0 - z0).| = 0 by COMPLEX1:44; then z0 in { z where z is Complex : |.(z - z0).| < g } by A1; hence z0 in N by A2; ::_thesis: verum end; Lm1: for z0 being Complex for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st ( N c= N1 & N c= N2 ) proof let z0 be Complex; ::_thesis: for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st ( N c= N1 & N c= N2 ) A1: z0 in COMPLEX by XCMPLX_0:def_2; let N1, N2 be Neighbourhood of z0; ::_thesis: ex N being Neighbourhood of z0 st ( N c= N1 & N c= N2 ) consider a1 being Real such that A2: 0 < a1 and A3: { y where y is Complex : |.(y - z0).| < a1 } c= N1 by Def5; consider a2 being Real such that A4: 0 < a2 and A5: { y where y is Complex : |.(y - z0).| < a2 } c= N2 by Def5; set g = min (a1,a2); take { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; ::_thesis: ( { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Subset of COMPLEX & { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Neighbourhood of z0 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N1 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N2 ) A6: min (a1,a2) <= a2 by XXREAL_0:17; A7: { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= { y where y is Complex : |.(y - z0).| < a2 } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } or z in { y where y is Complex : |.(y - z0).| < a2 } ) assume z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; ::_thesis: z in { y where y is Complex : |.(y - z0).| < a2 } then consider y being Complex such that A8: z = y and A9: |.(y - z0).| < min (a1,a2) ; |.(y - z0).| < a2 by A6, A9, XXREAL_0:2; hence z in { y where y is Complex : |.(y - z0).| < a2 } by A8; ::_thesis: verum end; A10: min (a1,a2) <= a1 by XXREAL_0:17; A11: { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= { y where y is Complex : |.(y - z0).| < a1 } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } or z in { y where y is Complex : |.(y - z0).| < a1 } ) assume z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; ::_thesis: z in { y where y is Complex : |.(y - z0).| < a1 } then consider y being Complex such that A12: z = y and A13: |.(y - z0).| < min (a1,a2) ; |.(y - z0).| < a1 by A10, A13, XXREAL_0:2; hence z in { y where y is Complex : |.(y - z0).| < a1 } by A12; ::_thesis: verum end; 0 < min (a1,a2) by A2, A4, XXREAL_0:15; hence ( { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Subset of COMPLEX & { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Neighbourhood of z0 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N1 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N2 ) by A1, A3, A5, A11, A7, Th6, XBOOLE_1:1; ::_thesis: verum end; definition let f be PartFunc of COMPLEX,COMPLEX; let z0 be Complex; predf is_differentiable_in z0 means :Def6: :: CFDIFF_1:def 6 ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ); end; :: deftheorem Def6 defines is_differentiable_in CFDIFF_1:def_6_:_ for f being PartFunc of COMPLEX,COMPLEX for z0 being Complex holds ( f is_differentiable_in z0 iff ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ); definition let f be PartFunc of COMPLEX,COMPLEX; let z0 be Complex; assume A1: f is_differentiable_in z0 ; func diff (f,z0) -> Element of COMPLEX means :Def7: :: CFDIFF_1:def 7 ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( it = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ); existence ex b1 being Element of COMPLEX ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b1 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) proof consider N being Neighbourhood of z0 such that A2: N c= dom f and A3: ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A1, Def6; consider L being C_LinearFunc, R being C_RestFunc such that A4: for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A3; consider a being Element of COMPLEX such that A5: for d being Element of COMPLEX holds L /. d = a * d by Def4; take a ; ::_thesis: ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) L /. 1r = a * 1r by A5 .= a ; hence ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) by A2, A4; ::_thesis: verum end; uniqueness for b1, b2 being Element of COMPLEX st ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b1 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) & ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b2 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) holds b1 = b2 proof set s0 = InvShift 2; let a, b be Element of COMPLEX ; ::_thesis: ( ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) & ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) implies a = b ) assume that A6: ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) and A7: ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) ; ::_thesis: a = b consider N being Neighbourhood of z0 such that N c= dom f and A8: ex L being C_LinearFunc ex R being C_RestFunc st ( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A6; consider L being C_LinearFunc, R being C_RestFunc such that A9: a = L /. 1r and A10: for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A8; consider a1 being Element of COMPLEX such that A11: for b being Element of COMPLEX holds L /. b = a1 * b by Def4; consider N1 being Neighbourhood of z0 such that N1 c= dom f and A12: ex L being C_LinearFunc ex R being C_RestFunc st ( b = L /. 1r & ( for z being Element of COMPLEX st z in N1 holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A7; consider L1 being C_LinearFunc, R1 being C_RestFunc such that A13: b = L1 /. 1r and A14: for z being Element of COMPLEX st z in N1 holds (f /. z) - (f /. z0) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A12; consider b1 being Element of COMPLEX such that A15: for b being Element of COMPLEX holds L1 /. b = b1 * b by Def4; reconsider s0 = InvShift 2 as Complex_Sequence ; consider N0 being Neighbourhood of z0 such that A16: ( N0 c= N & N0 c= N1 ) by Lm1; consider g being Real such that A17: 0 < g and A18: { y where y is Complex : |.(y - z0).| < g } c= N0 by Def5; set s1 = g (#) s0; A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_(g_(#)_s0)_._n_=_g_/_(n_+_2) let n be Element of NAT ; ::_thesis: (g (#) s0) . n = g / (n + 2) thus (g (#) s0) . n = g * (s0 . n) by VALUED_1:6 .= g * (1 / (n + 2)) by Def2 .= g / (n + 2) ; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_(g_(#)_s0)_._n let n be Element of NAT ; ::_thesis: 0 <> (g (#) s0) . n (g (#) s0) . n = g / (n + 2) by A19; hence 0 <> (g (#) s0) . n by A17; ::_thesis: verum end; then A20: g (#) s0 is non-zero by COMSEQ_1:4; lim s0 = 0 by Th3; then lim (g (#) s0) = g * 0 by COMSEQ_2:18; then reconsider h = g (#) s0 as non-zero 0 -convergent Complex_Sequence by A20, Def1; A21: for n being Element of NAT ex x being Complex st ( x in N & x in N1 & h . n = x - z0 ) proof let n be Element of NAT ; ::_thesis: ex x being Complex st ( x in N & x in N1 & h . n = x - z0 ) reconsider g0 = g / (n + 2) as Complex ; take x = z0 + g0; ::_thesis: ( x in N & x in N1 & h . n = x - z0 ) 0 + 1 < (n + 1) + 1 by XREAL_1:6; then A22: g / (n + 2) < g / 1 by A17, XREAL_1:76; |.((z0 + g0) - z0).| = g / (n + 2) by A17, ABSVALUE:def_1; then x in { y where y is Complex : |.(y - z0).| < g } by A22; then x in N0 by A18; hence ( x in N & x in N1 & h . n = x - z0 ) by A16, A19; ::_thesis: verum end; A23: a = a1 * 1r by A9, A11; A24: now__::_thesis:_for_z_being_Complex_st_z_in_N_&_z_in_N1_holds_ (a_*_(z_-_z0))_+_(R_/._(z_-_z0))_=_(b_*_(z_-_z0))_+_(R1_/._(z_-_z0)) let z be Complex; ::_thesis: ( z in N & z in N1 implies (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) ) assume that A25: z in N and A26: z in N1 ; ::_thesis: (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) reconsider t0 = z0, t = z as Element of COMPLEX by XCMPLX_0:def_2; (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A10, A25; then (L /. (z - z0)) + (R /. (z - z0)) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A14, A26; then (a1 * (t - t0)) + (R /. (t - t0)) = (L1 /. (t - t0)) + (R1 /. (t - t0)) by A11; then ((a1 * 1r) * (z - z0)) + (R /. (z - z0)) = ((b1 * 1r) * (z - z0)) + (R1 /. (z - z0)) by A15; hence (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) by A13, A15, A23; ::_thesis: verum end; now__::_thesis:_for_n_being_Nat_holds_a_-_b_=_(((h_")_(#)_(R1_/*_h))_+_(-_((h_")_(#)_(R_/*_h))))_._n dom R1 = COMPLEX by PARTFUN1:def_2; then A27: rng h c= dom R1 ; dom R = COMPLEX by PARTFUN1:def_2; then A28: rng h c= dom R ; let n be Nat; ::_thesis: a - b = (((h ") (#) (R1 /* h)) + (- ((h ") (#) (R /* h)))) . n A29: n in NAT by ORDINAL1:def_12; then A30: h . n <> 0c by COMSEQ_1:4; ex x being Complex st ( x in N & x in N1 & h . n = x - z0 ) by A21, A29; then (a * (h . n)) + (R /. (h . n)) = (b * (h . n)) + (R1 /. (h . n)) by A24; then A31: ((a * (h . n)) / (h . n)) + ((R /. (h . n)) / (h . n)) = ((b * (h . n)) + (R1 /. (h . n))) / (h . n) by XCMPLX_1:62; A32: (b * (h . n)) / (h . n) = b * ((h . n) / (h . n)) .= b * 1 by A30, XCMPLX_1:60 .= b ; A33: (R1 /. (h . n)) / (h . n) = (R1 /. (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R1 /* h) . n) * ((h ") . n) by A29, A27, FUNCT_2:108 .= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ; A34: (a * (h . n)) / (h . n) = a * ((h . n) / (h . n)) .= a * 1 by A30, XCMPLX_1:60 .= a ; (R /. (h . n)) / (h . n) = (R /. (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R /* h) . n) * ((h ") . n) by A29, A28, FUNCT_2:109 .= ((h ") (#) (R /* h)) . n by VALUED_1:5 ; hence a - b = (((h ") (#) (R1 /* h)) . n) + (- (((h ") (#) (R /* h)) . n)) by A31, A34, A32, A33 .= (((h ") (#) (R1 /* h)) . n) + ((- ((h ") (#) (R /* h))) . n) by VALUED_1:8 .= (((h ") (#) (R1 /* h)) + (- ((h ") (#) (R /* h)))) . n by A29, VALUED_1:1 ; ::_thesis: verum end; then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = a - b ) by VALUED_0:def_18; then A35: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = a - b by CFCONT_1:28; A36: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by Def3; ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by Def3; then a - b = 0 - 0 by A35, A36, COMSEQ_2:26; hence a = b ; ::_thesis: verum end; end; :: deftheorem Def7 defines diff CFDIFF_1:def_7_:_ for f being PartFunc of COMPLEX,COMPLEX for z0 being Complex st f is_differentiable_in z0 holds for b3 being Element of COMPLEX holds ( b3 = diff (f,z0) iff ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b3 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) ); definition let f be PartFunc of COMPLEX,COMPLEX; attrf is differentiable means :Def8: :: CFDIFF_1:def 8 for x being Element of COMPLEX st x in dom f holds f is_differentiable_in x; end; :: deftheorem Def8 defines differentiable CFDIFF_1:def_8_:_ for f being PartFunc of COMPLEX,COMPLEX holds ( f is differentiable iff for x being Element of COMPLEX st x in dom f holds f is_differentiable_in x ); definition let f be PartFunc of COMPLEX,COMPLEX; let X be set ; predf is_differentiable_on X means :Def9: :: CFDIFF_1:def 9 ( X c= dom f & f | X is differentiable ); end; :: deftheorem Def9 defines is_differentiable_on CFDIFF_1:def_9_:_ for f being PartFunc of COMPLEX,COMPLEX for X being set holds ( f is_differentiable_on X iff ( X c= dom f & f | X is differentiable ) ); theorem Th8: :: CFDIFF_1:8 for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds X is Subset of COMPLEX proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds X is Subset of COMPLEX let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_on X implies X is Subset of COMPLEX ) assume f is_differentiable_on X ; ::_thesis: X is Subset of COMPLEX then X c= dom f by Def9; hence X is Subset of COMPLEX by XBOOLE_1:1; ::_thesis: verum end; definition let X be Subset of COMPLEX; attrX is closed means :Def10: :: CFDIFF_1:def 10 for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X; end; :: deftheorem Def10 defines closed CFDIFF_1:def_10_:_ for X being Subset of COMPLEX holds ( X is closed iff for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X ); definition let X be Subset of COMPLEX; attrX is open means :Def11: :: CFDIFF_1:def 11 X ` is closed ; end; :: deftheorem Def11 defines open CFDIFF_1:def_11_:_ for X being Subset of COMPLEX holds ( X is open iff X ` is closed ); theorem Th9: :: CFDIFF_1:9 for X being Subset of COMPLEX st X is open holds for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X proof let X be Subset of COMPLEX; ::_thesis: ( X is open implies for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X ) assume X is open ; ::_thesis: for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X then A1: X ` is closed by Def11; let z0 be Complex; ::_thesis: ( z0 in X implies ex N being Neighbourhood of z0 st N c= X ) assume that A2: z0 in X and A3: for N being Neighbourhood of z0 holds not N c= X ; ::_thesis: contradiction defpred S1[ Element of NAT , Complex] means ( $2 in { y where y is Complex : |.(y - z0).| < 1 / ($1 + 1) } & $2 in X ` ); A4: z0 in COMPLEX by XCMPLX_0:def_2; now__::_thesis:_for_g_being_Real_st_0_<_g_holds_ ex_s_being_Element_of_COMPLEX_st_ (_s_in__{__y_where_y_is_Complex_:_|.(y_-_z0).|_<_g__}__&_s_in_X_`_) let g be Real; ::_thesis: ( 0 < g implies ex s being Element of COMPLEX st ( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` ) ) assume A5: 0 < g ; ::_thesis: ex s being Element of COMPLEX st ( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` ) set N = { y where y is Complex : |.(y - z0).| < g } ; { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A4, A5, Th6; then not { y where y is Complex : |.(y - z0).| < g } c= X by A3; then consider x being set such that A6: x in { y where y is Complex : |.(y - z0).| < g } and A7: not x in X by TARSKI:def_3; consider s being Complex such that A8: x = s and A9: |.(s - z0).| < g by A6; reconsider s = s as Element of COMPLEX by XCMPLX_0:def_2; take s = s; ::_thesis: ( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` ) thus s in { y where y is Complex : |.(y - z0).| < g } by A9; ::_thesis: s in X ` thus s in X ` by A7, A8, XBOOLE_0:def_5; ::_thesis: verum end; then A10: for n being Element of NAT ex s being Element of COMPLEX st S1[n,s] ; consider s1 being Function of NAT,COMPLEX such that A11: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A10); A12: rng s1 c= X ` proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s1 or y in X ` ) assume y in rng s1 ; ::_thesis: y in X ` then consider y1 being set such that A13: y1 in dom s1 and A14: s1 . y1 = y by FUNCT_1:def_3; reconsider y1 = y1 as Element of NAT by A13; s1 . y1 in X ` by A11; hence y in X ` by A14; ::_thesis: verum end; A15: 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_ |.((s1_._m)_-_z0).|_<_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 |.((s1 . m) - z0).| < p ) assume A16: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s1 . m) - z0).| < p consider n being Element of NAT such that A17: p " < n by SEQ_4:3; take n = n; ::_thesis: for m being Element of NAT st n <= m holds |.((s1 . m) - z0).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s1 . m) - z0).| < p ) assume n <= m ; ::_thesis: |.((s1 . m) - z0).| < p then n + 1 <= m + 1 by XREAL_1:6; then A18: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118; s1 . m in { y where y is Complex : |.(y - z0).| < 1 / (m + 1) } by A11; then ex y being Complex st ( s1 . m = y & |.(y - z0).| < 1 / (m + 1) ) ; then A19: |.((s1 . m) - z0).| < 1 / (n + 1) by A18, XXREAL_0:2; (p ") + 0 < n + 1 by A17, XREAL_1:8; then 1 / (n + 1) < 1 / (p ") by A16, XREAL_1:76; hence |.((s1 . m) - z0).| < p by A19, XXREAL_0:2; ::_thesis: verum end; then A20: s1 is convergent by A4, COMSEQ_2:def_5; then lim s1 = z0 by A4, A15, COMSEQ_2:def_6; then z0 in COMPLEX \ X by A20, A12, A1, Def10; hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: CFDIFF_1:10 for X being Subset of COMPLEX st X is open holds for z0 being Complex st z0 in X holds ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X proof let X be Subset of COMPLEX; ::_thesis: ( X is open implies for z0 being Complex st z0 in X holds ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X ) assume A1: X is open ; ::_thesis: for z0 being Complex st z0 in X holds ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X let z0 be Complex; ::_thesis: ( z0 in X implies ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X ) assume z0 in X ; ::_thesis: ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X then consider N being Neighbourhood of z0 such that A2: N c= X by A1, Th9; consider g being Real such that 0 < g and A3: { y where y is Complex : |.(y - z0).| < g } c= N by Def5; take g ; ::_thesis: { y where y is Complex : |.(y - z0).| < g } c= X thus { y where y is Complex : |.(y - z0).| < g } c= X by A2, A3, XBOOLE_1:1; ::_thesis: verum end; theorem Th11: :: CFDIFF_1:11 for X being Subset of COMPLEX st ( for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X ) holds X is open proof let X be Subset of COMPLEX; ::_thesis: ( ( for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X ) implies X is open ) assume that A1: for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X and A2: not X is open ; ::_thesis: contradiction not X ` is closed by A2, Def11; then consider s1 being Function of NAT,COMPLEX such that A3: rng s1 c= X ` and A4: s1 is convergent and A5: not lim s1 in X ` by Def10; consider N being Neighbourhood of lim s1 such that A6: N c= X by A1, A5, SUBSET_1:29; consider g being Real such that A7: 0 < g and A8: { y where y is Complex : |.(y - (lim s1)).| < g } c= N by Def5; consider n being Element of NAT such that A9: for m being Element of NAT st n <= m holds |.((s1 . m) - (lim s1)).| < g by A4, A7, COMSEQ_2:def_6; n in NAT ; then n in dom s1 by FUNCT_2:def_1; then A10: s1 . n in rng s1 by FUNCT_1:def_3; |.((s1 . n) - (lim s1)).| < g by A9; then s1 . n in { y where y is Complex : |.(y - (lim s1)).| < g } ; then s1 . n in N by A8; hence contradiction by A3, A6, A10, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: CFDIFF_1:12 for X being Subset of COMPLEX holds ( X is open iff for x being Complex st x in X holds ex N being Neighbourhood of x st N c= X ) by Th9, Th11; theorem Th13: :: CFDIFF_1:13 for X being Subset of COMPLEX for z0 being Element of COMPLEX for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds X is open proof let X be Subset of COMPLEX; ::_thesis: for z0 being Element of COMPLEX for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds X is open let z0 be Element of COMPLEX ; ::_thesis: for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds X is open let r be Element of REAL ; ::_thesis: ( X = { y where y is Complex : |.(y - z0).| < r } implies X is open ) reconsider X0 = X as Subset of COMPLEX ; assume A1: X = { y where y is Complex : |.(y - z0).| < r } ; ::_thesis: X is open for x being Complex st x in X0 holds ex N being Neighbourhood of x st N c= X0 proof let x be Complex; ::_thesis: ( x in X0 implies ex N being Neighbourhood of x st N c= X0 ) A2: x in COMPLEX by XCMPLX_0:def_2; reconsider r1 = (r - |.(x - z0).|) / 2 as Real ; set N = { y where y is Complex : |.(y - x).| < r1 } ; assume x in X0 ; ::_thesis: ex N being Neighbourhood of x st N c= X0 then ex y being Complex st ( x = y & |.(y - z0).| < r ) by A1; then A3: r - |.(x - z0).| > 0 by XREAL_1:50; then reconsider N = { y where y is Complex : |.(y - x).| < r1 } as Neighbourhood of x by A2, Th6; r1 < r - |.(x - z0).| by A3, XREAL_1:216; then A4: r1 + |.(x - z0).| < (r - |.(x - z0).|) + |.(x - z0).| by XREAL_1:8; take N ; ::_thesis: N c= X0 let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in N or z in X0 ) assume z in N ; ::_thesis: z in X0 then consider y1 being Complex such that A5: z = y1 and A6: |.(y1 - x).| < r1 ; |.(y1 - x).| + |.(x - z0).| < r1 + |.(x - z0).| by A6, XREAL_1:8; then ( |.(y1 - z0).| <= |.(y1 - x).| + |.(x - z0).| & |.(y1 - x).| + |.(x - z0).| < r ) by A4, COMPLEX1:63, XXREAL_0:2; then |.(y1 - z0).| < r by XXREAL_0:2; hence z in X0 by A1, A5; ::_thesis: verum end; hence X is open by Th11; ::_thesis: verum end; theorem :: CFDIFF_1:14 for X being Subset of COMPLEX for z0 being Element of COMPLEX for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| <= r } holds X is closed proof let X be Subset of COMPLEX; ::_thesis: for z0 being Element of COMPLEX for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| <= r } holds X is closed let z0 be Element of COMPLEX ; ::_thesis: for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| <= r } holds X is closed let r be Element of REAL ; ::_thesis: ( X = { y where y is Complex : |.(y - z0).| <= r } implies X is closed ) reconsider X0 = X as Subset of COMPLEX ; assume A1: X = { y where y is Complex : |.(y - z0).| <= r } ; ::_thesis: X is closed for s1 being Complex_Sequence st rng s1 c= X0 & s1 is convergent holds lim s1 in X0 proof reconsider s4 = NAT --> r as Real_Sequence ; reconsider s2 = NAT --> z0 as Complex_Sequence ; let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X0 & s1 is convergent implies lim s1 in X0 ) assume that A2: rng s1 c= X0 and A3: s1 is convergent ; ::_thesis: lim s1 in X0 set s3 = s1 - s2; A4: s2 is convergent by CFCONT_1:26; then A5: lim (s1 - s2) = (lim s1) - (lim s2) by A3, COMSEQ_2:26; A6: for n being Element of NAT holds |.(s1 - s2).| . n <= r proof let n be Element of NAT ; ::_thesis: |.(s1 - s2).| . n <= r now__::_thesis:_for_n_being_Element_of_NAT_holds_(s1_-_s2)_._n_=_(s1_._n)_-_z0 let n be Element of NAT ; ::_thesis: (s1 - s2) . n = (s1 . n) - z0 (s1 - s2) . n = (s1 . n) + ((- s2) . n) by VALUED_1:1 .= (s1 . n) - (s2 . n) by VALUED_1:8 ; hence (s1 - s2) . n = (s1 . n) - z0 by FUNCOP_1:7; ::_thesis: verum end; then A7: (s1 - s2) . n = (s1 . n) - z0 ; dom s1 = NAT by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:def_3; then s1 . n in X0 by A2; then ex y being Complex st ( y = s1 . n & |.(y - z0).| <= r ) by A1; hence |.(s1 - s2).| . n <= r by A7, VALUED_1:18; ::_thesis: verum end; s1 - s2 is convergent by A3, A4; then A8: lim |.(s1 - s2).| = |.(lim (s1 - s2)).| by SEQ_2:27; reconsider s3 = s1 - s2 as convergent Complex_Sequence by A3, A4; A9: for n being Element of NAT holds |.s3.| . n <= s4 . n proof let n be Element of NAT ; ::_thesis: |.s3.| . n <= s4 . n |.s3.| . n <= r by A6; hence |.s3.| . n <= s4 . n by FUNCOP_1:7; ::_thesis: verum end; A10: for n being Element of NAT holds lim s2 = z0 proof let n be Element of NAT ; ::_thesis: lim s2 = z0 lim s2 = s2 . n by CFCONT_1:28 .= z0 by FUNCOP_1:7 ; hence lim s2 = z0 ; ::_thesis: verum end; lim s4 = s4 . 0 by SEQ_4:26 .= r by FUNCOP_1:7 ; then lim |.s3.| <= r by A9, SEQ_2:18; then |.((lim s1) - z0).| <= r by A10, A5, A8; hence lim s1 in X0 by A1; ::_thesis: verum end; hence X is closed by Def10; ::_thesis: verum end; registration clusterV45() open for Element of K19(COMPLEX); existence ex b1 being Subset of COMPLEX st b1 is open proof reconsider X = { y where y is Complex : |.(y - 0c).| < 1 } as Subset of COMPLEX by Th6; X is open by Th13; hence ex b1 being Subset of COMPLEX st b1 is open ; ::_thesis: verum end; end; theorem Th15: :: CFDIFF_1:15 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f is_differentiable_in x ) ) ) proof let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f is_differentiable_in x ) ) ) let Z be open Subset of COMPLEX; ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f is_differentiable_in x ) ) ) thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Element of COMPLEX 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 Element of COMPLEX st x in Z holds f is_differentiable_in x ) ) hence A2: Z c= dom f by Def9; ::_thesis: for x being Element of COMPLEX st x in Z holds f is_differentiable_in x let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) A3: f | Z is differentiable by A1, Def9; assume A4: x0 in Z ; ::_thesis: f is_differentiable_in x0 then x0 in dom (f | Z) by A2, RELAT_1:57; then f | Z is_differentiable_in x0 by A3, Def8; then consider N being Neighbourhood of x0 such that A5: N c= dom (f | Z) and A6: ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6; take N ; :: according to CFDIFF_1:def_6 ::_thesis: ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - 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 A5, XBOOLE_1:1; ::_thesis: ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0)) consider L being C_LinearFunc, R being C_RestFunc such that A7: for x being Element of COMPLEX st x in N holds ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A6; take L ; ::_thesis: ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0)) take R ; ::_thesis: for z being Element of COMPLEX st z in N holds (f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0)) let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume A8: x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) then ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A7; then A9: (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5, A8, PARTFUN2:15; x0 in (dom f) /\ Z by A2, A4, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A9, PARTFUN2:16; ::_thesis: verum end; assume that A10: Z c= dom f and A11: for x being Element of COMPLEX st x in Z holds f is_differentiable_in x ; ::_thesis: f is_differentiable_on Z thus Z c= dom f by A10; :: according to CFDIFF_1:def_9 ::_thesis: f | Z is differentiable let x0 be Element of COMPLEX ; :: according to CFDIFF_1:def_8 ::_thesis: ( x0 in dom (f | Z) implies f | Z is_differentiable_in x0 ) assume x0 in dom (f | Z) ; ::_thesis: f | Z is_differentiable_in x0 then A12: x0 in Z by RELAT_1:57; then consider N1 being Neighbourhood of x0 such that A13: N1 c= Z by Th9; f is_differentiable_in x0 by A11, A12; then consider N being Neighbourhood of x0 such that A14: N c= dom f and A15: ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6; consider N2 being Neighbourhood of x0 such that A16: N2 c= N1 and A17: N2 c= N by Lm1; A18: N2 c= Z by A13, A16, XBOOLE_1:1; take N2 ; :: according to CFDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) ) N2 c= dom f by A14, A17, XBOOLE_1:1; then N2 c= (dom f) /\ Z by A18, XBOOLE_1:19; hence A19: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) consider L being C_LinearFunc, R being C_RestFunc such that A20: for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A15; A21: x0 in N2 by Th7; take L ; ::_thesis: ex R being C_RestFunc st for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) take R ; ::_thesis: for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) let x be Element of COMPLEX ; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume A22: 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 A17, A20; then ((f | Z) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A19, A22, PARTFUN2:15; hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A19, A21, PARTFUN2:15; ::_thesis: verum end; theorem :: CFDIFF_1:16 for Y being Subset of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds Y is open proof let Y be Subset of COMPLEX; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds Y is open let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_on Y implies Y is open ) assume A1: f is_differentiable_on Y ; ::_thesis: Y is open then A2: Y c= dom f by Def9; now__::_thesis:_for_x0_being_Complex_st_x0_in_Y_holds_ ex_N_being_Neighbourhood_of_x0_st_N_c=_Y let x0 be Complex; ::_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 A3: x0 in dom (f | Y) by A2, RELAT_1:57; f | Y is differentiable by A1, Def9; then f | Y is_differentiable_in x0 by A3, Def8; then consider N being Neighbourhood of x0 such that A4: N c= dom (f | Y) and ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds ((f | Y) /. x) - ((f | Y) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6; take N = N; ::_thesis: N c= Y dom (f | Y) = (dom f) /\ Y by RELAT_1:61; then dom (f | Y) c= Y by XBOOLE_1:17; hence N c= Y by A4, XBOOLE_1:1; ::_thesis: verum end; hence Y is open by Th11; ::_thesis: verum end; definition let f be PartFunc of COMPLEX,COMPLEX; let X be set ; assume A1: f is_differentiable_on X ; funcf `| X -> PartFunc of COMPLEX,COMPLEX means :Def12: :: CFDIFF_1:def 12 ( dom it = X & ( for x being Element of COMPLEX st x in X holds it /. x = diff (f,x) ) ); existence ex b1 being PartFunc of COMPLEX,COMPLEX st ( dom b1 = X & ( for x being Element of COMPLEX st x in X holds b1 /. x = diff (f,x) ) ) proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = diff (f,$1); defpred S1[ set ] means $1 in X; consider F being PartFunc of COMPLEX,COMPLEX such that A2: ( ( for x being Element of COMPLEX holds ( x in dom F iff S1[x] ) ) & ( for x being Element of COMPLEX st x in dom F holds F . x = H1(x) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = X & ( for x being Element of COMPLEX st x in X holds F /. x = diff (f,x) ) ) now__::_thesis:_for_y_being_set_st_y_in_X_holds_ y_in_dom_F A3: X is Subset of COMPLEX by A1, Th8; let y be set ; ::_thesis: ( y in X implies y in dom F ) assume y in X ; ::_thesis: y in dom F hence y in dom F by A2, A3; ::_thesis: verum end; then A4: X c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in X by A2; then dom F c= X by TARSKI:def_3; hence dom F = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Element of COMPLEX st x in X holds F /. x = diff (f,x) now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_X_holds_ F_/._x_=_diff_(f,x) let x be Element of COMPLEX ; ::_thesis: ( x in X implies F /. x = diff (f,x) ) assume x in X ; ::_thesis: F /. x = diff (f,x) then A5: x in dom F by A2; then F . x = diff (f,x) by A2; hence F /. x = diff (f,x) by A5, PARTFUN1:def_6; ::_thesis: verum end; hence for x being Element of COMPLEX st x in X holds F /. x = diff (f,x) ; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of COMPLEX,COMPLEX st dom b1 = X & ( for x being Element of COMPLEX st x in X holds b1 /. x = diff (f,x) ) & dom b2 = X & ( for x being Element of COMPLEX st x in X holds b2 /. x = diff (f,x) ) holds b1 = b2 proof let F, G be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( dom F = X & ( for x being Element of COMPLEX st x in X holds F /. x = diff (f,x) ) & dom G = X & ( for x being Element of COMPLEX st x in X holds G /. x = diff (f,x) ) implies F = G ) assume that A6: dom F = X and A7: for x being Element of COMPLEX st x in X holds F /. x = diff (f,x) and A8: dom G = X and A9: for x being Element of COMPLEX st x in X holds G /. x = diff (f,x) ; ::_thesis: F = G now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_dom_F_holds_ F_/._x_=_G_/._x let x be Element of COMPLEX ; ::_thesis: ( x in dom F implies F /. x = G /. x ) assume A10: x in dom F ; ::_thesis: F /. x = G /. x then F /. x = diff (f,x) by A6, A7; hence F /. x = G /. x by A6, A9, A10; ::_thesis: verum end; hence F = G by A6, A8, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem Def12 defines `| CFDIFF_1:def_12_:_ for f being PartFunc of COMPLEX,COMPLEX for X being set st f is_differentiable_on X holds for b3 being PartFunc of COMPLEX,COMPLEX holds ( b3 = f `| X iff ( dom b3 = X & ( for x being Element of COMPLEX st x in X holds b3 /. x = diff (f,x) ) ) ); theorem :: CFDIFF_1:17 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Element of COMPLEX st rng f = {a1} holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) proof set R = cf; A1: dom cf = COMPLEX by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c A2: ( rng h c= dom cf & n in NAT ) by A1, ORDINAL1:def_12; thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5 .= ((h ") . n) * (cf /. (h . n)) by A2, FUNCT_2:109 .= ((h ") . n) * 0c by FUNCOP_1:7 .= 0c ; ::_thesis: verum end; then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18; hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum end; then reconsider R = cf as C_RestFunc by Def3; set L = cf; for z being Element of COMPLEX holds cf /. z = 0c * z by FUNCOP_1:7; then reconsider L = cf as C_LinearFunc by Def4; let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Element of COMPLEX st rng f = {a1} holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & ex a1 being Element of COMPLEX st rng f = {a1} implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) ) assume A3: Z c= dom f ; ::_thesis: ( for a1 being Element of COMPLEX holds not rng f = {a1} or ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) ) given a1 being Element of COMPLEX such that A4: rng f = {a1} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) A5: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_dom_f_holds_ f_/._x0_=_a1 let x0 be Element of COMPLEX ; ::_thesis: ( x0 in dom f implies f /. x0 = a1 ) assume A6: x0 in dom f ; ::_thesis: f /. x0 = a1 then f . x0 in {a1} by A4, FUNCT_1:def_3; then f /. x0 in {a1} by A6, PARTFUN1:def_6; hence f /. x0 = a1 by TARSKI:def_1; ::_thesis: verum end; A7: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A8: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A9: N c= Z by Th9; A10: N c= dom f by A3, A9, XBOOLE_1:1; for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5, A10 .= a1 - a1 by A3, A5, A8 .= (L /. (x - x0)) + 0c by FUNCOP_1:7 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; hence f is_differentiable_in x0 by A10, Def6; ::_thesis: verum end; hence A11: f is_differentiable_on Z by A3, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0c ) assume A12: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0c then A13: f is_differentiable_in x0 by A7; then ex N being Neighbourhood of x0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by Def6; then consider N being Neighbourhood of x0 such that A14: N c= dom f ; A15: for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5, A14 .= a1 - a1 by A3, A5, A12 .= (L /. (x - x0)) + 0c by FUNCOP_1:7 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; thus (f `| Z) /. x0 = diff (f,x0) by A11, A12, Def12 .= L /. 1r by A13, A14, A15, Def7 .= 0c by FUNCOP_1:7 ; ::_thesis: verum end; registration let seq be non-zero Complex_Sequence; let k be Nat; clusterseq ^\ k -> non-zero ; coherence seq ^\ k is non-empty proof now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_k)_._n_<>_0c let n be Element of NAT ; ::_thesis: (seq ^\ k) . n <> 0c (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3; hence (seq ^\ k) . n <> 0c by COMSEQ_1:4; ::_thesis: verum end; hence seq ^\ k is non-empty by COMSEQ_1:4; ::_thesis: verum end; end; registration let h be non-zero 0 -convergent Complex_Sequence; let n be Element of NAT ; clusterh ^\ n -> 0 -convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = h ^\ n holds b1 is 0 -convergent proof lim h = 0 by Def1; then A1: lim (h ^\ n) = 0 by CFCONT_1:21; h ^\ n is convergent by CFCONT_1:21; hence for b1 being Complex_Sequence st b1 = h ^\ n holds b1 is 0 -convergent by A1, Def1; ::_thesis: verum end; end; theorem Th18: :: CFDIFF_1:18 for k being Element of NAT for seq, seq1 being Complex_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) proof let k be Element of NAT ; ::_thesis: for seq, seq1 being Complex_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) let seq, seq1 be Complex_Sequence; ::_thesis: (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_+_seq1)_^\_k)_._n_=_((seq_^\_k)_+_(seq1_^\_k))_._n let n be Element of NAT ; ::_thesis: ((seq + seq1) ^\ k) . n = ((seq ^\ k) + (seq1 ^\ k)) . n thus ((seq + seq1) ^\ k) . n = (seq + seq1) . (n + k) by NAT_1:def_3 .= (seq . (n + k)) + (seq1 . (n + k)) by VALUED_1:1 .= ((seq ^\ k) . n) + (seq1 . (n + k)) by NAT_1:def_3 .= ((seq ^\ k) . n) + ((seq1 ^\ k) . n) by NAT_1:def_3 .= ((seq ^\ k) + (seq1 ^\ k)) . n by VALUED_1:1 ; ::_thesis: verum end; hence (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem Th19: :: CFDIFF_1:19 for k being Element of NAT for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) proof let k be Element of NAT ; ::_thesis: for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) let seq, seq1 be Complex_Sequence; ::_thesis: (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_-_seq1)_^\_k)_._n_=_((seq_^\_k)_-_(seq1_^\_k))_._n let n be Element of NAT ; ::_thesis: ((seq - seq1) ^\ k) . n = ((seq ^\ k) - (seq1 ^\ k)) . n thus ((seq - seq1) ^\ k) . n = (seq + (- seq1)) . (n + k) by NAT_1:def_3 .= (seq . (n + k)) + ((- seq1) . (n + k)) by VALUED_1:1 .= (seq . (n + k)) + (- (seq1 . (n + k))) by VALUED_1:8 .= ((seq ^\ k) . n) - (seq1 . (n + k)) by NAT_1:def_3 .= ((seq ^\ k) . n) + (- ((seq1 ^\ k) . n)) by NAT_1:def_3 .= ((seq ^\ k) . n) + ((- (seq1 ^\ k)) . n) by VALUED_1:8 .= ((seq ^\ k) - (seq1 ^\ k)) . n by VALUED_1:1 ; ::_thesis: verum end; hence (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem Th20: :: CFDIFF_1:20 for k being Element of NAT for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) " proof let k be Element of NAT ; ::_thesis: for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) " let seq be Complex_Sequence; ::_thesis: (seq ") ^\ k = (seq ^\ k) " now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_")_^\_k)_._n_=_((seq_^\_k)_")_._n let n be Element of NAT ; ::_thesis: ((seq ") ^\ k) . n = ((seq ^\ k) ") . n thus ((seq ") ^\ k) . n = (seq ") . (n + k) by NAT_1:def_3 .= (seq . (n + k)) " by VALUED_1:10 .= ((seq ^\ k) . n) " by NAT_1:def_3 .= ((seq ^\ k) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence (seq ") ^\ k = (seq ^\ k) " by FUNCT_2:63; ::_thesis: verum end; theorem Th21: :: CFDIFF_1:21 for k being Element of NAT for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) proof let k be Element of NAT ; ::_thesis: for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) let seq, seq1 be Complex_Sequence; ::_thesis: (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_(#)_seq1)_^\_k)_._n_=_((seq_^\_k)_(#)_(seq1_^\_k))_._n let n be Element of NAT ; ::_thesis: ((seq (#) seq1) ^\ k) . n = ((seq ^\ k) (#) (seq1 ^\ k)) . n thus ((seq (#) seq1) ^\ k) . n = (seq (#) seq1) . (n + k) by NAT_1:def_3 .= (seq . (n + k)) * (seq1 . (n + k)) by VALUED_1:5 .= ((seq ^\ k) . n) * (seq1 . (n + k)) by NAT_1:def_3 .= ((seq ^\ k) . n) * ((seq1 ^\ k) . n) by NAT_1:def_3 .= ((seq ^\ k) (#) (seq1 ^\ k)) . n by VALUED_1:5 ; ::_thesis: verum end; hence (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem Th22: :: CFDIFF_1:22 for f being PartFunc of COMPLEX,COMPLEX for x0 being Complex for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Complex_Sequence for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) proof let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Complex for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Complex_Sequence for c being constant Complex_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 Complex; ::_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 Complex_Sequence for c being constant Complex_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 Complex_Sequence for c being constant Complex_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 Complex_Sequence for c being constant Complex_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 C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N1 holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6; consider N2 being Neighbourhood of x0 such that A4: N2 c= N and A5: N2 c= N1 by Lm1; A6: N2 c= dom f by A2, A4, XBOOLE_1:1; let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: for c being constant Complex_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 Complex_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 such that A9: 0 < g and A10: { y where y is Complex : |.(y - x0).| < g } c= N2 by Def5; |.(x0 - x0).| = 0 by COMPLEX1:44; then x0 in { y where y is Complex : |.(y - x0).| < g } by A9; then A11: x0 in N2 by A10; A12: rng c c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in dom f ) assume y in rng c ; ::_thesis: y in dom f then y = x0 by A7, TARSKI:def_1; then y in N by A4, A11; hence y in dom f by A2; ::_thesis: verum end; ex n being Element of NAT st ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) proof x0 in rng c by A7, TARSKI:def_1; then A13: lim c = x0 by CFCONT_1:27; A14: c is convergent by CFCONT_1:26; then A15: h + c is convergent ; lim h = 0 by Def1; then lim (h + c) = 0 + x0 by A14, A13, COMSEQ_2:14 .= x0 ; then consider n being Element of NAT such that A16: for m being Element of NAT st n <= m holds |.(((h + c) . m) - x0).| < g by A9, A15, COMSEQ_2:def_6; take n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) A17: rng (c ^\ n) = {x0} by A7, VALUED_0:26; thus rng (c ^\ n) c= N2 ::_thesis: rng ((h + c) ^\ n) c= N2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in N2 ) assume y in rng (c ^\ n) ; ::_thesis: y in N2 hence y in N2 by A11, A17, TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in N2 ) assume y in rng ((h + c) ^\ n) ; ::_thesis: y in N2 then consider m being Element of NAT such that A18: y = ((h + c) ^\ n) . m by FUNCT_2:113; reconsider y1 = y as Complex by A18; n + 0 <= n + m by XREAL_1:7; then |.(((h + c) . (n + m)) - x0).| < g by A16; then |.((((h + c) ^\ n) . m) - x0).| < g by NAT_1:def_3; then y1 in { z where z is Complex : |.(z - x0).| < g } by A18; hence y in N2 by A10; ::_thesis: verum end; then consider n being Element of NAT such that rng (c ^\ n) c= N2 and A19: rng ((h + c) ^\ n) c= N2 ; consider L being C_LinearFunc, R being C_RestFunc such that A20: for x being Element of COMPLEX st x in N1 holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A3; A21: rng (c ^\ n) c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom f ) assume 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; A23: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L /. 1r ) proof deffunc H1( Element of NAT ) -> Element of COMPLEX = (L /. 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1); consider s1 being Complex_Sequence such that A24: for k being Element of NAT holds s1 . k = H1(k) from COMSEQ_1:sch_1(); A25: 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_ abs_((s1_._k)_-_(L_/._1r))_<_r A26: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by Def3; 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 abs ((s1 . k) - (L /. 1r)) < r ) assume 0 < r ; ::_thesis: ex n1 being Element of NAT st for k being Element of NAT st n1 <= k holds abs ((s1 . k) - (L /. 1r)) < r then consider m being Element of NAT such that A27: for k being Element of NAT st m <= k holds abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0c) < r by A26, COMSEQ_2:def_6; take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds abs ((s1 . k) - (L /. 1r)) < r let k be Element of NAT ; ::_thesis: ( n1 <= k implies abs ((s1 . k) - (L /. 1r)) < r ) assume A28: n1 <= k ; ::_thesis: abs ((s1 . k) - (L /. 1r)) < r abs ((s1 . k) - (L /. 1r)) = abs (((L /. 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L /. 1r)) by A24 .= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0c) ; hence abs ((s1 . k) - (L /. 1r)) < r by A27, A28; ::_thesis: verum end; consider x being Element of COMPLEX such that A29: for b1 being Element of COMPLEX holds L /. b1 = x * b1 by Def4; A30: L /. 1r = x * 1r by A29 .= x ; now__::_thesis:_for_m_being_Element_of_NAT_holds_(((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_(#)_((h_^\_n)_"))_._m_=_s1_._m let m be Element of NAT ; ::_thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m A31: (h ^\ n) . m <> 0c by COMSEQ_1:4; thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by VALUED_1:5 .= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by VALUED_1:1 .= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) .= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:5 .= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10 .= ((L /. ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by FUNCT_2:115 .= ((x * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A29 .= (x * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) .= (x * 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A31, XCMPLX_0:def_7 .= s1 . m by A24, A30 ; ::_thesis: verum end; then A32: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63; hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A25, COMSEQ_2:def_5; ::_thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L /. 1r hence lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L /. 1r by A32, A25, COMSEQ_2:def_6; ::_thesis: verum end; A33: 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 FUNCT_2:112; then A34: ((h + c) ^\ n) . k in N2 by A19; ( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by FUNCT_2:112, VALUED_0:26; then A35: (c ^\ n) . k = x0 by A7, TARSKI:def_1; (((h + c) ^\ n) . k) - ((c ^\ n) . k) = ((h + c) . (k + n)) - ((c ^\ n) . k) by NAT_1:def_3 .= ((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k) by VALUED_1:1 .= (((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k) by NAT_1:def_3 .= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by NAT_1:def_3 .= (h ^\ n) . k ; hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A20, A5, A34, A35; ::_thesis: verum end; A36: rng (h + c) c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom f ) assume y in rng (h + c) ; ::_thesis: y in dom f then y in N by A8; hence y in dom f by A2; ::_thesis: verum end; A37: rng ((h + c) ^\ n) c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in dom f ) assume y in rng ((h + c) ^\ n) ; ::_thesis: y in dom f then y in N2 by A19; then y in N by A4; hence y in dom f by A2; ::_thesis: verum end; now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_/*_((h_+_c)_^\_n))_-_(f_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k let k be Element of NAT ; ::_thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by CFCONT_1:1 .= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A37, FUNCT_2:109 .= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A21, FUNCT_2:109 .= (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A33 .= ((L /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by FUNCT_2:115 .= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by FUNCT_2:115 .= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by VALUED_1:1 ; ::_thesis: verum end; then A38: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by FUNCT_2:def_7 .= (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by A36, VALUED_0:27 .= (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) ") by A12, VALUED_0:27 .= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) ") by Th19 .= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ") ^\ n) by Th20 .= (((f /* (h + c)) - (f /* c)) (#) (h ")) ^\ n by Th21 ; then A39: L /. 1r = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A23, CFCONT_1:23; thus (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A23, A38, CFCONT_1:22; ::_thesis: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) for x being Element of COMPLEX st x in N2 holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A20, A5; hence diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A1, A6, A39, Def7; ::_thesis: verum end; theorem Th23: :: CFDIFF_1:23 for f1, f2 being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX 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 f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX 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 Element of COMPLEX ; ::_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 C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N1 holds (f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6; consider L1 being C_LinearFunc, R1 being C_RestFunc such that A5: for x being Element of COMPLEX 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 C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N2 holds (f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, Def6; consider L2 being C_LinearFunc, R2 being C_RestFunc such that A8: for x being Element of COMPLEX st x in N2 holds (f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A7; reconsider R = R1 + R2 as C_RestFunc ; reconsider L = L1 + L2 as C_LinearFunc ; consider N being Neighbourhood of x0 such that A9: N c= N1 and A10: N c= N2 by Lm1; A11: N c= dom f2 by A6, A10, XBOOLE_1:1; N c= dom f1 by A3, A9, XBOOLE_1:1; then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27; then A12: N c= dom (f1 + f2) by VALUED_1:def_1; A13: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N_holds_ ((f1_+_f2)_/._x)_-_((f1_+_f2)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Element of COMPLEX ; ::_thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) A14: x0 in N by Th7; assume A15: 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 A12, CFUNCT_1:1 .= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A12, A14, CFUNCT_1:1 .= ((f1 /. x) - (f1 /. x0)) + ((f2 /. x) - (f2 /. x0)) .= ((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A9, A15 .= ((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A8, A10, A15 .= ((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) .= (L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by CFUNCT_1:64 .= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:64 ; ::_thesis: verum end; hence f1 + f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) hence diff ((f1 + f2),x0) = L /. 1r by A12, A13, Def7 .= (L1 /. 1r) + (L2 /. 1r) by CFUNCT_1:64 .= (diff (f1,x0)) + (L2 /. 1r) by A1, A3, A5, Def7 .= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def7 ; ::_thesis: verum end; theorem Th24: :: CFDIFF_1:24 for f1, f2 being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX 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 f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX 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 Element of COMPLEX ; ::_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 C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N1 holds (f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6; consider L1 being C_LinearFunc, R1 being C_RestFunc such that A5: for x being Element of COMPLEX 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 C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N2 holds (f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, Def6; consider L2 being C_LinearFunc, R2 being C_RestFunc such that A8: for x being Element of COMPLEX st x in N2 holds (f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A7; reconsider R = R1 - R2 as C_RestFunc ; reconsider L = L1 - L2 as C_LinearFunc ; consider N being Neighbourhood of x0 such that A9: N c= N1 and A10: N c= N2 by Lm1; A11: N c= dom f2 by A6, A10, XBOOLE_1:1; N c= dom f1 by A3, A9, XBOOLE_1:1; then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27; then A12: N c= dom (f1 - f2) by CFUNCT_1:2; A13: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N_holds_ ((f1_-_f2)_/._x)_-_((f1_-_f2)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Element of COMPLEX ; ::_thesis: ( x in N implies ((f1 - f2) /. x) - ((f1 - f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) A14: x0 in N by Th7; assume A15: 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 A12, CFUNCT_1:2 .= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A12, A14, CFUNCT_1:2 .= ((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0)) .= ((L1 /. (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0)) by A5, A9, A15 .= ((L1 /. (x - x0)) + (R1 /. (x - x0))) - ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A8, A10, A15 .= ((L1 /. (x - x0)) - (L2 /. (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) .= (L /. (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by CFUNCT_1:64 .= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:64 ; ::_thesis: verum end; hence f1 - f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) hence diff ((f1 - f2),x0) = L /. 1r by A12, A13, Def7 .= (L1 /. 1r) - (L2 /. 1r) by CFUNCT_1:64 .= (diff (f1,x0)) - (L2 /. 1r) by A1, A3, A5, Def7 .= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def7 ; ::_thesis: verum end; theorem Th25: :: CFDIFF_1:25 for a being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f is_differentiable_in x0 holds ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) ) proof let a be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f is_differentiable_in x0 holds ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f is_differentiable_in x0 holds ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) ) let x0 be Element of COMPLEX ; ::_thesis: ( f is_differentiable_in x0 implies ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) ) ) assume A1: f is_differentiable_in x0 ; ::_thesis: ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) ) then consider N1 being Neighbourhood of x0 such that A2: N1 c= dom f and A3: ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N1 holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6; consider L1 being C_LinearFunc, R1 being C_RestFunc such that A4: for x being Element of COMPLEX st x in N1 holds (f /. x) - (f /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A3; reconsider R = a (#) R1 as C_RestFunc ; reconsider L = a (#) L1 as C_LinearFunc ; A5: N1 c= dom (a (#) f) by A2, VALUED_1:def_5; A6: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N1_holds_ ((a_(#)_f)_/._x)_-_((a_(#)_f)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Element of COMPLEX ; ::_thesis: ( x in N1 implies ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) A7: x0 in N1 by Th7; assume A8: x in N1 ; ::_thesis: ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) hence ((a (#) f) /. x) - ((a (#) f) /. x0) = (a * (f /. x)) - ((a (#) f) /. x0) by A5, CFUNCT_1:4 .= (a * (f /. x)) - (a * (f /. x0)) by A5, A7, CFUNCT_1:4 .= a * ((f /. x) - (f /. x0)) .= a * ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A4, A8 .= (a * (L1 /. (x - x0))) + (a * (R1 /. (x - x0))) .= (L /. (x - x0)) + (a * (R1 /. (x - x0))) by CFUNCT_1:65 .= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:65 ; ::_thesis: verum end; hence a (#) f is_differentiable_in x0 by A5, Def6; ::_thesis: diff ((a (#) f),x0) = a * (diff (f,x0)) hence diff ((a (#) f),x0) = L /. 1r by A5, A6, Def7 .= a * (L1 /. 1r) by CFUNCT_1:65 .= a * (diff (f,x0)) by A1, A2, A4, Def7 ; ::_thesis: verum end; theorem Th26: :: CFDIFF_1:26 for f1, f2 being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) ) proof let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) ) let x0 be Element of COMPLEX ; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) ) ) assume that A1: f1 is_differentiable_in x0 and A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) ) consider N2 being Neighbourhood of x0 such that A3: N2 c= dom f2 and A4: ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N2 holds (f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, Def6; consider L2 being C_LinearFunc, R2 being C_RestFunc such that A5: for x being Element of COMPLEX st x in N2 holds (f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A4; reconsider R12 = (f1 /. x0) (#) R2 as C_RestFunc ; reconsider L12 = (f1 /. x0) (#) L2 as C_LinearFunc ; consider N1 being Neighbourhood of x0 such that A6: N1 c= dom f1 and A7: ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N1 holds (f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6; consider L1 being C_LinearFunc, R1 being C_RestFunc such that A8: for x being Element of COMPLEX st x in N1 holds (f1 /. x) - (f1 /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A7; reconsider R11 = (f2 /. x0) (#) R1 as C_RestFunc ; reconsider L11 = (f2 /. x0) (#) L1 as C_LinearFunc ; reconsider R18 = R2 (#) L1 as C_RestFunc ; reconsider R17 = R1 (#) R2 as C_RestFunc ; reconsider R16 = R1 (#) L2 as C_RestFunc ; reconsider R14 = L1 (#) L2 as C_RestFunc ; reconsider R13 = R11 + R12 as C_RestFunc ; reconsider L = L11 + L12 as C_LinearFunc ; reconsider R15 = R13 + R14 as C_RestFunc ; reconsider R19 = R16 + R17 as C_RestFunc ; reconsider R20 = R19 + R18 as C_RestFunc ; reconsider R = R15 + R20 as C_RestFunc ; consider N being Neighbourhood of x0 such that A9: N c= N1 and A10: N c= N2 by Lm1; A11: N c= dom f2 by A3, A10, XBOOLE_1:1; N c= dom f1 by A6, A9, XBOOLE_1:1; then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27; then A12: N c= dom (f1 (#) f2) by VALUED_1:def_4; A13: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N_holds_ ((f1_(#)_f2)_/._x)_-_((f1_(#)_f2)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Element of COMPLEX ; ::_thesis: ( x in N implies ((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) A14: x0 in N by Th7; assume A15: x in N ; ::_thesis: ((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) then A16: ((f1 /. x) - (f1 /. x0)) + (f1 /. x0) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0) by A8, A9; thus ((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0) = ((f1 /. x) * (f2 /. x)) - ((f1 (#) f2) /. x0) by A12, A15, CFUNCT_1:3 .= ((((f1 /. x) * (f2 /. x)) + (- ((f1 /. x) * (f2 /. x0)))) + ((f1 /. x) * (f2 /. x0))) - ((f1 /. x0) * (f2 /. x0)) by A12, A14, CFUNCT_1:3 .= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((f1 /. x) - (f1 /. x0)) * (f2 /. x0)) .= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((L1 /. (x - x0)) + (R1 /. (x - x0))) * (f2 /. x0)) by A8, A9, A15 .= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((f2 /. x0) * (L1 /. (x - x0))) + ((R1 /. (x - x0)) * (f2 /. x0))) .= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + ((L11 /. (x - x0)) + ((f2 /. x0) * (R1 /. (x - x0)))) by CFUNCT_1:65 .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((f2 /. x) - (f2 /. x0))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by A16, CFUNCT_1:65 .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by A5, A10, A15 .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + (((f1 /. x0) * (L2 /. (x - x0))) + ((f1 /. x0) * (R2 /. (x - x0))))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((f1 /. x0) * (R2 /. (x - x0))))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by CFUNCT_1:65 .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + (R12 /. (x - x0)))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by CFUNCT_1:65 .= (((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((L11 /. (x - x0)) + ((R11 /. (x - x0)) + (R12 /. (x - x0))))) .= (((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((L11 /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1:64 .= (((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + (((L11 /. (x - x0)) + (L12 /. (x - x0))) + (R13 /. (x - x0))) .= ((((L1 /. (x - x0)) * (L2 /. (x - x0))) + ((L1 /. (x - x0)) * (R2 /. (x - x0)))) + ((R1 /. (x - x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64 .= (((R14 /. (x - x0)) + ((R2 /. (x - x0)) * (L1 /. (x - x0)))) + ((R1 /. (x - x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64 .= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + (((R1 /. (x - x0)) * (L2 /. (x - x0))) + ((R1 /. (x - x0)) * (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64 .= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + ((R1 /. (x - x0)) * (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64 .= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + (R17 /. (x - x0)))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64 .= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + (R19 /. (x - x0))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64 .= ((R14 /. (x - x0)) + ((R19 /. (x - x0)) + (R18 /. (x - x0)))) + ((L /. (x - x0)) + (R13 /. (x - x0))) .= ((L /. (x - x0)) + (R13 /. (x - x0))) + ((R14 /. (x - x0)) + (R20 /. (x - x0))) by CFUNCT_1:64 .= (L /. (x - x0)) + (((R13 /. (x - x0)) + (R14 /. (x - x0))) + (R20 /. (x - x0))) .= (L /. (x - x0)) + ((R15 /. (x - x0)) + (R20 /. (x - x0))) by CFUNCT_1:64 .= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:64 ; ::_thesis: verum end; hence f1 (#) f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) hence diff ((f1 (#) f2),x0) = L /. 1r by A12, A13, Def7 .= (L11 /. 1r) + (L12 /. 1r) by CFUNCT_1:64 .= ((f2 /. x0) * (L1 /. 1r)) + (L12 /. 1r) by CFUNCT_1:65 .= ((f2 /. x0) * (L1 /. 1r)) + ((f1 /. x0) * (L2 /. 1r)) by CFUNCT_1:65 .= ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (L2 /. 1r)) by A1, A6, A8, Def7 .= ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) by A2, A3, A5, Def7 ; ::_thesis: verum end; theorem :: CFDIFF_1:27 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & f | Z = id Z holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 1r ) ) proof set R = cf; reconsider L = id COMPLEX as PartFunc of COMPLEX,COMPLEX ; A1: COMPLEX c= COMPLEX ; then for b being Element of COMPLEX holds L /. b = 1r * b by PARTFUN2:6; then reconsider L = L as C_LinearFunc by Def4; A2: dom cf = COMPLEX by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c A3: ( n in NAT & rng h c= dom cf ) by A2, ORDINAL1:def_12; thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5 .= ((h ") . n) * (cf /. (h . n)) by A3, FUNCT_2:109 .= ((h ") . n) * 0c by FUNCOP_1:7 .= 0c ; ::_thesis: verum end; then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18; hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum end; then reconsider R = cf as C_RestFunc by Def3; let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & f | Z = id Z holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 1r ) ) let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 1r ) ) ) assume that A4: Z c= dom f and A5: f | Z = id Z ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 1r ) ) A6: now__::_thesis:_for_x_being_Complex_st_x_in_Z_holds_ f_/._x_=_x let x be Complex; ::_thesis: ( x in Z implies f /. x = x ) assume A7: x in Z ; ::_thesis: f /. x = x then (f | Z) . x = x by A5, FUNCT_1:18; then f . x = x by A7, FUNCT_1:49; hence f /. x = x by A4, A7, PARTFUN1:def_6; ::_thesis: verum end; A8: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_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 Th9; A11: for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = x - (f /. x0) by A6, A10 .= x - x0 by A6, A9 .= (L /. (x - x0)) + 0c by A1, PARTFUN2:6 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; N c= dom f by A4, A10, XBOOLE_1:1; hence f is_differentiable_in x0 by A11, Def6; ::_thesis: verum end; hence A12: f is_differentiable_on Z by A4, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 1r let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 1r ) assume A13: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 1r then consider N1 being Neighbourhood of x0 such that A14: N1 c= Z by Th9; A15: f is_differentiable_in x0 by A8, A13; then ex N being Neighbourhood of x0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by Def6; then consider N being Neighbourhood of x0 such that A16: N c= dom f ; consider N2 being Neighbourhood of x0 such that A17: N2 c= N1 and A18: N2 c= N by Lm1; A19: N2 c= dom f by A16, A18, XBOOLE_1:1; A20: for x being Element of COMPLEX st x in N2 holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N2 implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N2 ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) then x in N1 by A17; hence (f /. x) - (f /. x0) = x - (f /. x0) by A6, A14 .= x - x0 by A6, A13 .= (L /. (x - x0)) + 0c by A1, PARTFUN2:6 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; thus (f `| Z) /. x0 = diff (f,x0) by A12, A13, Def12 .= L /. 1r by A15, A19, A20, Def7 .= 1r by A1, PARTFUN2:6 ; ::_thesis: verum end; theorem :: CFDIFF_1:28 for f1, f2 being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) proof let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) let Z be open Subset of COMPLEX; ::_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 Element of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ f1_+_f2_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_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, Th15; hence f1 + f2 is_differentiable_in x0 by Th23; ::_thesis: verum end; hence A3: f1 + f2 is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_ ((f1_+_f2)_`|_Z)_/._x_=_(diff_(f1,x))_+_(diff_(f2,x)) let x be Element of COMPLEX ; ::_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, Th15; thus ((f1 + f2) `| Z) /. x = diff ((f1 + f2),x) by A3, A4, Def12 .= (diff (f1,x)) + (diff (f2,x)) by A5, Th23 ; ::_thesis: verum end; hence for x being Element of COMPLEX st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ; ::_thesis: verum end; theorem :: CFDIFF_1:29 for f1, f2 being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) proof let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) let Z be open Subset of COMPLEX; ::_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 Element of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ f1_-_f2_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_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, Th15; hence f1 - f2 is_differentiable_in x0 by Th24; ::_thesis: verum end; hence A3: f1 - f2 is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_ ((f1_-_f2)_`|_Z)_/._x_=_(diff_(f1,x))_-_(diff_(f2,x)) let x be Element of COMPLEX ; ::_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, Th15; thus ((f1 - f2) `| Z) /. x = diff ((f1 - f2),x) by A3, A4, Def12 .= (diff (f1,x)) - (diff (f2,x)) by A5, Th24 ; ::_thesis: verum end; hence for x being Element of COMPLEX st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ; ::_thesis: verum end; theorem :: CFDIFF_1:30 for a being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) ) ) proof let a be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) ) ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) ) ) let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom (a (#) f) & f is_differentiable_on Z implies ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) ) ) ) assume that A1: Z c= dom (a (#) f) and A2: f is_differentiable_on Z ; ::_thesis: ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) ) ) now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ a_(#)_f_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies a (#) f is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: a (#) f is_differentiable_in x0 then f is_differentiable_in x0 by A2, Th15; hence a (#) f is_differentiable_in x0 by Th25; ::_thesis: verum end; hence A3: a (#) f is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_ ((a_(#)_f)_`|_Z)_/._x_=_a_*_(diff_(f,x)) let x be Element of COMPLEX ; ::_thesis: ( x in Z implies ((a (#) f) `| Z) /. x = a * (diff (f,x)) ) assume A4: x in Z ; ::_thesis: ((a (#) f) `| Z) /. x = a * (diff (f,x)) then A5: f is_differentiable_in x by A2, Th15; thus ((a (#) f) `| Z) /. x = diff ((a (#) f),x) by A3, A4, Def12 .= a * (diff (f,x)) by A5, Th25 ; ::_thesis: verum end; hence for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) ; ::_thesis: verum end; theorem :: CFDIFF_1:31 for f1, f2 being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) ) proof let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX 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 Element of COMPLEX st x in Z holds ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) ) let Z be open Subset of COMPLEX; ::_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 Element of COMPLEX st x in Z holds ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) ) ) assume that A1: Z c= dom (f1 (#) f2) and A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 (#) f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) ) now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ f1_(#)_f2_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_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, Th15; hence f1 (#) f2 is_differentiable_in x0 by Th26; ::_thesis: verum end; hence A3: f1 (#) f2 is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_ ((f1_(#)_f2)_`|_Z)_/._x_=_((f2_/._x)_*_(diff_(f1,x)))_+_((f1_/._x)_*_(diff_(f2,x))) let x be Element of COMPLEX ; ::_thesis: ( x in Z implies ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) assume A4: x in Z ; ::_thesis: ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th15; thus ((f1 (#) f2) `| Z) /. x = diff ((f1 (#) f2),x) by A3, A4, Def12 .= ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) by A5, Th26 ; ::_thesis: verum end; hence for x being Element of COMPLEX st x in Z holds ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ; ::_thesis: verum end; theorem :: CFDIFF_1:32 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) proof let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) ) set R = cf; A1: dom cf = COMPLEX by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c A2: ( n in NAT & rng h c= dom cf ) by A1, ORDINAL1:def_12; thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5 .= ((h ") . n) * (cf /. (h . n)) by A2, FUNCT_2:109 .= ((h ") . n) * 0c by FUNCOP_1:7 .= 0c ; ::_thesis: verum end; then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18; hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum end; then reconsider R = cf as C_RestFunc by Def3; set L = cf; for x being Element of COMPLEX holds cf /. x = 0c * x by FUNCOP_1:7; then reconsider L = cf as C_LinearFunc by Def4; assume that A3: Z c= dom f and A4: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) consider a1 being Element of COMPLEX such that A5: for x being Element of COMPLEX st x in Z /\ (dom f) holds f /. x = a1 by A4, PARTFUN2:35; A6: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A7: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A8: N c= Z by Th9; A9: N c= dom f by A3, A8, XBOOLE_1:1; A10: x0 in Z /\ (dom f) by A3, A7, XBOOLE_0:def_4; for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) then x in Z /\ (dom f) by A8, A9, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5 .= a1 - a1 by A5, A10 .= (L /. (x - x0)) + 0c by FUNCOP_1:7 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; hence f is_differentiable_in x0 by A9, Def6; ::_thesis: verum end; hence A11: f is_differentiable_on Z by A3, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0c ) assume A12: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0c then consider N being Neighbourhood of x0 such that A13: N c= Z by Th9; A14: N c= dom f by A3, A13, XBOOLE_1:1; A15: x0 in Z /\ (dom f) by A3, A12, XBOOLE_0:def_4; A16: for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) then x in Z /\ (dom f) by A13, A14, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5 .= a1 - a1 by A5, A15 .= (L /. (x - x0)) + 0c by FUNCOP_1:7 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; A17: f is_differentiable_in x0 by A6, A12; thus (f `| Z) /. x0 = diff (f,x0) by A11, A12, Def12 .= L /. 1r by A17, A14, A16, Def7 .= 0c by FUNCOP_1:7 ; ::_thesis: verum end; theorem :: CFDIFF_1:33 for a, b being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f /. x = (a * x) + b ) holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = a ) ) proof let a, b be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f /. x = (a * x) + b ) holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = a ) ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f /. x = (a * x) + b ) holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = a ) ) let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f /. x = (a * x) + b ) implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = a ) ) ) set R = cf; A1: dom cf = COMPLEX by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c A2: ( n in NAT & rng h c= dom cf ) by A1, ORDINAL1:def_12; thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5 .= ((h ") . n) * (cf /. (h . n)) by A2, FUNCT_2:109 .= ((h ") . n) * 0c by FUNCOP_1:7 .= 0c ; ::_thesis: verum end; then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18; hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum end; then reconsider R = cf as C_RestFunc by Def3; assume that A3: Z c= dom f and A4: for x being Element of COMPLEX st x in Z holds f /. x = (a * x) + b ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = a ) ) deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = a * $1; consider L being Function of COMPLEX,COMPLEX such that A5: for x being Element of COMPLEX holds L . x = H1(x) from FUNCT_2:sch_4(); for z being Element of COMPLEX holds L /. z = a * z by A5; then reconsider L = L as C_LinearFunc by Def4; A6: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A7: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A8: N c= Z by Th9; A9: for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = ((a * x) + b) - (f /. x0) by A4, A8 .= ((a * x) + b) - ((a * x0) + b) by A4, A7 .= (a * (x - x0)) + 0c .= (L /. (x - x0)) + 0c by A5 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; N c= dom f by A3, A8, XBOOLE_1:1; hence f is_differentiable_in x0 by A9, Def6; ::_thesis: verum end; hence A10: f is_differentiable_on Z by A3, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = a let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = a ) assume A11: x0 in Z ; ::_thesis: (f `| Z) /. x0 = a then consider N being Neighbourhood of x0 such that A12: N c= Z by Th9; A13: for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) proof let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = ((a * x) + b) - (f /. x0) by A4, A12 .= ((a * x) + b) - ((a * x0) + b) by A4, A11 .= (a * (x - x0)) + 0c .= (L /. (x - x0)) + 0c by A5 .= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; A14: N c= dom f by A3, A12, XBOOLE_1:1; A15: f is_differentiable_in x0 by A6, A11; thus (f `| Z) /. x0 = diff (f,x0) by A10, A11, Def12 .= L /. 1r by A15, A14, A13, Def7 .= a * 1r by A5 .= a ; ::_thesis: verum end; theorem Th34: :: CFDIFF_1:34 for f being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f is_differentiable_in x0 holds f is_continuous_in x0 proof let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f is_differentiable_in x0 holds f is_continuous_in x0 let x0 be Element of COMPLEX ; ::_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 C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6; A3: x0 in N by Th7; now__::_thesis:_for_s1_being_Complex_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 such that A4: 0 < g and A5: { y where y is Complex : |.(y - x0).| < g } c= N by Def5; reconsider s2 = NAT --> x0 as Complex_Sequence ; let s1 be Complex_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 |.((s1 . m) - x0).| < g by A7, A8, A4, COMSEQ_2:def_6; A11: lim s2 = s2 . 0 by CFCONT_1:28 .= x0 by FUNCOP_1:7 ; deffunc H1( Element of NAT ) -> Element of COMPLEX = (s1 . $1) - (s2 . $1); consider s3 being Complex_Sequence such that A12: for n being Element of NAT holds s3 . n = H1(n) from FUNCT_2:sch_4(); A13: s3 = s1 - s2 by A12, CFCONT_1:1; A14: s2 is convergent by CFCONT_1:26; then A15: s3 is convergent by A7, A13; lim s3 = lim (s1 - s2) by A12, CFCONT_1:1 .= x0 - x0 by A7, A8, A14, A11, COMSEQ_2:26 .= 0c ; then A16: lim (s3 ^\ l) = 0c by A15, CFCONT_1:21; reconsider c = s2 ^\ l as constant Complex_Sequence ; A17: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s3_._n_=_0c given n being Element of NAT such that A18: s3 . n = 0c ; ::_thesis: contradiction (s1 . n) - (s2 . n) = 0c by A12, A18; hence contradiction by A9, FUNCOP_1:7; ::_thesis: verum end; A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(s3_^\_l)_._n_=_0c given n being Element of NAT such that A20: (s3 ^\ l) . n = 0c ; ::_thesis: contradiction s3 . (n + l) = 0c by A20, NAT_1:def_3; hence contradiction by A17; ::_thesis: verum end; then A21: s3 ^\ l is non-zero by COMSEQ_1:4; s3 ^\ l is convergent by A15, CFCONT_1:21; then reconsider h = s3 ^\ l as non-zero 0 -convergent Complex_Sequence by A16, A21, Def1; 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 VALUED_1:1 .= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by CFCONT_1:1 .= (f /* (h + c)) . n ; ::_thesis: verum end; then A22: ((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 A13, Th18 .= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3 .= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by VALUED_1:1 .= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by CFCONT_1:1 .= (s1 ^\ l) . n by NAT_1:def_3 ; ::_thesis: verum end; then A23: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A22, FUNCT_2:63 .= (f /* s1) ^\ l by A6, VALUED_0:27 ; A24: 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 A25: y = (s2 ^\ l) . n by FUNCT_2:113; y = s2 . (n + l) by A25, 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 A26: y = x0 by TARSKI:def_1; c . 0 = s2 . (0 + l) by NAT_1:def_3 .= y by A26, FUNCOP_1:7 ; hence y in rng c by FUNCT_2:4; ::_thesis: verum end; A27: 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 A28: 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 thus for m being Element of NAT st n <= m holds |.(((f /* c) . m) - (f /. x0)).| < p ::_thesis: verum proof 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} c= dom f by A2, A3, ZFMISC_1:31; then |.(((f /* c) . m) - (f /. x0)).| = |.((f /. (c . m)) - (f /. x0)).| by A24, FUNCT_2:109 .= |.((f /. (s2 . (m + l))) - (f /. x0)).| by NAT_1:def_3 .= |.((f /. x0) - (f /. x0)).| by FUNCOP_1:7 .= 0 by ABSVALUE:2 ; hence |.(((f /* c) . m) - (f /. x0)).| < p by A28; ::_thesis: verum end; end; then A29: f /* c is convergent by COMSEQ_2:def_5; 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 A19; thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by VALUED_1:5 .= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:5 .= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10 .= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n) .= 1 * (((f /* (h + c)) - (f /* c)) . n) by A30, XCMPLX_0:def_7 .= ((f /* (h + c)) - (f /* c)) . n ; ::_thesis: verum end; then A31: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63; rng (h + c) c= N proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in N ) assume A32: y in rng (h + c) ; ::_thesis: y in N then consider n being Element of NAT such that A33: y = (h + c) . n by FUNCT_2:113; reconsider y1 = y as Complex by A32; (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A13, Th18 .= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3 .= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by VALUED_1:1 .= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by CFCONT_1:1 .= s1 . (l + n) ; then |.(((h + c) . n) - x0).| < g by A10, NAT_1:12; then y1 in { z where z is Complex : |.(z - x0).| < g } by A33; hence y in N by A5; ::_thesis: verum end; then A34: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A2, A24, Th22; then A35: (f /* (h + c)) - (f /* c) is convergent by A31; then A36: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A29; hence f /* s1 is convergent by A23, CFCONT_1:22; ::_thesis: f /. x0 = lim (f /* s1) lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0c * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A16, A34, COMSEQ_2:30 .= 0 ; then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0c + (lim (f /* c)) by A31, A35, A29, COMSEQ_2:14 .= f /. x0 by A27, A29, COMSEQ_2:def_6 ; hence f /. x0 = lim (f /* s1) by A36, A23, CFCONT_1:23; ::_thesis: verum end; hence f is_continuous_in x0 by A2, A3, CFCONT_1:31; ::_thesis: verum end; theorem :: CFDIFF_1:35 for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds f is_continuous_on X proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds f is_continuous_on X let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_on X implies f is_continuous_on X ) assume A1: f is_differentiable_on X ; ::_thesis: f is_continuous_on X hence A2: X c= dom f by Def9; :: according to CFCONT_1:def_2 ::_thesis: for b1 being Element of COMPLEX holds ( not b1 in X or f | X is_continuous_in b1 ) let x be Element of COMPLEX ; ::_thesis: ( not x in X or f | X is_continuous_in x ) assume x in X ; ::_thesis: f | X is_continuous_in x then A3: x in dom (f | X) by A2, RELAT_1:57; f | X is differentiable by A1, Def9; then f | X is_differentiable_in x by A3, Def8; hence f | X is_continuous_in x by Th34; ::_thesis: verum end; theorem :: CFDIFF_1:36 for X being set for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let Z be open Subset of COMPLEX; ::_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 A3: f | X is differentiable by A1, Def9; X c= dom f by A1, Def9; hence Z c= dom f by A2, XBOOLE_1:1; :: according to CFDIFF_1:def_9 ::_thesis: f | Z is differentiable let x0 be Element of COMPLEX ; :: according to CFDIFF_1:def_8 ::_thesis: ( x0 in dom (f | Z) implies f | Z is_differentiable_in x0 ) assume A4: x0 in dom (f | Z) ; ::_thesis: f | Z is_differentiable_in x0 then A5: x0 in dom f by RELAT_1:57; A6: x0 in Z by A4, RELAT_1:57; then consider N1 being Neighbourhood of x0 such that A7: N1 c= Z by Th9; x0 in dom (f | X) by A2, A5, A6, RELAT_1:57; then f | X is_differentiable_in x0 by A3, Def8; then consider N being Neighbourhood of x0 such that A8: N c= dom (f | X) and A9: ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds ((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6; consider N2 being Neighbourhood of x0 such that A10: N2 c= N and A11: N2 c= N1 by Lm1; A12: N2 c= Z by A7, A11, XBOOLE_1:1; take N2 ; :: according to CFDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) ) dom (f | X) = (dom f) /\ X by RELAT_1:61; then dom (f | X) c= dom f by XBOOLE_1:17; then N c= dom f by A8, XBOOLE_1:1; then N2 c= dom f by A10, XBOOLE_1:1; then N2 c= (dom f) /\ Z by A12, XBOOLE_1:19; hence A13: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) consider L being C_LinearFunc, R being C_RestFunc such that A14: for x being Element of COMPLEX st x in N holds ((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A9; take L ; ::_thesis: ex R being C_RestFunc st for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) take R ; ::_thesis: for z being Element of COMPLEX st z in N2 holds ((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) let x be Element of COMPLEX ; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) assume A15: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) then ((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A10, A14; then A16: ((f | X) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, A5, A6, PARTFUN2:17; x in N by A10, A15; then (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A8, A16, PARTFUN2:15; then (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5, A6, PARTFUN2:17; hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A13, A15, PARTFUN2:15; ::_thesis: verum end; theorem :: CFDIFF_1:37 canceled; theorem :: CFDIFF_1:38 for x0 being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds ex R being C_RestFunc st ( R /. 0c = 0c & R is_continuous_in 0c ) proof let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds ex R being C_RestFunc st ( R /. 0c = 0c & R is_continuous_in 0c ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_in x0 implies ex R being C_RestFunc st ( R /. 0c = 0c & R is_continuous_in 0c ) ) assume f is_differentiable_in x0 ; ::_thesis: ex R being C_RestFunc st ( R /. 0c = 0c & R is_continuous_in 0c ) then consider N being Neighbourhood of x0 such that N c= dom f and A1: ex L being C_LinearFunc ex R being C_RestFunc st for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6; consider L being C_LinearFunc, R being C_RestFunc such that A2: for x being Element of COMPLEX st x in N holds (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1; take R ; ::_thesis: ( R /. 0c = 0c & R is_continuous_in 0c ) consider a being Element of COMPLEX such that A3: for z being Element of COMPLEX holds L /. z = a * z by Def4; (f /. x0) - (f /. x0) = (L /. (x0 - x0)) + (R /. (x0 - x0)) by A2, Th7; then A4: 0c = (a * 0c) + (R /. 0c) by A3; hence R /. 0c = 0c ; ::_thesis: R is_continuous_in 0c A5: now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_ (_R_/*_h_is_convergent_&_lim_(R_/*_h)_=_R_/._0c_) let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( R /* h is convergent & lim (R /* h) = R /. 0c ) (h ") (#) (R /* h) is bounded by Def3; then consider M being Real such that M > 0 and A6: for n being Element of NAT holds |.(((h ") (#) (R /* h)) . n).| < M by COMSEQ_2:8; lim h = 0 by Def1; then lim |.h.| = |.0.| by SEQ_2:27; then A7: lim (M (#) |.h.|) = M * |.0.| by SEQ_2:8 .= M * 0 by ABSVALUE:2 .= 0 ; A8: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ |.(((R_/*_h)_._n)_-_0c).|_<_p let p be Real; ::_thesis: ( 0 < p implies ex m being Element of NAT st for n being Element of NAT st m <= n holds |.(((R /* h) . n) - 0c).| < p ) assume 0 < p ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds |.(((R /* h) . n) - 0c).| < p then consider m being Element of NAT such that A9: for n being Element of NAT st m <= n holds abs (((M (#) |.h.|) . n) - 0) < p by A7, SEQ_2:def_7; take m = m; ::_thesis: for n being Element of NAT st m <= n holds |.(((R /* h) . n) - 0c).| < p now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_ |.(((R_/*_h)_._n)_-_0c).|_<_p let n be Element of NAT ; ::_thesis: ( m <= n implies |.(((R /* h) . n) - 0c).| < p ) assume m <= n ; ::_thesis: |.(((R /* h) . n) - 0c).| < p then A10: abs (((M (#) |.h.|) . n) - 0) < p by A9; |.(((h ") (#) (R /* h)) . n).| = |.(((h ") . n) * ((R /* h) . n)).| by VALUED_1:5 .= |.(((h . n) ") * ((R /* h) . n)).| by VALUED_1:10 ; then A11: |.(((h . n) ") * ((R /* h) . n)).| <= M by A6; |.(h . n).| >= 0 by COMPLEX1:46; then |.(h . n).| * |.(((h . n) ") * ((R /* h) . n)).| <= M * |.(h . n).| by A11, XREAL_1:64; then |.((h . n) * (((h . n) ") * ((R /* h) . n))).| <= M * |.(h . n).| by COMPLEX1:65; then ( h . n <> 0c & |.(((h . n) * ((h . n) ")) * ((R /* h) . n)).| <= M * |.(h . n).| ) by COMSEQ_1:4; then |.(1r * ((R /* h) . n)).| <= M * |.(h . n).| by XCMPLX_0:def_7; then |.((R /* h) . n).| <= M * (|.h.| . n) by VALUED_1:18; then A12: |.((R /* h) . n).| <= (M (#) |.h.|) . n by SEQ_1:9; then 0 <= (M (#) |.h.|) . n by COMPLEX1:46; then (M (#) |.h.|) . n < p by A10, ABSVALUE:def_1; hence |.(((R /* h) . n) - 0c).| < p by A12, XXREAL_0:2; ::_thesis: verum end; hence for n being Element of NAT st m <= n holds |.(((R /* h) . n) - 0c).| < p ; ::_thesis: verum end; hence R /* h is convergent by COMSEQ_2:def_5; ::_thesis: lim (R /* h) = R /. 0c hence lim (R /* h) = R /. 0c by A4, A8, COMSEQ_2:def_6; ::_thesis: verum end; A13: now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_R_&_s1_is_convergent_&_lim_s1_=_0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_0_)_holds_ (_R_/*_s1_is_convergent_&_lim_(R_/*_s1)_=_R_/._0c_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Element of NAT holds s1 . n <> 0 ) implies ( R /* s1 is convergent & lim (R /* s1) = R /. 0c ) ) assume that rng s1 c= dom R and A14: ( s1 is convergent & lim s1 = 0 ) and A15: for n being Element of NAT holds s1 . n <> 0 ; ::_thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. 0c ) s1 is non-zero by A15, COMSEQ_1:4; then s1 is non-zero 0 -convergent Complex_Sequence by A14, Def1; hence ( R /* s1 is convergent & lim (R /* s1) = R /. 0c ) by A5; ::_thesis: verum end; dom R = COMPLEX by PARTFUN1:def_2; hence R is_continuous_in 0c by A13, CFCONT_1:31; ::_thesis: verum end;