:: CFCONT_1 semantic presentation begin definition let f be PartFunc of COMPLEX,COMPLEX; let x0 be Element of COMPLEX ; predf is_continuous_in x0 means :Def1: :: CFCONT_1:def 1 ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ); end; :: deftheorem Def1 defines is_continuous_in CFCONT_1:def_1_:_ for f being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ); theorem Th1: :: CFCONT_1:1 for seq1, seq2, seq3 being Complex_Sequence holds ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) thus ( seq1 = seq2 - seq3 implies for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 ) proof assume A1: seq1 = seq2 - seq3 ; ::_thesis: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_-_(seq3_._n) let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) - (seq3 . n) seq1 . n = (seq2 . n) + ((- seq3) . n) by A1, VALUED_1:1; then seq1 . n = (seq2 . n) + (- (seq3 . n)) by VALUED_1:8; hence seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum end; hence for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum end; assume A2: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: seq1 = seq2 - seq3 now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_+_(-_seq3))_._n let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 + (- seq3)) . n thus seq1 . n = (seq2 . n) - (seq3 . n) by A2 .= (seq2 . n) + (- (seq3 . n)) .= (seq2 . n) + ((- seq3) . n) by VALUED_1:8 .= (seq2 + (- seq3)) . n by VALUED_1:1 ; ::_thesis: verum end; hence seq1 = seq2 - seq3 by FUNCT_2:63; ::_thesis: verum end; theorem Th2: :: CFCONT_1:2 for seq1, seq2 being Complex_Sequence for Ns being V37() sequence of NAT holds ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) let Ns be V37() sequence of NAT; ::_thesis: ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_+_(seq2_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) * Ns) . n = ((seq1 * Ns) + (seq2 * Ns)) . n thus ((seq1 + seq2) * Ns) . n = (seq1 + seq2) . (Ns . n) by FUNCT_2:15 .= (seq1 . (Ns . n)) + (seq2 . (Ns . n)) by VALUED_1:1 .= ((seq1 * Ns) . n) + (seq2 . (Ns . n)) by FUNCT_2:15 .= ((seq1 * Ns) . n) + ((seq2 * Ns) . n) by FUNCT_2:15 .= ((seq1 * Ns) + (seq2 * Ns)) . n by VALUED_1:1 ; ::_thesis: verum end; hence (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) by FUNCT_2:63; ::_thesis: ( (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_-_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_-_(seq2_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((seq1 - seq2) * Ns) . n = ((seq1 * Ns) - (seq2 * Ns)) . n thus ((seq1 - seq2) * Ns) . n = (seq1 - seq2) . (Ns . n) by FUNCT_2:15 .= (seq1 . (Ns . n)) - (seq2 . (Ns . n)) by Th1 .= ((seq1 * Ns) . n) - (seq2 . (Ns . n)) by FUNCT_2:15 .= ((seq1 * Ns) . n) - ((seq2 * Ns) . n) by FUNCT_2:15 .= ((seq1 * Ns) - (seq2 * Ns)) . n by Th1 ; ::_thesis: verum end; hence (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) by FUNCT_2:63; ::_thesis: (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_(#)_(seq2_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) * Ns) . n = ((seq1 * Ns) (#) (seq2 * Ns)) . n thus ((seq1 (#) seq2) * Ns) . n = (seq1 (#) seq2) . (Ns . n) by FUNCT_2:15 .= (seq1 . (Ns . n)) * (seq2 . (Ns . n)) by VALUED_1:5 .= ((seq1 * Ns) . n) * (seq2 . (Ns . n)) by FUNCT_2:15 .= ((seq1 * Ns) . n) * ((seq2 * Ns) . n) by FUNCT_2:15 .= ((seq1 * Ns) (#) (seq2 * Ns)) . n by VALUED_1:5 ; ::_thesis: verum end; hence (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) by FUNCT_2:63; ::_thesis: verum end; theorem Th3: :: CFCONT_1:3 for g being Element of COMPLEX for seq being Complex_Sequence for Ns being V37() sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns) proof let g be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence for Ns being V37() sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns) let seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns) let Ns be V37() sequence of NAT; ::_thesis: (g (#) seq) * Ns = g (#) (seq * Ns) now__::_thesis:_for_n_being_Element_of_NAT_holds_((g_(#)_seq)_*_Ns)_._n_=_(g_(#)_(seq_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((g (#) seq) * Ns) . n = (g (#) (seq * Ns)) . n thus ((g (#) seq) * Ns) . n = (g (#) seq) . (Ns . n) by FUNCT_2:15 .= g * (seq . (Ns . n)) by VALUED_1:6 .= g * ((seq * Ns) . n) by FUNCT_2:15 .= (g (#) (seq * Ns)) . n by VALUED_1:6 ; ::_thesis: verum end; hence (g (#) seq) * Ns = g (#) (seq * Ns) by FUNCT_2:63; ::_thesis: verum end; theorem :: CFCONT_1:4 for seq being Complex_Sequence for Ns being V37() sequence of NAT holds ( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| ) proof let seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds ( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| ) let Ns be V37() sequence of NAT; ::_thesis: ( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| ) thus (- seq) * Ns = ((- 1r) (#) seq) * Ns by COMSEQ_1:11 .= (- 1r) (#) (seq * Ns) by Th3 .= - (seq * Ns) by COMSEQ_1:11 ; ::_thesis: |.seq.| * Ns = |.(seq * Ns).| now__::_thesis:_for_n_being_Element_of_NAT_holds_(|.seq.|_*_Ns)_._n_=_|.(seq_*_Ns).|_._n let n be Element of NAT ; ::_thesis: (|.seq.| * Ns) . n = |.(seq * Ns).| . n thus (|.seq.| * Ns) . n = |.seq.| . (Ns . n) by FUNCT_2:15 .= |.(seq . (Ns . n)).| by VALUED_1:18 .= |.((seq * Ns) . n).| by FUNCT_2:15 .= |.(seq * Ns).| . n by VALUED_1:18 ; ::_thesis: verum end; hence |.seq.| * Ns = |.(seq * Ns).| by FUNCT_2:63; ::_thesis: verum end; theorem Th5: :: CFCONT_1:5 for seq being Complex_Sequence for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns proof let seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns let Ns be V37() sequence of NAT; ::_thesis: (seq * Ns) " = (seq ") * Ns now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_*_Ns)_")_._n_=_((seq_")_*_Ns)_._n let n be Element of NAT ; ::_thesis: ((seq * Ns) ") . n = ((seq ") * Ns) . n thus ((seq * Ns) ") . n = ((seq * Ns) . n) " by VALUED_1:10 .= (seq . (Ns . n)) " by FUNCT_2:15 .= (seq ") . (Ns . n) by VALUED_1:10 .= ((seq ") * Ns) . n by FUNCT_2:15 ; ::_thesis: verum end; hence (seq * Ns) " = (seq ") * Ns by FUNCT_2:63; ::_thesis: verum end; theorem :: CFCONT_1:6 for seq1, seq being Complex_Sequence for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns) proof let seq1, seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns) let Ns be V37() sequence of NAT; ::_thesis: (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns) thus (seq1 /" seq) * Ns = (seq1 * Ns) (#) ((seq ") * Ns) by Th2 .= (seq1 * Ns) /" (seq * Ns) by Th5 ; ::_thesis: verum end; theorem Th7: :: CFCONT_1:7 for seq being Complex_Sequence for h1, h2 being PartFunc of COMPLEX,COMPLEX st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) proof let seq be Complex_Sequence; ::_thesis: for h1, h2 being PartFunc of COMPLEX,COMPLEX st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) let h1, h2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) ) A1: (dom h1) /\ (dom h2) c= dom h1 by XBOOLE_1:17; A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17; assume A3: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) then A4: rng seq c= dom (h1 + h2) by VALUED_1:def_1; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_+_h2)_/*_seq)_._n_=_((h1_/*_seq)_+_(h2_/*_seq))_._n let n be Element of NAT ; ::_thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) + (h2 /* seq)) . n A5: seq . n in rng seq by VALUED_0:28; thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A4, FUNCT_2:109 .= (h1 /. (seq . n)) + (h2 /. (seq . n)) by A4, A5, CFUNCT_1:1 .= ((h1 /* seq) . n) + (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) + (h2 /* seq)) . n by VALUED_1:1 ; ::_thesis: verum end; hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by FUNCT_2:63; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) A6: rng seq c= dom (h1 - h2) by A3, CFUNCT_1:2; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_-_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_-_((h2_/*_seq)_._n) let n be Element of NAT ; ::_thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n) A7: seq . n in rng seq by VALUED_0:28; thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A6, FUNCT_2:109 .= (h1 /. (seq . n)) - (h2 /. (seq . n)) by A6, A7, CFUNCT_1:2 .= ((h1 /* seq) . n) - (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum end; hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by Th1; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) A8: rng seq c= dom (h1 (#) h2) by A3, VALUED_1:def_4; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_(#)_h2)_/*_seq)_._n_=_((h1_/*_seq)_(#)_(h2_/*_seq))_._n let n be Element of NAT ; ::_thesis: ((h1 (#) h2) /* seq) . n = ((h1 /* seq) (#) (h2 /* seq)) . n A9: seq . n in rng seq by VALUED_0:28; thus ((h1 (#) h2) /* seq) . n = (h1 (#) h2) /. (seq . n) by A8, FUNCT_2:109 .= (h1 /. (seq . n)) * (h2 /. (seq . n)) by A8, A9, CFUNCT_1:3 .= ((h1 /* seq) . n) * (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) . n) * ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) (#) (h2 /* seq)) . n by VALUED_1:5 ; ::_thesis: verum end; hence (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th8: :: CFCONT_1:8 for g being Element of COMPLEX for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds (g (#) h) /* seq = g (#) (h /* seq) proof let g be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds (g (#) h) /* seq = g (#) (h /* seq) let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds (g (#) h) /* seq = g (#) (h /* seq) let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom h implies (g (#) h) /* seq = g (#) (h /* seq) ) assume A1: rng seq c= dom h ; ::_thesis: (g (#) h) /* seq = g (#) (h /* seq) then A2: rng seq c= dom (g (#) h) by VALUED_1:def_5; now__::_thesis:_for_n_being_Element_of_NAT_holds_((g_(#)_h)_/*_seq)_._n_=_(g_(#)_(h_/*_seq))_._n let n be Element of NAT ; ::_thesis: ((g (#) h) /* seq) . n = (g (#) (h /* seq)) . n A3: seq . n in rng seq by VALUED_0:28; thus ((g (#) h) /* seq) . n = (g (#) h) /. (seq . n) by A2, FUNCT_2:109 .= g * (h /. (seq . n)) by A2, A3, CFUNCT_1:4 .= g * ((h /* seq) . n) by A1, FUNCT_2:109 .= (g (#) (h /* seq)) . n by VALUED_1:6 ; ::_thesis: verum end; hence (g (#) h) /* seq = g (#) (h /* seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: CFCONT_1:9 for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds - (h /* seq) = (- h) /* seq proof let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds - (h /* seq) = (- h) /* seq let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom h implies - (h /* seq) = (- h) /* seq ) assume A1: rng seq c= dom h ; ::_thesis: - (h /* seq) = (- h) /* seq thus - (h /* seq) = (- 1r) (#) (h /* seq) by COMSEQ_1:11 .= ((- 1r) (#) h) /* seq by A1, Th8 .= (- h) /* seq by CFUNCT_1:31 ; ::_thesis: verum end; theorem Th10: :: CFCONT_1:10 for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds h /* seq is non-zero proof let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds h /* seq is non-zero let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom (h ^) implies h /* seq is non-zero ) assume A1: rng seq c= dom (h ^) ; ::_thesis: h /* seq is non-zero then A2: ( (dom h) \ (h " {0c}) c= dom h & rng seq c= (dom h) \ (h " {0c}) ) by CFUNCT_1:def_2, XBOOLE_1:36; now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(h_/*_seq)_._n_=_0c given n being Element of NAT such that A3: (h /* seq) . n = 0c ; ::_thesis: contradiction seq . n in rng seq by VALUED_0:28; then seq . n in dom (h ^) by A1; then seq . n in (dom h) \ (h " {0c}) by CFUNCT_1:def_2; then ( seq . n in dom h & not seq . n in h " {0c} ) by XBOOLE_0:def_5; then A4: not h /. (seq . n) in {0c} by PARTFUN2:26; h /. (seq . n) = 0c by A2, A3, FUNCT_2:109, XBOOLE_1:1; hence contradiction by A4, TARSKI:def_1; ::_thesis: verum end; hence h /* seq is non-zero by COMSEQ_1:4; ::_thesis: verum end; theorem Th11: :: CFCONT_1:11 for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds (h ^) /* seq = (h /* seq) " proof let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds (h ^) /* seq = (h /* seq) " let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom (h ^) implies (h ^) /* seq = (h /* seq) " ) assume A1: rng seq c= dom (h ^) ; ::_thesis: (h ^) /* seq = (h /* seq) " then A2: ( (dom h) \ (h " {0c}) c= dom h & rng seq c= (dom h) \ (h " {0c}) ) by CFUNCT_1:def_2, XBOOLE_1:36; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_^)_/*_seq)_._n_=_((h_/*_seq)_")_._n let n be Element of NAT ; ::_thesis: ((h ^) /* seq) . n = ((h /* seq) ") . n A3: seq . n in rng seq by VALUED_0:28; thus ((h ^) /* seq) . n = (h ^) /. (seq . n) by A1, FUNCT_2:109 .= (h /. (seq . n)) " by A1, A3, CFUNCT_1:def_2 .= ((h /* seq) . n) " by A2, FUNCT_2:109, XBOOLE_1:1 .= ((h /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence (h ^) /* seq = (h /* seq) " by FUNCT_2:63; ::_thesis: verum end; theorem :: CFCONT_1:12 for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX for Ns being V37() sequence of NAT st rng seq c= dom h holds Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) proof let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX for Ns being V37() sequence of NAT st rng seq c= dom h holds Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Ns being V37() sequence of NAT st rng seq c= dom h holds Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) let Ns be V37() sequence of NAT; ::_thesis: ( rng seq c= dom h implies Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) ) assume A1: rng seq c= dom h ; ::_thesis: Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_((h_/*_seq)_*_Ns))_._n_=_(Re_(h_/*_(seq_*_Ns)))_._n let n be Element of NAT ; ::_thesis: (Re ((h /* seq) * Ns)) . n = (Re (h /* (seq * Ns))) . n seq * Ns is subsequence of seq by VALUED_0:def_17; then A2: rng (seq * Ns) c= rng seq by VALUED_0:21; thus (Re ((h /* seq) * Ns)) . n = Re (((h /* seq) * Ns) . n) by COMSEQ_3:def_5 .= Re ((h /* seq) . (Ns . n)) by FUNCT_2:15 .= Re (h /. (seq . (Ns . n))) by A1, FUNCT_2:109 .= Re (h /. ((seq * Ns) . n)) by FUNCT_2:15 .= Re ((h /* (seq * Ns)) . n) by A1, A2, FUNCT_2:109, XBOOLE_1:1 .= (Re (h /* (seq * Ns))) . n by COMSEQ_3:def_5 ; ::_thesis: verum end; hence Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) by FUNCT_2:63; ::_thesis: verum end; theorem :: CFCONT_1:13 for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX for Ns being V37() sequence of NAT st rng seq c= dom h holds Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) proof let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX for Ns being V37() sequence of NAT st rng seq c= dom h holds Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Ns being V37() sequence of NAT st rng seq c= dom h holds Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) let Ns be V37() sequence of NAT; ::_thesis: ( rng seq c= dom h implies Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) ) assume A1: rng seq c= dom h ; ::_thesis: Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_((h_/*_seq)_*_Ns))_._n_=_(Im_(h_/*_(seq_*_Ns)))_._n let n be Element of NAT ; ::_thesis: (Im ((h /* seq) * Ns)) . n = (Im (h /* (seq * Ns))) . n seq * Ns is subsequence of seq by VALUED_0:def_17; then A2: rng (seq * Ns) c= rng seq by VALUED_0:21; thus (Im ((h /* seq) * Ns)) . n = Im (((h /* seq) * Ns) . n) by COMSEQ_3:def_6 .= Im ((h /* seq) . (Ns . n)) by FUNCT_2:15 .= Im (h /. (seq . (Ns . n))) by A1, FUNCT_2:109 .= Im (h /. ((seq * Ns) . n)) by FUNCT_2:15 .= Im ((h /* (seq * Ns)) . n) by A1, A2, FUNCT_2:109, XBOOLE_1:1 .= (Im (h /* (seq * Ns))) . n by COMSEQ_3:def_6 ; ::_thesis: verum end; hence Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) by FUNCT_2:63; ::_thesis: verum end; theorem :: CFCONT_1:14 for seq being Complex_Sequence for h1, h2 being PartFunc of COMPLEX,COMPLEX st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) proof let seq be Complex_Sequence; ::_thesis: for h1, h2 being PartFunc of COMPLEX,COMPLEX st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) let h1, h2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) ) assume ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) then dom (h1 + h2) = COMPLEX by PARTFUN1:def_2; then (dom h1) /\ (dom h2) = COMPLEX by VALUED_1:def_1; then A1: rng seq c= (dom h1) /\ (dom h2) ; hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by Th7; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, Th7; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) thus (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by A1, Th7; ::_thesis: verum end; theorem :: CFCONT_1:15 for g being Element of COMPLEX for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st h is total holds (g (#) h) /* seq = g (#) (h /* seq) proof let g be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st h is total holds (g (#) h) /* seq = g (#) (h /* seq) let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st h is total holds (g (#) h) /* seq = g (#) (h /* seq) let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( h is total implies (g (#) h) /* seq = g (#) (h /* seq) ) assume h is total ; ::_thesis: (g (#) h) /* seq = g (#) (h /* seq) then dom h = COMPLEX by PARTFUN1:def_2; then rng seq c= dom h ; hence (g (#) h) /* seq = g (#) (h /* seq) by Th8; ::_thesis: verum end; theorem :: CFCONT_1:16 for X being set for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " {0} = {} holds ((h ^) | X) /* seq = ((h | X) /* seq) " proof let X be set ; ::_thesis: for seq being Complex_Sequence for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " {0} = {} holds ((h ^) | X) /* seq = ((h | X) /* seq) " let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " {0} = {} holds ((h ^) | X) /* seq = ((h | X) /* seq) " let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom (h | X) & h " {0} = {} implies ((h ^) | X) /* seq = ((h | X) /* seq) " ) assume that A1: rng seq c= dom (h | X) and A2: h " {0} = {} ; ::_thesis: ((h ^) | X) /* seq = ((h | X) /* seq) " now__::_thesis:_for_x_being_set_st_x_in_rng_seq_holds_ x_in_dom_((h_^)_|_X) let x be set ; ::_thesis: ( x in rng seq implies x in dom ((h ^) | X) ) assume x in rng seq ; ::_thesis: x in dom ((h ^) | X) then x in dom (h | X) by A1; then A3: x in (dom h) /\ X by RELAT_1:61; then x in (dom h) \ (h " {0c}) by A2, XBOOLE_0:def_4; then A4: x in dom (h ^) by CFUNCT_1:def_2; x in X by A3, XBOOLE_0:def_4; then x in (dom (h ^)) /\ X by A4, XBOOLE_0:def_4; hence x in dom ((h ^) | X) by RELAT_1:61; ::_thesis: verum end; then A5: rng seq c= dom ((h ^) | X) by TARSKI:def_3; now__::_thesis:_for_n_being_Element_of_NAT_holds_(((h_^)_|_X)_/*_seq)_._n_=_(((h_|_X)_/*_seq)_")_._n let n be Element of NAT ; ::_thesis: (((h ^) | X) /* seq) . n = (((h | X) /* seq) ") . n A6: seq . n in rng seq by VALUED_0:28; then seq . n in dom (h | X) by A1; then A7: seq . n in (dom h) /\ X by RELAT_1:61; then seq . n in (dom h) \ (h " {0c}) by A2, XBOOLE_0:def_4; then A8: seq . n in dom (h ^) by CFUNCT_1:def_2; seq . n in X by A7, XBOOLE_0:def_4; then seq . n in (dom (h ^)) /\ X by A8, XBOOLE_0:def_4; then A9: seq . n in dom ((h ^) | X) by RELAT_1:61; thus (((h ^) | X) /* seq) . n = ((h ^) | X) /. (seq . n) by A5, FUNCT_2:109 .= (h ^) /. (seq . n) by A9, PARTFUN2:15 .= (h /. (seq . n)) " by A8, CFUNCT_1:def_2 .= ((h | X) /. (seq . n)) " by A1, A6, PARTFUN2:15 .= (((h | X) /* seq) . n) " by A1, FUNCT_2:109 .= (((h | X) /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence ((h ^) | X) /* seq = ((h | X) /* seq) " by FUNCT_2:63; ::_thesis: verum end; theorem Th17: :: CFCONT_1:17 for seq1, seq being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds seq1 is convergent proof let seq1, seq be Complex_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies seq1 is convergent ) assume that A1: seq1 is subsequence of seq and A2: seq is convergent ; ::_thesis: seq1 is convergent consider g being Element of COMPLEX such that A3: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g).| < p by A2, COMSEQ_2:def_5; take t = g; :: 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 <= |.K65((seq1 . b3),t).| ) ) 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 <= |.K65((seq1 . b2),t).| ) ) assume 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= |.K65((seq1 . b2),t).| ) then consider n1 being Element of NAT such that A4: for m being Element of NAT st n1 <= m holds |.((seq . m) - g).| < p by A3; take n = n1; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= |.K65((seq1 . b1),t).| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.K65((seq1 . m),t).| ) assume A5: n <= m ; ::_thesis: not p <= |.K65((seq1 . m),t).| consider Nseq being V37() sequence of NAT such that A6: seq1 = seq * Nseq by A1, VALUED_0:def_17; m <= Nseq . m by SEQM_3:14; then A7: n <= Nseq . m by A5, XXREAL_0:2; seq1 . m = seq . (Nseq . m) by A6, FUNCT_2:15; hence |.((seq1 . m) - t).| < p by A4, A7; ::_thesis: verum end; theorem Th18: :: CFCONT_1:18 for seq1, seq being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds lim seq1 = lim seq proof let seq1, seq be Complex_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq ) assume that A1: seq1 is subsequence of seq and A2: seq is convergent ; ::_thesis: lim seq1 = lim seq consider Nseq being V37() sequence of NAT such that A3: seq1 = seq * Nseq by A1, VALUED_0:def_17; A4: 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_ |.((seq1_._m)_-_(lim_seq)).|_<_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 |.((seq1 . m) - (lim seq)).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds |.((seq . m) - (lim seq)).| < p by A2, COMSEQ_2:def_6; take n = n1; ::_thesis: for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p ) assume A6: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p m <= Nseq . m by SEQM_3:14; then A7: n <= Nseq . m by A6, XXREAL_0:2; seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15; hence |.((seq1 . m) - (lim seq)).| < p by A5, A7; ::_thesis: verum end; seq1 is convergent by A1, A2, Th17; hence lim seq1 = lim seq by A4, COMSEQ_2:def_6; ::_thesis: verum end; theorem Th19: :: CFCONT_1:19 for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Element of NAT st for n being Element of NAT st k <= n holds seq1 . n = seq . n holds seq1 is convergent proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st for n being Element of NAT st k <= n holds seq1 . n = seq . n implies seq1 is convergent ) assume that A1: seq is convergent and A2: ex k being Element of NAT st for n being Element of NAT st k <= n holds seq1 . n = seq . n ; ::_thesis: seq1 is convergent consider g1 being Element of COMPLEX such that A3: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g1).| < p by A1, COMSEQ_2:def_5; consider k being Element of NAT such that A4: for n being Element of NAT st k <= n holds seq1 . n = seq . n by A2; take g = g1; :: 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 <= |.K65((seq1 . 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 <= |.K65((seq1 . b2),g).| ) ) assume 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= |.K65((seq1 . b2),g).| ) then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds |.((seq . m) - g1).| < p by A3; A6: now__::_thesis:_(_n1_<=_k_implies_ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((seq1_._m)_-_g).|_<_p_) assume A7: n1 <= k ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - g).| < p take n = k; ::_thesis: for m being Element of NAT st n <= m holds |.((seq1 . m) - g).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - g).| < p ) assume A8: n <= m ; ::_thesis: |.((seq1 . m) - g).| < p then n1 <= m by A7, XXREAL_0:2; then |.((seq . m) - g1).| < p by A5; hence |.((seq1 . m) - g).| < p by A4, A8; ::_thesis: verum end; now__::_thesis:_(_k_<=_n1_implies_ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((seq1_._m)_-_g).|_<_p_) assume A9: k <= n1 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - g).| < p take n = n1; ::_thesis: for m being Element of NAT st n <= m holds |.((seq1 . m) - g).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - g).| < p ) assume A10: n <= m ; ::_thesis: |.((seq1 . m) - g).| < p then seq1 . m = seq . m by A4, A9, XXREAL_0:2; hence |.((seq1 . m) - g).| < p by A5, A10; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - g).| < p by A6; ::_thesis: verum end; theorem :: CFCONT_1:20 for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Element of NAT st for n being Element of NAT st k <= n holds seq1 . n = seq . n holds lim seq = lim seq1 proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st for n being Element of NAT st k <= n holds seq1 . n = seq . n implies lim seq = lim seq1 ) assume that A1: seq is convergent and A2: ex k being Element of NAT st for n being Element of NAT st k <= n holds seq1 . n = seq . n ; ::_thesis: lim seq = lim seq1 consider k being Element of NAT such that A3: for n being Element of NAT st k <= n holds seq1 . n = seq . n by A2; A4: 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_ |.((seq1_._m)_-_(lim_seq)).|_<_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 |.((seq1 . m) - (lim seq)).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds |.((seq . m) - (lim seq)).| < p by A1, COMSEQ_2:def_6; A6: now__::_thesis:_(_n1_<=_k_implies_ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((seq1_._m)_-_(lim_seq)).|_<_p_) assume A7: n1 <= k ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p take n = k; ::_thesis: for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p ) assume A8: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p then n1 <= m by A7, XXREAL_0:2; then |.((seq . m) - (lim seq)).| < p by A5; hence |.((seq1 . m) - (lim seq)).| < p by A3, A8; ::_thesis: verum end; now__::_thesis:_(_k_<=_n1_implies_ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((seq1_._m)_-_(lim_seq)).|_<_p_) assume A9: k <= n1 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p take n = n1; ::_thesis: for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p ) assume A10: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p then seq1 . m = seq . m by A3, A9, XXREAL_0:2; hence |.((seq1 . m) - (lim seq)).| < p by A5, A10; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p by A6; ::_thesis: verum end; seq1 is convergent by A1, A2, Th19; hence lim seq = lim seq1 by A4, COMSEQ_2:def_6; ::_thesis: verum end; theorem :: CFCONT_1:21 for k being Element of NAT for seq being Complex_Sequence st seq is convergent holds ( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th17, Th18; theorem Th22: :: CFCONT_1:22 for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds seq1 is convergent proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is convergent ) assume that A1: seq is convergent and A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: seq1 is convergent consider k being Element of NAT such that A3: seq = seq1 ^\ k by A2; consider g1 being Element of COMPLEX such that A4: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g1).| < p by A1, COMSEQ_2:def_5; take g = g1; :: 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 <= |.K65((seq1 . 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 <= |.K65((seq1 . b2),g).| ) ) assume 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= |.K65((seq1 . b2),g).| ) then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds |.((seq . m) - g1).| < p by A4; take n = n1 + k; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= |.K65((seq1 . b1),g).| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.K65((seq1 . m),g).| ) assume A6: n <= m ; ::_thesis: not p <= |.K65((seq1 . m),g).| then consider l being Nat such that A7: m = (n1 + k) + l by NAT_1:10; reconsider l = l as Element of NAT by ORDINAL1:def_12; m - k = ((n1 + l) + k) + (- k) by A7; then consider m1 being Element of NAT such that A8: m1 = m - k ; now__::_thesis:_n1_<=_m1 assume not n1 <= m1 ; ::_thesis: contradiction then m1 + k < n1 + k by XREAL_1:6; hence contradiction by A6, A8; ::_thesis: verum end; then A9: |.((seq . m1) - g1).| < p by A5; m1 + k = m by A8; hence |.((seq1 . m) - g).| < p by A3, A9, NAT_1:def_3; ::_thesis: verum end; theorem :: CFCONT_1:23 for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds lim seq1 = lim seq proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies lim seq1 = lim seq ) assume that A1: seq is convergent and A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: lim seq1 = lim seq consider k being Element of NAT such that A3: seq = seq1 ^\ k by A2; A4: 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_ |.((seq1_._m)_-_(lim_seq)).|_<_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 |.((seq1 . m) - (lim seq)).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds |.((seq . m) - (lim seq)).| < p by A1, COMSEQ_2:def_6; take n = n1 + k; ::_thesis: for m being Element of NAT st n <= m holds |.((seq1 . m) - (lim seq)).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p ) assume A6: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p then consider l being Nat such that A7: m = (n1 + k) + l by NAT_1:10; reconsider l = l as Element of NAT by ORDINAL1:def_12; m - k = ((n1 + l) + k) + (- k) by A7; then consider m1 being Element of NAT such that A8: m1 = m - k ; now__::_thesis:_n1_<=_m1 assume not n1 <= m1 ; ::_thesis: contradiction then m1 + k < n1 + k by XREAL_1:6; hence contradiction by A6, A8; ::_thesis: verum end; then A9: |.((seq . m1) - (lim seq)).| < p by A5; m1 + k = m by A8; hence |.((seq1 . m) - (lim seq)).| < p by A3, A9, NAT_1:def_3; ::_thesis: verum end; seq1 is convergent by A1, A2, Th22; hence lim seq1 = lim seq by A4, COMSEQ_2:def_6; ::_thesis: verum end; theorem Th24: :: CFCONT_1:24 for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds ex k being Element of NAT st seq ^\ k is non-zero proof let seq be Complex_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies ex k being Element of NAT st seq ^\ k is non-zero ) assume that A1: seq is convergent and A2: lim seq <> 0 ; ::_thesis: ex k being Element of NAT st seq ^\ k is non-zero consider n1 being Element of NAT such that A3: for m being Element of NAT st n1 <= m holds |.(lim seq).| / 2 < |.(seq . m).| by A1, A2, COMSEQ_2:33; take k = n1; ::_thesis: seq ^\ k is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_k)_._n_<>_0c let n be Element of NAT ; ::_thesis: (seq ^\ k) . n <> 0c 0 <= n by NAT_1:2; then 0 + k <= n + k by XREAL_1:7; then |.(lim seq).| / 2 < |.(seq . (n + k)).| by A3; then A4: |.(lim seq).| / 2 < |.((seq ^\ k) . n).| by NAT_1:def_3; 0 < |.(lim seq).| by A2, COMPLEX1:47; then 0 / 2 < |.(lim seq).| / 2 by XREAL_1:74; then 0 < |.((seq ^\ k) . n).| by A4, XXREAL_0:2; hence (seq ^\ k) . n <> 0c by COMPLEX1:47; ::_thesis: verum end; hence seq ^\ k is non-zero by COMSEQ_1:4; ::_thesis: verum end; theorem :: CFCONT_1:25 for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds ex seq1 being Complex_Sequence st ( seq1 is subsequence of seq & seq1 is non-zero ) proof let seq be Complex_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies ex seq1 being Complex_Sequence st ( seq1 is subsequence of seq & seq1 is non-zero ) ) assume ( seq is convergent & lim seq <> 0 ) ; ::_thesis: ex seq1 being Complex_Sequence st ( seq1 is subsequence of seq & seq1 is non-zero ) then consider k being Element of NAT such that A1: seq ^\ k is non-zero by Th24; take seq ^\ k ; ::_thesis: ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero ) thus ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero ) by A1; ::_thesis: verum end; theorem Th26: :: CFCONT_1:26 for seq being Complex_Sequence st seq is constant holds seq is convergent proof let seq be Complex_Sequence; ::_thesis: ( seq is constant implies seq is convergent ) assume seq is constant ; ::_thesis: seq is convergent then consider t being Element of COMPLEX such that A1: for n being Nat holds seq . n = t by VALUED_0:def_18; take g = t; :: 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 <= |.K65((seq . 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 <= |.K65((seq . 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 <= |.K65((seq . b2),g).| ) take n = 0 ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= |.K65((seq . b1),g).| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.K65((seq . m),g).| ) assume n <= m ; ::_thesis: not p <= |.K65((seq . m),g).| |.((seq . m) - g).| = |.(t - g).| by A1 .= 0 by COMPLEX1:44 ; hence |.((seq . m) - g).| < p by A2; ::_thesis: verum end; theorem Th27: :: CFCONT_1:27 for g being Element of COMPLEX for seq being Complex_Sequence st ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) holds lim seq = g proof let g be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence st ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) holds lim seq = g let seq be Complex_Sequence; ::_thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g ) A1: now__::_thesis:_(_seq_is_constant_&_g_in_rng_seq_&_(_(_seq_is_constant_&_g_in_rng_seq_)_or_(_seq_is_constant_&_ex_n_being_Element_of_NAT_st_seq_._n_=_g_)_)_implies_lim_seq_=_g_) assume that A2: seq is constant and A3: g in rng seq ; ::_thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g ) consider g1 being Element of COMPLEX such that A4: rng seq = {g1} by A2, FUNCT_2:111; consider g2 being Element of COMPLEX such that A5: for n being Nat holds seq . n = g2 by A2, VALUED_0:def_18; A6: g = g1 by A3, A4, TARSKI:def_1; A7: 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_ |.((seq_._m)_-_g).|_<_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 |.((seq . m) - g).| < p ) assume A8: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g).| < p take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds |.((seq . m) - g).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq . m) - g).| < p ) assume n <= m ; ::_thesis: |.((seq . m) - g).| < p m in NAT ; then m in dom seq by COMSEQ_1:2; then seq . m in rng seq by FUNCT_1:def_3; then g2 in rng seq by A5; then g2 = g by A4, A6, TARSKI:def_1; then seq . m = g by A5; hence |.((seq . m) - g).| < p by A8, COMPLEX1:44; ::_thesis: verum end; seq is convergent by A2, Th26; hence ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g ) by A7, COMSEQ_2:def_6; ::_thesis: verum end; A9: now__::_thesis:_(_seq_is_constant_&_ex_n_being_Element_of_NAT_st_seq_._n_=_g_&_(_(_seq_is_constant_&_g_in_rng_seq_)_or_(_seq_is_constant_&_ex_n_being_Element_of_NAT_st_seq_._n_=_g_)_)_implies_lim_seq_=_g_) assume that seq is constant and A10: ex n being Element of NAT st seq . n = g ; ::_thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g ) consider n being Element of NAT such that A11: seq . n = g by A10; n in NAT ; then n in dom seq by COMSEQ_1:2; hence ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g ) by A1, A11, FUNCT_1:def_3; ::_thesis: verum end; assume ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) ; ::_thesis: lim seq = g hence lim seq = g by A1, A9; ::_thesis: verum end; theorem :: CFCONT_1:28 for seq being Complex_Sequence st seq is constant holds for n being Element of NAT holds lim seq = seq . n by Th27; theorem :: CFCONT_1:29 for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds for seq1 being Complex_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds lim (seq1 ") = (lim seq) " proof let seq be Complex_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies for seq1 being Complex_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds lim (seq1 ") = (lim seq) " ) assume that A1: seq is convergent and A2: lim seq <> 0 ; ::_thesis: for seq1 being Complex_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds lim (seq1 ") = (lim seq) " let seq1 be Complex_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq1 is non-zero implies lim (seq1 ") = (lim seq) " ) assume that A3: seq1 is subsequence of seq and A4: seq1 is non-zero ; ::_thesis: lim (seq1 ") = (lim seq) " lim seq1 = lim seq by A1, A3, Th18; hence lim (seq1 ") = (lim seq) " by A1, A2, A3, A4, Th17, COMSEQ_2:35; ::_thesis: verum end; theorem :: CFCONT_1:30 for seq, seq1 being Complex_Sequence st seq is constant & seq1 is convergent holds ( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) ) proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is constant & seq1 is convergent implies ( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) ) ) assume that A1: seq is constant and A2: seq1 is convergent ; ::_thesis: ( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) ) A3: seq is convergent by A1, Th26; hence lim (seq + seq1) = (lim seq) + (lim seq1) by A2, COMSEQ_2:14 .= (seq . 0) + (lim seq1) by A1, Th27 ; ::_thesis: ( lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) ) thus lim (seq - seq1) = (lim seq) - (lim seq1) by A2, A3, COMSEQ_2:26 .= (seq . 0) - (lim seq1) by A1, Th27 ; ::_thesis: ( lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) ) thus lim (seq1 - seq) = (lim seq1) - (lim seq) by A2, A3, COMSEQ_2:26 .= (lim seq1) - (seq . 0) by A1, Th27 ; ::_thesis: lim (seq (#) seq1) = (seq . 0) * (lim seq1) thus lim (seq (#) seq1) = (lim seq) * (lim seq1) by A2, A3, COMSEQ_2:30 .= (seq . 0) * (lim seq1) by A1, Th27 ; ::_thesis: verum end; scheme :: CFCONT_1:sch 1 CompSeqChoice{ P1[ set , set ] } : ex s1 being Complex_Sequence st for n being Element of NAT holds P1[n,s1 . n] provided A1: for n being Element of NAT ex g being Element of COMPLEX st P1[n,g] proof A2: for t being Element of NAT ex ff being Element of COMPLEX st P1[t,ff] by A1; consider f being Function of NAT,COMPLEX such that A3: for t being Element of NAT holds P1[t,f . t] from FUNCT_2:sch_3(A2); reconsider s = f as Complex_Sequence ; take s ; ::_thesis: for n being Element of NAT holds P1[n,s . n] let n be Element of NAT ; ::_thesis: P1[n,s . n] thus P1[n,s . n] by A3; ::_thesis: verum end; begin theorem :: CFCONT_1:31 for x0 being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_in x0 iff ( x0 in dom f & ( 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) ) ) ) ) proof let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_in x0 iff ( x0 in dom f & ( 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) ) ) ) ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( 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) ) ) ) ) thus ( f is_continuous_in x0 implies ( x0 in dom f & ( 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) ) ) ) ) by Def1; ::_thesis: ( x0 in dom f & ( 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) ) ) implies f is_continuous_in x0 ) assume that A1: x0 in dom f and A2: 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) ) ; ::_thesis: f is_continuous_in x0 thus x0 in dom f by A1; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) let s2 be Complex_Sequence; ::_thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ) assume that A3: rng s2 c= dom f and A4: ( s2 is convergent & lim s2 = x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) now__::_thesis:_(_f_/*_s2_is_convergent_&_f_/._x0_=_lim_(f_/*_s2)_) percases ( ex n being Element of NAT st for m being Element of NAT st n <= m holds s2 . m = x0 or for n being Element of NAT ex m being Element of NAT st ( n <= m & s2 . m <> x0 ) ) ; suppose ex n being Element of NAT st for m being Element of NAT st n <= m holds s2 . m = x0 ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) then consider N being Element of NAT such that A5: for m being Element of NAT st N <= m holds s2 . m = x0 ; A6: for n being Element of NAT holds (s2 ^\ N) . n = x0 proof let n be Element of NAT ; ::_thesis: (s2 ^\ N) . n = x0 s2 . (n + N) = x0 by A5, NAT_1:12; hence (s2 ^\ N) . n = x0 by NAT_1:def_3; ::_thesis: verum end; A7: f /* (s2 ^\ N) = (f /* s2) ^\ N by A3, VALUED_0:27; A8: rng (s2 ^\ N) c= rng s2 by VALUED_0:21; A9: now__::_thesis:_for_p_being_Real_st_p_>_0_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.(((f_/*_(s2_^\_N))_._m)_-_(f_/._x0)).|_<_p let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p ) assume A10: p > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p ) assume n <= m ; ::_thesis: |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| = |.((f /. ((s2 ^\ N) . m)) - (f /. x0)).| by A3, A8, FUNCT_2:109, XBOOLE_1:1 .= |.((f /. x0) - (f /. x0)).| by A6 .= 0 by COMPLEX1:44 ; hence |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p by A10; ::_thesis: verum end; then A11: f /* (s2 ^\ N) is convergent by COMSEQ_2:def_5; then f /. x0 = lim ((f /* s2) ^\ N) by A9, A7, COMSEQ_2:def_6; hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A11, A7, Th18, Th22; ::_thesis: verum end; supposeA12: for n being Element of NAT ex m being Element of NAT st ( n <= m & s2 . m <> x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) defpred S1[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds ( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds m <= k ) ); defpred S2[ set , set , set ] means S1[$2,$3]; defpred S3[ set ] means s2 . $1 <> x0; ex m1 being Element of NAT st ( 0 <= m1 & s2 . m1 <> x0 ) by A12; then A13: ex m being Nat st S3[m] ; consider M being Nat such that A14: ( S3[M] & ( for n being Nat st S3[n] holds M <= n ) ) from NAT_1:sch_5(A13); reconsider M9 = M as Element of NAT by ORDINAL1:def_12; A15: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_ (_n_<_m_&_s2_._m_<>_x0_) let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n < m & s2 . m <> x0 ) consider m being Element of NAT such that A16: ( n + 1 <= m & s2 . m <> x0 ) by A12; take m = m; ::_thesis: ( n < m & s2 . m <> x0 ) thus ( n < m & s2 . m <> x0 ) by A16, NAT_1:13; ::_thesis: verum end; A17: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y] proof let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S2[n,x,y] defpred S4[ Nat] means ( x < $1 & s2 . $1 <> x0 ); ex m being Element of NAT st S4[m] by A15; then A18: ex m being Nat st S4[m] ; consider l being Nat such that A19: ( S4[l] & ( for k being Nat st S4[k] holds l <= k ) ) from NAT_1:sch_5(A18); take l ; ::_thesis: ( l is Element of REAL & l is Element of NAT & S2[n,x,l] ) l in NAT by ORDINAL1:def_12; hence ( l is Element of REAL & l is Element of NAT & S2[n,x,l] ) by A19; ::_thesis: verum end; consider F being Function of NAT,NAT such that A20: ( F . 0 = M9 & ( for n being Element of NAT holds S2[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A17); A21: for n being Element of NAT holds F . n is real ; A22: rng F c= NAT ; A23: dom F = NAT by FUNCT_2:def_1; then reconsider F = F as Real_Sequence by A21, SEQ_1:2; A24: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_Element_of_NAT let n be Element of NAT ; ::_thesis: F . n is Element of NAT F . n in rng F by A23, FUNCT_1:def_3; hence F . n is Element of NAT by A22; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_<_F_._(n_+_1) let n be Element of NAT ; ::_thesis: F . n < F . (n + 1) ( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A24; hence F . n < F . (n + 1) by A20; ::_thesis: verum end; then reconsider F = F as V37() sequence of NAT by SEQM_3:def_6; A25: s2 * F is subsequence of s2 by VALUED_0:def_17; then A26: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A4, Th17, Th18; A27: for n being Element of NAT st s2 . n <> x0 holds ex m being Element of NAT st F . m = n proof defpred S4[ set ] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) ); assume ex n being Element of NAT st S4[n] ; ::_thesis: contradiction then A28: ex n being Nat st S4[n] ; consider M1 being Nat such that A29: ( S4[M1] & ( for n being Nat st S4[n] holds M1 <= n ) ) from NAT_1:sch_5(A28); defpred S5[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 ); A30: ex n being Nat st S5[n] proof take M ; ::_thesis: S5[M] ( M <= M1 & M <> M1 ) by A14, A20, A29; hence M < M1 by XXREAL_0:1; ::_thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M ) thus s2 . M <> x0 by A14; ::_thesis: ex m being Element of NAT st F . m = M take 0 ; ::_thesis: F . 0 = M thus F . 0 = M by A20; ::_thesis: verum end; A31: for n being Nat st S5[n] holds n <= M1 ; consider MX being Nat such that A32: ( S5[MX] & ( for n being Nat st S5[n] holds n <= MX ) ) from NAT_1:sch_6(A31, A30); A33: for k being Element of NAT st MX < k & k < M1 holds s2 . k = x0 proof given k being Element of NAT such that A34: MX < k and A35: ( k < M1 & s2 . k <> x0 ) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ; suppose ex m being Element of NAT st F . m = k ; ::_thesis: contradiction hence contradiction by A32, A34, A35; ::_thesis: verum end; suppose for m being Element of NAT holds F . m <> k ; ::_thesis: contradiction hence contradiction by A29, A35; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; consider m being Element of NAT such that A36: F . m = MX by A32; A37: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A20, A36; M1 in NAT by ORDINAL1:def_12; then A38: F . (m + 1) <= M1 by A20, A29, A32, A36; now__::_thesis:_not_F_._(m_+_1)_<>_M1 assume F . (m + 1) <> M1 ; ::_thesis: contradiction then F . (m + 1) < M1 by A38, XXREAL_0:1; hence contradiction by A33, A37; ::_thesis: verum end; hence contradiction by A29; ::_thesis: verum end; defpred S4[ Element of NAT ] means (s2 * F) . $1 <> x0; A39: for k being Element of NAT st S4[k] holds S4[k + 1] proof let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] ) assume (s2 * F) . k <> x0 ; ::_thesis: S4[k + 1] S1[F . k,F . (k + 1)] by A20; then s2 . (F . (k + 1)) <> x0 ; hence S4[k + 1] by FUNCT_2:15; ::_thesis: verum end; A40: S4[ 0 ] by A14, A20, FUNCT_2:15; A41: for n being Element of NAT holds S4[n] from NAT_1:sch_1(A40, A39); A42: rng (s2 * F) c= rng s2 by A25, VALUED_0:21; then rng (s2 * F) c= dom f by A3, XBOOLE_1:1; then A43: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A2, A41, A26; A44: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.(((f_/*_s2)_._m)_-_(f_/._x0)).|_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((f /* s2) . m) - (f /. x0)).| < p ) assume A45: 0 < p ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((f /* s2) . m) - (f /. x0)).| < p then consider n being Element of NAT such that A46: for m being Element of NAT st n <= m holds |.(((f /* (s2 * F)) . m) - (f /. x0)).| < p by A43, COMSEQ_2:def_6; take k = F . n; ::_thesis: for m being Element of NAT st k <= m holds |.(((f /* s2) . m) - (f /. x0)).| < p let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((f /* s2) . m) - (f /. x0)).| < p ) assume A47: k <= m ; ::_thesis: |.(((f /* s2) . m) - (f /. x0)).| < p now__::_thesis:_|.(((f_/*_s2)_._m)_-_(f_/._x0)).|_<_p percases ( s2 . m = x0 or s2 . m <> x0 ) ; suppose s2 . m = x0 ; ::_thesis: |.(((f /* s2) . m) - (f /. x0)).| < p then |.(((f /* s2) . m) - (f /. x0)).| = |.((f /. x0) - (f /. x0)).| by A3, FUNCT_2:109 .= 0 by COMPLEX1:44 ; hence |.(((f /* s2) . m) - (f /. x0)).| < p by A45; ::_thesis: verum end; suppose s2 . m <> x0 ; ::_thesis: |.(((f /* s2) . m) - (f /. x0)).| < p then consider l being Element of NAT such that A48: m = F . l by A27; n <= l by A47, A48, SEQM_3:1; then |.(((f /* (s2 * F)) . l) - (f /. x0)).| < p by A46; then |.((f /. ((s2 * F) . l)) - (f /. x0)).| < p by A3, A42, FUNCT_2:109, XBOOLE_1:1; then |.((f /. (s2 . m)) - (f /. x0)).| < p by A48, FUNCT_2:15; hence |.(((f /* s2) . m) - (f /. x0)).| < p by A3, FUNCT_2:109; ::_thesis: verum end; end; end; hence |.(((f /* s2) . m) - (f /. x0)).| < p ; ::_thesis: verum end; hence f /* s2 is convergent by COMSEQ_2:def_5; ::_thesis: f /. x0 = lim (f /* s2) hence f /. x0 = lim (f /* s2) by A44, COMSEQ_2:def_6; ::_thesis: verum end; end; end; hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ; ::_thesis: verum end; theorem Th32: :: CFCONT_1:32 for x0 being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) proof let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_in x0 ) proof assume A1: f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) hence x0 in dom f by Def1; ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) given r being Real such that A2: 0 < r and A3: for s being Real holds ( not 0 < s or ex x1 being Element of COMPLEX st ( x1 in dom f & |.(x1 - x0).| < s & not |.((f /. x1) - (f /. x0)).| < r ) ) ; ::_thesis: contradiction defpred S1[ Element of NAT , Element of COMPLEX ] means ( $2 in dom f & |.($2 - x0).| < 1 / ($1 + 1) & not |.((f /. $2) - (f /. x0)).| < r ); A4: for n being Element of NAT ex g being Element of COMPLEX st S1[n,g] proof let n be Element of NAT ; ::_thesis: ex g being Element of COMPLEX st S1[n,g] 0 < n + 1 by NAT_1:3; then 0 < (n + 1) " by XREAL_1:122; then 0 < 1 / (n + 1) by XCMPLX_1:215; then consider g being Element of COMPLEX such that A5: ( g in dom f & |.(g - x0).| < 1 / (n + 1) & not |.((f /. g) - (f /. x0)).| < r ) by A3; take g ; ::_thesis: S1[n,g] thus S1[n,g] by A5; ::_thesis: verum end; consider s1 being Complex_Sequence such that A6: for n being Element of NAT holds S1[n,s1 . n] from CFCONT_1:sch_1(A4); A7: rng s1 c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s1 or x in dom f ) assume x in rng s1 ; ::_thesis: x in dom f then ex n being Element of NAT st x = s1 . n by FUNCT_2:113; hence x in dom f by A6; ::_thesis: verum end; A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_|.(((f_/*_s1)_._n)_-_(f_/._x0)).|_<_r let n be Element of NAT ; ::_thesis: not |.(((f /* s1) . n) - (f /. x0)).| < r not |.((f /. (s1 . n)) - (f /. x0)).| < r by A6; hence not |.(((f /* s1) . n) - (f /. x0)).| < r by A7, FUNCT_2:109; ::_thesis: verum end; A9: now__::_thesis:_for_s_being_Real_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.((s1_._m)_-_x0).|_<_s let s be Real; ::_thesis: ( 0 < s implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.((s1 . m) - x0).| < s ) consider n being Element of NAT such that A10: s " < n by SEQ_4:3; assume 0 < s ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.((s1 . m) - x0).| < s then A11: 0 < s " by XREAL_1:122; (s ") + 0 < n + 1 by A10, XREAL_1:8; then 1 / (n + 1) < 1 / (s ") by A11, XREAL_1:76; then A12: 1 / (n + 1) < s by XCMPLX_1:216; take k = n; ::_thesis: for m being Element of NAT st k <= m holds |.((s1 . m) - x0).| < s let m be Element of NAT ; ::_thesis: ( k <= m implies |.((s1 . m) - x0).| < s ) assume k <= m ; ::_thesis: |.((s1 . m) - x0).| < s then k + 1 <= m + 1 by XREAL_1:6; then 1 / (m + 1) <= 1 / (k + 1) by NAT_1:3, XREAL_1:118; then 1 / (m + 1) < s by A12, XXREAL_0:2; hence |.((s1 . m) - x0).| < s by A6, XXREAL_0:2; ::_thesis: verum end; then A13: s1 is convergent by COMSEQ_2:def_5; then lim s1 = x0 by A9, COMSEQ_2:def_6; then ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A7, A13, Def1; then consider n being Element of NAT such that A14: for m being Element of NAT st n <= m holds |.(((f /* s1) . m) - (f /. x0)).| < r by A2, COMSEQ_2:def_6; |.(((f /* s1) . n) - (f /. x0)).| < r by A14; hence contradiction by A8; ::_thesis: verum end; assume that A15: x0 in dom f and A16: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ; ::_thesis: f is_continuous_in x0 now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_=_x0_holds_ (_f_/*_s1_is_convergent_&_f_/._x0_=_lim_(f_/*_s1)_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) assume that A17: rng s1 c= dom f and A18: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) A19: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.(((f_/*_s1)_._m)_-_(f_/._x0)).|_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((f /* s1) . m) - (f /. x0)).| < p ) assume 0 < p ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((f /* s1) . m) - (f /. x0)).| < p then consider s being Real such that A20: 0 < s and A21: for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < p by A16; consider n being Element of NAT such that A22: for m being Element of NAT st n <= m holds |.((s1 . m) - x0).| < s by A18, A20, COMSEQ_2:def_6; take k = n; ::_thesis: for m being Element of NAT st k <= m holds |.(((f /* s1) . m) - (f /. x0)).| < p let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((f /* s1) . m) - (f /. x0)).| < p ) assume k <= m ; ::_thesis: |.(((f /* s1) . m) - (f /. x0)).| < p then ( s1 . m in rng s1 & |.((s1 . m) - x0).| < s ) by A22, VALUED_0:28; then |.((f /. (s1 . m)) - (f /. x0)).| < p by A17, A21; hence |.(((f /* s1) . m) - (f /. x0)).| < p by A17, FUNCT_2:109; ::_thesis: verum end; then f /* s1 is convergent by COMSEQ_2:def_5; hence ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A19, COMSEQ_2:def_6; ::_thesis: verum end; hence f is_continuous_in x0 by A15, Def1; ::_thesis: verum end; theorem Th33: :: CFCONT_1:33 for x0 being Element of COMPLEX for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) proof let x0 be Element of COMPLEX ; ::_thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_in x0 & f2 is_continuous_in x0 implies ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) ) assume that A1: f1 is_continuous_in x0 and A2: f2 is_continuous_in x0 ; ::_thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) A3: ( x0 in dom f1 & x0 in dom f2 ) by A1, A2, Def1; now__::_thesis:_(_x0_in_dom_(f1_+_f2)_&_(_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_(f1_+_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_ (_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_/._x0_=_lim_((f1_+_f2)_/*_s1)_)_)_) x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4; hence A4: x0 in dom (f1 + f2) by VALUED_1:def_1; ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 holds ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) ) assume that A5: rng s1 c= dom (f1 + f2) and A6: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) A7: rng s1 c= (dom f1) /\ (dom f2) by A5, VALUED_1:def_1; dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1; then dom (f1 + f2) c= dom f2 by XBOOLE_1:17; then A8: rng s1 c= dom f2 by A5, XBOOLE_1:1; then A9: f2 /* s1 is convergent by A2, A6, Def1; dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1; then dom (f1 + f2) c= dom f1 by XBOOLE_1:17; then A10: rng s1 c= dom f1 by A5, XBOOLE_1:1; then A11: f1 /* s1 is convergent by A1, A6, Def1; then (f1 /* s1) + (f2 /* s1) is convergent by A9; hence (f1 + f2) /* s1 is convergent by A7, Th7; ::_thesis: (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) A12: f1 /. x0 = lim (f1 /* s1) by A1, A6, A10, Def1; A13: f2 /. x0 = lim (f2 /* s1) by A2, A6, A8, Def1; thus (f1 + f2) /. x0 = (f1 /. x0) + (f2 /. x0) by A4, CFUNCT_1:1 .= lim ((f1 /* s1) + (f2 /* s1)) by A11, A12, A9, A13, COMSEQ_2:14 .= lim ((f1 + f2) /* s1) by A7, Th7 ; ::_thesis: verum end; hence f1 + f2 is_continuous_in x0 by Def1; ::_thesis: ( f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) now__::_thesis:_(_x0_in_dom_(f1_-_f2)_&_(_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_(f1_-_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_ (_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_/._x0_=_lim_((f1_-_f2)_/*_s1)_)_)_) x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4; hence A14: x0 in dom (f1 - f2) by CFUNCT_1:2; ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 holds ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) ) assume that A15: rng s1 c= dom (f1 - f2) and A16: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) A17: rng s1 c= (dom f1) /\ (dom f2) by A15, CFUNCT_1:2; dom (f1 - f2) = (dom f1) /\ (dom f2) by CFUNCT_1:2; then dom (f1 - f2) c= dom f2 by XBOOLE_1:17; then A18: rng s1 c= dom f2 by A15, XBOOLE_1:1; then A19: f2 /* s1 is convergent by A2, A16, Def1; dom (f1 - f2) = (dom f1) /\ (dom f2) by CFUNCT_1:2; then dom (f1 - f2) c= dom f1 by XBOOLE_1:17; then A20: rng s1 c= dom f1 by A15, XBOOLE_1:1; then A21: f1 /* s1 is convergent by A1, A16, Def1; then (f1 /* s1) - (f2 /* s1) is convergent by A19; hence (f1 - f2) /* s1 is convergent by A17, Th7; ::_thesis: (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) A22: f1 /. x0 = lim (f1 /* s1) by A1, A16, A20, Def1; A23: f2 /. x0 = lim (f2 /* s1) by A2, A16, A18, Def1; thus (f1 - f2) /. x0 = (f1 /. x0) - (f2 /. x0) by A14, CFUNCT_1:2 .= lim ((f1 /* s1) - (f2 /* s1)) by A21, A22, A19, A23, COMSEQ_2:26 .= lim ((f1 - f2) /* s1) by A17, Th7 ; ::_thesis: verum end; hence f1 - f2 is_continuous_in x0 by Def1; ::_thesis: f1 (#) f2 is_continuous_in x0 x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4; hence A24: x0 in dom (f1 (#) f2) by VALUED_1:def_4; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 holds ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) ) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) ) ) assume that A25: rng s1 c= dom (f1 (#) f2) and A26: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) ) dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4; then dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17; then A27: rng s1 c= dom f2 by A25, XBOOLE_1:1; then A28: f2 /* s1 is convergent by A2, A26, Def1; A29: rng s1 c= (dom f1) /\ (dom f2) by A25, VALUED_1:def_4; dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4; then dom (f1 (#) f2) c= dom f1 by XBOOLE_1:17; then A30: rng s1 c= dom f1 by A25, XBOOLE_1:1; then A31: f1 /* s1 is convergent by A1, A26, Def1; then (f1 /* s1) (#) (f2 /* s1) is convergent by A28; hence (f1 (#) f2) /* s1 is convergent by A29, Th7; ::_thesis: (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) A32: f1 /. x0 = lim (f1 /* s1) by A1, A26, A30, Def1; A33: f2 /. x0 = lim (f2 /* s1) by A2, A26, A27, Def1; thus (f1 (#) f2) /. x0 = (f1 /. x0) * (f2 /. x0) by A24, CFUNCT_1:3 .= lim ((f1 /* s1) (#) (f2 /* s1)) by A31, A32, A28, A33, COMSEQ_2:30 .= lim ((f1 (#) f2) /* s1) by A29, Th7 ; ::_thesis: verum end; theorem Th34: :: CFCONT_1:34 for x0, g being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds g (#) f is_continuous_in x0 proof let x0, g be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds g (#) f is_continuous_in x0 let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 implies g (#) f is_continuous_in x0 ) assume A1: f is_continuous_in x0 ; ::_thesis: g (#) f is_continuous_in x0 then x0 in dom f by Def1; hence A2: x0 in dom (g (#) f) by VALUED_1:def_5; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (g (#) f) & s1 is convergent & lim s1 = x0 holds ( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) ) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (g (#) f) & s1 is convergent & lim s1 = x0 implies ( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) ) ) assume that A3: rng s1 c= dom (g (#) f) and A4: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) ) A5: rng s1 c= dom f by A3, VALUED_1:def_5; then A6: f /. x0 = lim (f /* s1) by A1, A4, Def1; A7: f /* s1 is convergent by A1, A4, A5, Def1; then g (#) (f /* s1) is convergent ; hence (g (#) f) /* s1 is convergent by A5, Th8; ::_thesis: (g (#) f) /. x0 = lim ((g (#) f) /* s1) thus (g (#) f) /. x0 = g * (f /. x0) by A2, CFUNCT_1:4 .= lim (g (#) (f /* s1)) by A7, A6, COMSEQ_2:18 .= lim ((g (#) f) /* s1) by A5, Th8 ; ::_thesis: verum end; theorem :: CFCONT_1:35 for x0 being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds - f is_continuous_in x0 proof let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds - f is_continuous_in x0 let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 implies - f is_continuous_in x0 ) A1: - f = (- 1r) (#) f by CFUNCT_1:31; assume f is_continuous_in x0 ; ::_thesis: - f is_continuous_in x0 hence - f is_continuous_in x0 by A1, Th34; ::_thesis: verum end; theorem Th36: :: CFCONT_1:36 for x0 being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 & f /. x0 <> 0 holds f ^ is_continuous_in x0 proof let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 & f /. x0 <> 0 holds f ^ is_continuous_in x0 let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 & f /. x0 <> 0 implies f ^ is_continuous_in x0 ) assume that A1: f is_continuous_in x0 and A2: f /. x0 <> 0 ; ::_thesis: f ^ is_continuous_in x0 not f /. x0 in {0c} by A2, TARSKI:def_1; then A3: not x0 in f " {0c} by PARTFUN2:26; x0 in dom f by A1, Def1; then x0 in (dom f) \ (f " {0c}) by A3, XBOOLE_0:def_5; hence A4: x0 in dom (f ^) by CFUNCT_1:def_2; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f ^) & s1 is convergent & lim s1 = x0 holds ( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) ) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f ^) & s1 is convergent & lim s1 = x0 implies ( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) ) ) assume that A5: rng s1 c= dom (f ^) and A6: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) ) ( (dom f) \ (f " {0c}) c= dom f & rng s1 c= (dom f) \ (f " {0c}) ) by A5, CFUNCT_1:def_2, XBOOLE_1:36; then rng s1 c= dom f by XBOOLE_1:1; then A7: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A6, Def1; f /* s1 is non-zero by A5, Th10; then (f /* s1) " is convergent by A2, A7, COMSEQ_2:34; hence (f ^) /* s1 is convergent by A5, Th11; ::_thesis: (f ^) /. x0 = lim ((f ^) /* s1) thus (f ^) /. x0 = (f /. x0) " by A4, CFUNCT_1:def_2 .= lim ((f /* s1) ") by A2, A5, A7, Th10, COMSEQ_2:35 .= lim ((f ^) /* s1) by A5, Th11 ; ::_thesis: verum end; theorem :: CFCONT_1:37 for x0 being Element of COMPLEX for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f1 /. x0 <> 0 & f2 is_continuous_in x0 holds f2 / f1 is_continuous_in x0 proof let x0 be Element of COMPLEX ; ::_thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f1 /. x0 <> 0 & f2 is_continuous_in x0 holds f2 / f1 is_continuous_in x0 let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_in x0 & f1 /. x0 <> 0 & f2 is_continuous_in x0 implies f2 / f1 is_continuous_in x0 ) assume that A1: ( f1 is_continuous_in x0 & f1 /. x0 <> 0 ) and A2: f2 is_continuous_in x0 ; ::_thesis: f2 / f1 is_continuous_in x0 f1 ^ is_continuous_in x0 by A1, Th36; then f2 (#) (f1 ^) is_continuous_in x0 by A2, Th33; hence f2 / f1 is_continuous_in x0 by CFUNCT_1:39; ::_thesis: verum end; definition let f be PartFunc of COMPLEX,COMPLEX; let X be set ; predf is_continuous_on X means :Def2: :: CFCONT_1:def 2 ( X c= dom f & ( for x0 being Element of COMPLEX st x0 in X holds f | X is_continuous_in x0 ) ); end; :: deftheorem Def2 defines is_continuous_on CFCONT_1:def_2_:_ for f being PartFunc of COMPLEX,COMPLEX for X being set holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Element of COMPLEX st x0 in X holds f | X is_continuous_in x0 ) ) ); theorem Th38: :: CFCONT_1:38 for X being set for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_on X iff ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_on X iff ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X iff ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) thus ( f is_continuous_on X implies ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) ::_thesis: ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) implies f is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) then A2: X c= dom f by Def2; now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_ (_f_/*_s1_is_convergent_&_f_/._(lim_s1)_=_lim_(f_/*_s1)_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) assume that A3: rng s1 c= X and A4: s1 is convergent and A5: lim s1 in X ; ::_thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) A6: f | X is_continuous_in lim s1 by A1, A5, Def2; A7: dom (f | X) = (dom f) /\ X by RELAT_1:61 .= X by A2, XBOOLE_1:28 ; now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n A8: s1 . n in rng s1 by VALUED_0:28; thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A3, A7, FUNCT_2:109 .= f /. (s1 . n) by A3, A7, A8, PARTFUN2:15 .= (f /* s1) . n by A2, A3, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum end; then A9: (f | X) /* s1 = f /* s1 by FUNCT_2:63; f /. (lim s1) = (f | X) /. (lim s1) by A5, A7, PARTFUN2:15 .= lim (f /* s1) by A3, A4, A7, A6, A9, Def1 ; hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A7, A6, A9, Def1; ::_thesis: verum end; hence ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) by A1, Def2; ::_thesis: verum end; assume that A10: X c= dom f and A11: for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ; ::_thesis: f is_continuous_on X now__::_thesis:_for_x1_being_Element_of_COMPLEX_st_x1_in_X_holds_ f_|_X_is_continuous_in_x1 A12: dom (f | X) = (dom f) /\ X by RELAT_1:61 .= X by A10, XBOOLE_1:28 ; let x1 be Element of COMPLEX ; ::_thesis: ( x1 in X implies f | X is_continuous_in x1 ) assume A13: x1 in X ; ::_thesis: f | X is_continuous_in x1 now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_(f_|_X)_&_s1_is_convergent_&_lim_s1_=_x1_holds_ (_(f_|_X)_/*_s1_is_convergent_&_(f_|_X)_/._x1_=_lim_((f_|_X)_/*_s1)_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 implies ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) ) assume that A14: rng s1 c= dom (f | X) and A15: s1 is convergent and A16: lim s1 = x1 ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n A17: s1 . n in rng s1 by VALUED_0:28; thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A14, FUNCT_2:109 .= f /. (s1 . n) by A14, A17, PARTFUN2:15 .= (f /* s1) . n by A10, A12, A14, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum end; then A18: (f | X) /* s1 = f /* s1 by FUNCT_2:63; (f | X) /. (lim s1) = f /. (lim s1) by A13, A12, A16, PARTFUN2:15 .= lim ((f | X) /* s1) by A11, A13, A12, A14, A15, A16, A18 ; hence ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) by A11, A13, A12, A14, A15, A16, A18; ::_thesis: verum end; hence f | X is_continuous_in x1 by A13, A12, Def1; ::_thesis: verum end; hence f is_continuous_on X by A10, Def2; ::_thesis: verum end; theorem Th39: :: CFCONT_1:39 for X being set for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) thus ( f is_continuous_on X implies ( X c= dom f & ( for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) ::_thesis: ( X c= dom f & ( for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: ( X c= dom f & ( for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) hence X c= dom f by Def2; ::_thesis: for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) A2: X c= dom f by A1, Def2; let x0 be Element of COMPLEX ; ::_thesis: for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) assume that A3: x0 in X and A4: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) f | X is_continuous_in x0 by A1, A3, Def2; then consider s being Real such that A5: 0 < s and A6: for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th32; take s ; ::_thesis: ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) thus 0 < s by A5; ::_thesis: for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r let x1 be Element of COMPLEX ; ::_thesis: ( x1 in X & |.(x1 - x0).| < s implies |.((f /. x1) - (f /. x0)).| < r ) assume that A7: x1 in X and A8: |.(x1 - x0).| < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r A9: dom (f | X) = (dom f) /\ X by RELAT_1:61 .= X by A2, XBOOLE_1:28 ; then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2:15 .= |.(((f | X) /. x1) - ((f | X) /. x0)).| by A3, A9, PARTFUN2:15 ; hence |.((f /. x1) - (f /. x0)).| < r by A6, A9, A7, A8; ::_thesis: verum end; assume that A10: X c= dom f and A11: for x0 being Element of COMPLEX for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ; ::_thesis: f is_continuous_on X A12: dom (f | X) = (dom f) /\ X by RELAT_1:61 .= X by A10, XBOOLE_1:28 ; now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_X_holds_ f_|_X_is_continuous_in_x0 let x0 be Element of COMPLEX ; ::_thesis: ( x0 in X implies f | X is_continuous_in x0 ) assume A13: x0 in X ; ::_thesis: f | X is_continuous_in x0 for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) then consider s being Real such that A14: 0 < s and A15: for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r by A11, A13; take s ; ::_thesis: ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) thus 0 < s by A14; ::_thesis: for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r let x1 be Element of COMPLEX ; ::_thesis: ( x1 in dom (f | X) & |.(x1 - x0).| < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) assume that A16: x1 in dom (f | X) and A17: |.(x1 - x0).| < s ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x0)).| < r |.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, A13, PARTFUN2:15 .= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2:15 ; hence |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A12, A15, A16, A17; ::_thesis: verum end; hence f | X is_continuous_in x0 by A12, A13, Th32; ::_thesis: verum end; hence f is_continuous_on X by A10, Def2; ::_thesis: verum end; theorem Th40: :: CFCONT_1:40 for X being set for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_on X iff f | X is_continuous_on X ) proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX holds ( f is_continuous_on X iff f | X is_continuous_on X ) let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X iff f | X is_continuous_on X ) thus ( f is_continuous_on X implies f | X is_continuous_on X ) ::_thesis: ( f | X is_continuous_on X implies f is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: f | X is_continuous_on X then X c= dom f by Def2; then X c= (dom f) /\ X by XBOOLE_1:28; hence X c= dom (f | X) by RELAT_1:61; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X holds (f | X) | X is_continuous_in x0 let g be Element of COMPLEX ; ::_thesis: ( g in X implies (f | X) | X is_continuous_in g ) assume g in X ; ::_thesis: (f | X) | X is_continuous_in g then f | X is_continuous_in g by A1, Def2; hence (f | X) | X is_continuous_in g by RELAT_1:72; ::_thesis: verum end; assume A2: f | X is_continuous_on X ; ::_thesis: f is_continuous_on X then X c= dom (f | X) by Def2; then ( (dom f) /\ X c= dom f & X c= (dom f) /\ X ) by RELAT_1:61, XBOOLE_1:17; hence X c= dom f by XBOOLE_1:1; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X holds f | X is_continuous_in x0 let g be Element of COMPLEX ; ::_thesis: ( g in X implies f | X is_continuous_in g ) assume g in X ; ::_thesis: f | X is_continuous_in g then (f | X) | X is_continuous_in g by A2, Def2; hence f | X is_continuous_in g by RELAT_1:72; ::_thesis: verum end; theorem Th41: :: CFCONT_1:41 for X, X1 being set for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & X1 c= X holds f is_continuous_on X1 proof let X, X1 be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & X1 c= X holds f is_continuous_on X1 let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X & X1 c= X implies f is_continuous_on X1 ) assume that A1: f is_continuous_on X and A2: X1 c= X ; ::_thesis: f is_continuous_on X1 X c= dom f by A1, Def2; hence A3: X1 c= dom f by A2, XBOOLE_1:1; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X1 holds f | X1 is_continuous_in x0 let g be Element of COMPLEX ; ::_thesis: ( g in X1 implies f | X1 is_continuous_in g ) assume A4: g in X1 ; ::_thesis: f | X1 is_continuous_in g then A5: f | X is_continuous_in g by A1, A2, Def2; thus f | X1 is_continuous_in g ::_thesis: verum proof (dom f) /\ X1 c= (dom f) /\ X by A2, XBOOLE_1:26; then dom (f | X1) c= (dom f) /\ X by RELAT_1:61; then A6: dom (f | X1) c= dom (f | X) by RELAT_1:61; g in (dom f) /\ X1 by A3, A4, XBOOLE_0:def_4; hence A7: g in dom (f | X1) by RELAT_1:61; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = g holds ( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) ) then A8: (f | X) /. g = f /. g by A6, PARTFUN2:15 .= (f | X1) /. g by A7, PARTFUN2:15 ; let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = g implies ( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) ) ) assume that A9: rng s1 c= dom (f | X1) and A10: ( s1 is convergent & lim s1 = g ) ; ::_thesis: ( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) ) A11: rng s1 c= dom (f | X) by A9, A6, XBOOLE_1:1; A12: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_((f_|_X1)_/*_s1)_._n let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = ((f | X1) /* s1) . n A13: s1 . n in rng s1 by VALUED_0:28; thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A9, A6, FUNCT_2:109, XBOOLE_1:1 .= f /. (s1 . n) by A11, A13, PARTFUN2:15 .= (f | X1) /. (s1 . n) by A9, A13, PARTFUN2:15 .= ((f | X1) /* s1) . n by A9, FUNCT_2:109 ; ::_thesis: verum end; ( (f | X) /* s1 is convergent & (f | X) /. g = lim ((f | X) /* s1) ) by A5, A10, A11, Def1; hence ( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) ) by A8, A12, FUNCT_2:63; ::_thesis: verum end; end; theorem :: CFCONT_1:42 for x0 being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st x0 in dom f holds f is_continuous_on {x0} proof let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st x0 in dom f holds f is_continuous_on {x0} let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( x0 in dom f implies f is_continuous_on {x0} ) assume A1: x0 in dom f ; ::_thesis: f is_continuous_on {x0} thus {x0} c= dom f :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in {x0} holds f | {x0} is_continuous_in x0 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x0} or x in dom f ) assume x in {x0} ; ::_thesis: x in dom f hence x in dom f by A1, TARSKI:def_1; ::_thesis: verum end; let t be Element of COMPLEX ; ::_thesis: ( t in {x0} implies f | {x0} is_continuous_in t ) assume A2: t in {x0} ; ::_thesis: f | {x0} is_continuous_in t thus f | {x0} is_continuous_in t ::_thesis: verum proof t in dom f by A1, A2, TARSKI:def_1; then t in (dom f) /\ {x0} by A2, XBOOLE_0:def_4; hence t in dom (f | {x0}) by RELAT_1:61; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = t holds ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) ) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = t implies ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) ) ) assume that A3: rng s1 c= dom (f | {x0}) and s1 is convergent and lim s1 = t ; ::_thesis: ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) ) A4: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17; rng s1 c= (dom f) /\ {x0} by A3, RELAT_1:61; then A5: rng s1 c= {x0} by A4, XBOOLE_1:1; A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_x0 let n be Element of NAT ; ::_thesis: s1 . n = x0 s1 . n in rng s1 by VALUED_0:28; hence s1 . n = x0 by A5, TARSKI:def_1; ::_thesis: verum end; A7: t = x0 by A2, TARSKI:def_1; A8: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((((f_|_{x0})_/*_s1)_._m)_-_((f_|_{x0})_/._t)).|_<_r let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r ) assume A9: 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r let m be Element of NAT ; ::_thesis: ( n <= m implies |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r ) assume n <= m ; ::_thesis: |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| = |.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).| by A7, A3, FUNCT_2:109 .= |.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).| by A6 .= 0 by COMPLEX1:44 ; hence |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r by A9; ::_thesis: verum end; hence (f | {x0}) /* s1 is convergent by COMSEQ_2:def_5; ::_thesis: (f | {x0}) /. t = lim ((f | {x0}) /* s1) hence (f | {x0}) /. t = lim ((f | {x0}) /* s1) by A8, COMSEQ_2:def_6; ::_thesis: verum end; end; theorem Th43: :: CFCONT_1:43 for X being set for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f2 is_continuous_on X holds ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X ) proof let X be set ; ::_thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f2 is_continuous_on X holds ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X ) let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_on X & f2 is_continuous_on X implies ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X ) ) assume A1: ( f1 is_continuous_on X & f2 is_continuous_on X ) ; ::_thesis: ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X ) then ( X c= dom f1 & X c= dom f2 ) by Th38; then A2: X c= (dom f1) /\ (dom f2) by XBOOLE_1:19; then A3: X c= dom (f1 + f2) by CFUNCT_1:1; now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_ (_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_/._(lim_s1)_=_lim_((f1_+_f2)_/*_s1)_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) ) assume that A4: rng s1 c= X and A5: s1 is convergent and A6: lim s1 in X ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) A7: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A4, A5, A6, Th38; then A8: (f1 /* s1) + (f2 /* s1) is convergent ; A9: rng s1 c= (dom f1) /\ (dom f2) by A2, A4, XBOOLE_1:1; ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A4, A5, A6, Th38; then (f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A3, A6, CFUNCT_1:1 .= lim ((f1 /* s1) + (f2 /* s1)) by A7, COMSEQ_2:14 .= lim ((f1 + f2) /* s1) by A9, Th7 ; hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A8, Th7; ::_thesis: verum end; hence f1 + f2 is_continuous_on X by A3, Th38; ::_thesis: ( f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X ) A10: X c= dom (f1 - f2) by A2, CFUNCT_1:2; now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_ (_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_/._(lim_s1)_=_lim_((f1_-_f2)_/*_s1)_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) ) assume that A11: rng s1 c= X and A12: s1 is convergent and A13: lim s1 in X ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A11, A12, A13, Th38; then A15: (f1 /* s1) - (f2 /* s1) is convergent ; A16: rng s1 c= (dom f1) /\ (dom f2) by A2, A11, XBOOLE_1:1; ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A11, A12, A13, Th38; then (f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A10, A13, CFUNCT_1:2 .= lim ((f1 /* s1) - (f2 /* s1)) by A14, COMSEQ_2:26 .= lim ((f1 - f2) /* s1) by A16, Th7 ; hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A16, A15, Th7; ::_thesis: verum end; hence f1 - f2 is_continuous_on X by A10, Th38; ::_thesis: f1 (#) f2 is_continuous_on X A17: X c= dom (f1 (#) f2) by A2, CFUNCT_1:3; now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_ (_(f1_(#)_f2)_/*_s1_is_convergent_&_(f1_(#)_f2)_/._(lim_s1)_=_lim_((f1_(#)_f2)_/*_s1)_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) ) ) assume that A18: rng s1 c= X and A19: s1 is convergent and A20: lim s1 in X ; ::_thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) ) A21: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A18, A19, A20, Th38; then A22: (f1 /* s1) (#) (f2 /* s1) is convergent ; A23: rng s1 c= (dom f1) /\ (dom f2) by A2, A18, XBOOLE_1:1; ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A18, A19, A20, Th38; then (f1 (#) f2) /. (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by A17, A20, CFUNCT_1:3 .= lim ((f1 /* s1) (#) (f2 /* s1)) by A21, COMSEQ_2:30 .= lim ((f1 (#) f2) /* s1) by A23, Th7 ; hence ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) ) by A23, A22, Th7; ::_thesis: verum end; hence f1 (#) f2 is_continuous_on X by A17, Th38; ::_thesis: verum end; theorem :: CFCONT_1:44 for X, X1 being set for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f2 is_continuous_on X1 holds ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) proof let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f2 is_continuous_on X1 holds ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_on X & f2 is_continuous_on X1 implies ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) ) assume ( f1 is_continuous_on X & f2 is_continuous_on X1 ) ; ::_thesis: ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) then ( f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 ) by Th41, XBOOLE_1:17; hence ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) by Th43; ::_thesis: verum end; theorem Th45: :: CFCONT_1:45 for g being Element of COMPLEX for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds g (#) f is_continuous_on X proof let g be Element of COMPLEX ; ::_thesis: for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds g (#) f is_continuous_on X let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds g (#) f is_continuous_on X let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X implies g (#) f is_continuous_on X ) assume A1: f is_continuous_on X ; ::_thesis: g (#) f is_continuous_on X then A2: X c= dom f by Th38; then A3: X c= dom (g (#) f) by CFUNCT_1:4; now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_ (_(g_(#)_f)_/*_s1_is_convergent_&_(g_(#)_f)_/._(lim_s1)_=_lim_((g_(#)_f)_/*_s1)_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) ) assume that A4: rng s1 c= X and A5: s1 is convergent and A6: lim s1 in X ; ::_thesis: ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) A7: f /* s1 is convergent by A1, A4, A5, A6, Th38; then A8: g (#) (f /* s1) is convergent ; f /. (lim s1) = lim (f /* s1) by A1, A4, A5, A6, Th38; then (g (#) f) /. (lim s1) = g * (lim (f /* s1)) by A3, A6, CFUNCT_1:4 .= lim (g (#) (f /* s1)) by A7, COMSEQ_2:18 .= lim ((g (#) f) /* s1) by A2, A4, Th8, XBOOLE_1:1 ; hence ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) by A2, A4, A8, Th8, XBOOLE_1:1; ::_thesis: verum end; hence g (#) f is_continuous_on X by A3, Th38; ::_thesis: verum end; theorem :: CFCONT_1:46 for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds - f is_continuous_on X proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds - f is_continuous_on X let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X implies - f is_continuous_on X ) A1: - f = (- 1r) (#) f by CFUNCT_1:31; assume f is_continuous_on X ; ::_thesis: - f is_continuous_on X hence - f is_continuous_on X by A1, Th45; ::_thesis: verum end; theorem Th47: :: CFCONT_1:47 for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & f " {0} = {} holds f ^ is_continuous_on X proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & f " {0} = {} holds f ^ is_continuous_on X let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X & f " {0} = {} implies f ^ is_continuous_on X ) assume that A1: f is_continuous_on X and A2: f " {0} = {} ; ::_thesis: f ^ is_continuous_on X A3: dom (f ^) = (dom f) \ {} by A2, CFUNCT_1:def_2 .= dom f ; hence A4: X c= dom (f ^) by A1, Def2; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X holds (f ^) | X is_continuous_in x0 let g be Element of COMPLEX ; ::_thesis: ( g in X implies (f ^) | X is_continuous_in g ) assume A5: g in X ; ::_thesis: (f ^) | X is_continuous_in g then A6: f | X is_continuous_in g by A1, Def2; g in (dom (f ^)) /\ X by A4, A5, XBOOLE_0:def_4; then A7: g in dom ((f ^) | X) by RELAT_1:61; now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_((f_^)_|_X)_&_s1_is_convergent_&_lim_s1_=_g_holds_ (_((f_^)_|_X)_/*_s1_is_convergent_&_lim_(((f_^)_|_X)_/*_s1)_=_((f_^)_|_X)_/._g_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom ((f ^) | X) & s1 is convergent & lim s1 = g implies ( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) /. g ) ) assume that A8: rng s1 c= dom ((f ^) | X) and A9: ( s1 is convergent & lim s1 = g ) ; ::_thesis: ( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) /. g ) rng s1 c= (dom (f ^)) /\ X by A8, RELAT_1:61; then A10: rng s1 c= dom (f | X) by A3, RELAT_1:61; then A11: (f | X) /* s1 is convergent by A6, A9, Def1; now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_<>_0c let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n <> 0c A12: s1 . n in rng s1 by VALUED_0:28; ( rng s1 c= (dom f) /\ X & (dom f) /\ X c= dom f ) by A3, A8, RELAT_1:61, XBOOLE_1:17; then A13: rng s1 c= dom f by XBOOLE_1:1; A14: now__::_thesis:_not_f_/._(s1_._n)_=_0c assume f /. (s1 . n) = 0c ; ::_thesis: contradiction then f /. (s1 . n) in {0c} by TARSKI:def_1; hence contradiction by A2, A13, A12, PARTFUN2:26; ::_thesis: verum end; ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A10, FUNCT_2:109 .= f /. (s1 . n) by A10, A12, PARTFUN2:15 ; hence ((f | X) /* s1) . n <> 0c by A14; ::_thesis: verum end; then A15: (f | X) /* s1 is non-zero by COMSEQ_1:4; g in (dom f) /\ X by A3, A4, A5, XBOOLE_0:def_4; then A16: g in dom (f | X) by RELAT_1:61; then A17: (f | X) /. g = f /. g by PARTFUN2:15; now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_^)_|_X)_/*_s1)_._n_=_(((f_|_X)_/*_s1)_")_._n let n be Element of NAT ; ::_thesis: (((f ^) | X) /* s1) . n = (((f | X) /* s1) ") . n A18: s1 . n in rng s1 by VALUED_0:28; then s1 . n in dom ((f ^) | X) by A8; then s1 . n in (dom (f ^)) /\ X by RELAT_1:61; then A19: s1 . n in dom (f ^) by XBOOLE_0:def_4; thus (((f ^) | X) /* s1) . n = ((f ^) | X) /. (s1 . n) by A8, FUNCT_2:109 .= (f ^) /. (s1 . n) by A8, A18, PARTFUN2:15 .= (f /. (s1 . n)) " by A19, CFUNCT_1:def_2 .= ((f | X) /. (s1 . n)) " by A10, A18, PARTFUN2:15 .= (((f | X) /* s1) . n) " by A10, FUNCT_2:109 .= (((f | X) /* s1) ") . n by VALUED_1:10 ; ::_thesis: verum end; then A20: ((f ^) | X) /* s1 = ((f | X) /* s1) " by FUNCT_2:63; A21: now__::_thesis:_not_f_/._g_=_0c assume f /. g = 0c ; ::_thesis: contradiction then f /. g in {0c} by TARSKI:def_1; hence contradiction by A2, A3, A4, A5, PARTFUN2:26; ::_thesis: verum end; then lim ((f | X) /* s1) <> 0c by A6, A9, A10, A17, Def1; hence ((f ^) | X) /* s1 is convergent by A11, A15, A20, COMSEQ_2:34; ::_thesis: lim (((f ^) | X) /* s1) = ((f ^) | X) /. g (f | X) /. g = lim ((f | X) /* s1) by A6, A9, A10, Def1; hence lim (((f ^) | X) /* s1) = ((f | X) /. g) " by A11, A17, A21, A15, A20, COMSEQ_2:35 .= (f /. g) " by A16, PARTFUN2:15 .= (f ^) /. g by A4, A5, CFUNCT_1:def_2 .= ((f ^) | X) /. g by A7, PARTFUN2:15 ; ::_thesis: verum end; hence (f ^) | X is_continuous_in g by A7, Def1; ::_thesis: verum end; theorem :: CFCONT_1:48 for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & (f | X) " {0} = {} holds f ^ is_continuous_on X proof let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & (f | X) " {0} = {} holds f ^ is_continuous_on X let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X & (f | X) " {0} = {} implies f ^ is_continuous_on X ) assume that A1: f is_continuous_on X and A2: (f | X) " {0} = {} ; ::_thesis: f ^ is_continuous_on X f | X is_continuous_on X by A1, Th40; then (f | X) ^ is_continuous_on X by A2, Th47; then (f ^) | X is_continuous_on X by CFUNCT_1:54; hence f ^ is_continuous_on X by Th40; ::_thesis: verum end; theorem :: CFCONT_1:49 for X being set for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f1 " {0} = {} & f2 is_continuous_on X holds f2 / f1 is_continuous_on X proof let X be set ; ::_thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f1 " {0} = {} & f2 is_continuous_on X holds f2 / f1 is_continuous_on X let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_on X & f1 " {0} = {} & f2 is_continuous_on X implies f2 / f1 is_continuous_on X ) assume that A1: ( f1 is_continuous_on X & f1 " {0} = {} ) and A2: f2 is_continuous_on X ; ::_thesis: f2 / f1 is_continuous_on X f1 ^ is_continuous_on X by A1, Th47; then f2 (#) (f1 ^) is_continuous_on X by A2, Th43; hence f2 / f1 is_continuous_on X by CFUNCT_1:39; ::_thesis: verum end; theorem :: CFCONT_1:50 for f being PartFunc of COMPLEX,COMPLEX st f is total & ( for x1, x2 being Element of COMPLEX holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Element of COMPLEX st f is_continuous_in x0 holds f is_continuous_on COMPLEX proof let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is total & ( for x1, x2 being Element of COMPLEX holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Element of COMPLEX st f is_continuous_in x0 implies f is_continuous_on COMPLEX ) assume that A1: f is total and A2: for x1, x2 being Element of COMPLEX holds f /. (x1 + x2) = (f /. x1) + (f /. x2) and A3: ex x0 being Element of COMPLEX st f is_continuous_in x0 ; ::_thesis: f is_continuous_on COMPLEX A4: dom f = COMPLEX by A1, PARTFUN1:def_2; consider x0 being Element of COMPLEX such that A5: f is_continuous_in x0 by A3; A6: (f /. x0) + 0c = f /. (x0 + 0c) .= (f /. x0) + (f /. 0c) by A2 ; A7: now__::_thesis:_for_x1_being_Element_of_COMPLEX_holds_-_(f_/._x1)_=_f_/._(-_x1) let x1 be Element of COMPLEX ; ::_thesis: - (f /. x1) = f /. (- x1) 0c = f /. (x1 + (- x1)) by A6 .= (f /. x1) + (f /. (- x1)) by A2 ; hence - (f /. x1) = f /. (- x1) ; ::_thesis: verum end; A8: now__::_thesis:_for_x1,_x2_being_Element_of_COMPLEX_holds_f_/._(x1_-_x2)_=_(f_/._x1)_-_(f_/._x2) let x1, x2 be Element of COMPLEX ; ::_thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2) thus f /. (x1 - x2) = f /. (x1 + (- x2)) .= (f /. x1) + (f /. (- x2)) by A2 .= (f /. x1) + (- (f /. x2)) by A7 .= (f /. x1) - (f /. x2) ; ::_thesis: verum end; now__::_thesis:_for_x1_being_Element_of_COMPLEX_ for_r_being_Real_st_x1_in_COMPLEX_&_r_>_0_holds_ ex_s_being_Real_st_ (_s_>_0_&_(_for_x2_being_Element_of_COMPLEX_st_x2_in_COMPLEX_&_|.(x2_-_x1).|_<_s_holds_ |.((f_/._x2)_-_(f_/._x1)).|_<_r_)_) let x1 be Element of COMPLEX ; ::_thesis: for r being Real st x1 in COMPLEX & r > 0 holds ex s being Real st ( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds |.((f /. x2) - (f /. x1)).| < r ) ) let r be Real; ::_thesis: ( x1 in COMPLEX & r > 0 implies ex s being Real st ( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds |.((f /. x2) - (f /. x1)).| < r ) ) ) assume that x1 in COMPLEX and A9: r > 0 ; ::_thesis: ex s being Real st ( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds |.((f /. x2) - (f /. x1)).| < r ) ) set y = x1 - x0; consider s being Real such that A10: 0 < s and A11: for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r by A5, A9, Th32; take s = s; ::_thesis: ( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds |.((f /. x2) - (f /. x1)).| < r ) ) thus s > 0 by A10; ::_thesis: for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds |.((f /. x2) - (f /. x1)).| < r let x2 be Element of COMPLEX ; ::_thesis: ( x2 in COMPLEX & |.(x2 - x1).| < s implies |.((f /. x2) - (f /. x1)).| < r ) assume that x2 in COMPLEX and A12: |.(x2 - x1).| < s ; ::_thesis: |.((f /. x2) - (f /. x1)).| < r A13: |.((x2 - (x1 - x0)) - x0).| = |.(x2 - x1).| ; (x1 - x0) + x0 = x1 ; then |.((f /. x2) - (f /. x1)).| = |.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).| by A2 .= |.(((f /. x2) - (f /. (x1 - x0))) - (f /. x0)).| .= |.((f /. (x2 - (x1 - x0))) - (f /. x0)).| by A8 ; hence |.((f /. x2) - (f /. x1)).| < r by A4, A11, A12, A13; ::_thesis: verum end; hence f is_continuous_on COMPLEX by A4, Th39; ::_thesis: verum end; definition let X be set ; attrX is compact means :Def3: :: CFCONT_1:def 3 for s1 being Complex_Sequence st rng s1 c= X holds ex s2 being Complex_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ); end; :: deftheorem Def3 defines compact CFCONT_1:def_3_:_ for X being set holds ( X is compact iff for s1 being Complex_Sequence st rng s1 c= X holds ex s2 being Complex_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ); theorem Th51: :: CFCONT_1:51 for f being PartFunc of COMPLEX,COMPLEX st dom f is compact & f is_continuous_on dom f holds rng f is compact proof let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( dom f is compact & f is_continuous_on dom f implies rng f is compact ) assume that A1: dom f is compact and A2: f is_continuous_on dom f ; ::_thesis: rng f is compact now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_rng_f_holds_ ex_q2_being_Element_of_K19(K20(NAT,COMPLEX))_st_ (_q2_is_subsequence_of_s1_&_q2_is_convergent_&_lim_q2_in_rng_f_) let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= rng f implies ex q2 being Element of K19(K20(NAT,COMPLEX)) st ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) ) assume A3: rng s1 c= rng f ; ::_thesis: ex q2 being Element of K19(K20(NAT,COMPLEX)) st ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) defpred S1[ set , set ] means ( $2 in dom f & f /. $2 = s1 . $1 ); A4: for n being Element of NAT ex g being Element of COMPLEX st S1[n,g] proof let n be Element of NAT ; ::_thesis: ex g being Element of COMPLEX st S1[n,g] s1 . n in rng s1 by VALUED_0:28; then consider g being Element of COMPLEX such that A5: ( g in dom f & s1 . n = f . g ) by A3, PARTFUN1:3; take g ; ::_thesis: S1[n,g] thus S1[n,g] by A5, PARTFUN1:def_6; ::_thesis: verum end; consider q1 being Complex_Sequence such that A6: for n being Element of NAT holds S1[n,q1 . n] from CFCONT_1:sch_1(A4); now__::_thesis:_for_x_being_set_st_x_in_rng_q1_holds_ x_in_dom_f let x be set ; ::_thesis: ( x in rng q1 implies x in dom f ) assume x in rng q1 ; ::_thesis: x in dom f then ex n being Element of NAT st x = q1 . n by FUNCT_2:113; hence x in dom f by A6; ::_thesis: verum end; then A7: rng q1 c= dom f by TARSKI:def_3; then consider s2 being Complex_Sequence such that A8: s2 is subsequence of q1 and A9: s2 is convergent and A10: lim s2 in dom f by A1, Def3; take q2 = f /* s2; ::_thesis: ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) rng s2 c= rng q1 by A8, VALUED_0:21; then A11: rng s2 c= dom f by A7, XBOOLE_1:1; now__::_thesis:_for_n_being_Element_of_NAT_holds_(f_/*_q1)_._n_=_s1_._n let n be Element of NAT ; ::_thesis: (f /* q1) . n = s1 . n f /. (q1 . n) = s1 . n by A6; hence (f /* q1) . n = s1 . n by A7, FUNCT_2:109; ::_thesis: verum end; then A12: f /* q1 = s1 by FUNCT_2:63; f | (dom f) is_continuous_in lim s2 by A2, A10, Def2; then A13: f is_continuous_in lim s2 by RELAT_1:68; then f /. (lim s2) = lim (f /* s2) by A9, A11, Def1; then f . (lim s2) = lim (f /* s2) by A10, PARTFUN1:def_6; hence ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A7, A12, A8, A9, A10, A13, A11, Def1, FUNCT_1:def_3, VALUED_0:22; ::_thesis: verum end; hence rng f is compact by Def3; ::_thesis: verum end; theorem :: CFCONT_1:52 for Y being Subset of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st Y c= dom f & Y is compact & f is_continuous_on Y holds f .: Y is compact proof let Y be Subset of COMPLEX; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st Y c= dom f & Y is compact & f is_continuous_on Y holds f .: Y is compact let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( Y c= dom f & Y is compact & f is_continuous_on Y implies f .: Y is compact ) assume that A1: Y c= dom f and A2: Y is compact and A3: f is_continuous_on Y ; ::_thesis: f .: Y is compact A4: dom (f | Y) = (dom f) /\ Y by RELAT_1:61 .= Y by A1, XBOOLE_1:28 ; f | Y is_continuous_on Y proof thus Y c= dom (f | Y) by A4; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in Y holds (f | Y) | Y is_continuous_in x0 let g be Element of COMPLEX ; ::_thesis: ( g in Y implies (f | Y) | Y is_continuous_in g ) assume g in Y ; ::_thesis: (f | Y) | Y is_continuous_in g then f | Y is_continuous_in g by A3, Def2; hence (f | Y) | Y is_continuous_in g by RELAT_1:72; ::_thesis: verum end; then rng (f | Y) is compact by A2, A4, Th51; hence f .: Y is compact by RELAT_1:115; ::_thesis: verum end;