:: Property of Complex Sequence and Continuity of Complex Function :: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama :: :: Received December 7, 1999 :: Copyright (c) 1999-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, COMSEQ_1, PARTFUN1, REAL_1, ORDINAL2, NAT_1, SEQ_1, FCONT_1, RELAT_1, TARSKI, SEQ_2, FUNCT_2, ARYTM_1, FUNCT_1, ARYTM_3, VALUED_1, COMPLEX1, XBOOLE_0, ORDINAL4, VALUED_0, CARD_1, XXREAL_0, XREAL_0, RCOMP_1, CFCONT_1, XCMPLX_0; notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, PARTFUN1, FUNCT_2, SEQ_1, RELSET_1, VALUED_0, VALUED_1, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, XXREAL_0, RECDEF_1; constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, COMSEQ_2, CFUNCT_1, COMSEQ_3, RECDEF_1, SEQM_3, VALUED_1, RELSET_1; registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0, VALUED_1, COMSEQ_2, XCMPLX_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, COMSEQ_2; equalities VALUED_1; expansions TARSKI, COMSEQ_2; theorems TARSKI, NAT_1, FUNCT_1, COMPLEX1, SEQ_1, SEQM_3, SEQ_4, COMSEQ_1, COMSEQ_2, COMSEQ_3, PARTFUN1, CFUNCT_1, RELAT_1, FUNCT_2, PARTFUN2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, VALUED_0, XCMPLX_0; schemes NAT_1, RECDEF_1, FUNCT_2; begin reserve n,n1,m,m1,k for Nat; reserve x,X,X1 for set; reserve g,g1,g2,t,x0,x1,x2 for Complex; reserve s1,s2,q1,seq,seq1,seq2,seq3 for Complex_Sequence; reserve Y for Subset of COMPLEX; reserve f,f1,f2,h,h1,h2 for PartFunc of COMPLEX,COMPLEX; reserve p,r,s for Real; reserve Ns,Nseq for increasing sequence of NAT; :: :: COMPLEX SEQUENCE :: definition let f,x0; pred f is_continuous_in x0 means x0 in dom f & for s1 st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds f/*s1 is convergent & f/.x0 = lim (f/*s1); end; theorem Th1: seq1=seq2-seq3 iff for n holds seq1.n=seq2.n-seq3.n proof thus seq1=seq2-seq3 implies for n holds seq1.n=seq2.n-seq3.n proof assume A1: seq1=seq2-seq3; now let n; A2: n in NAT by ORDINAL1:def 12; seq1.n=seq2.n+(-seq3).n by A1,VALUED_1:1,A2; then seq1.n=seq2.n+(-seq3.n) by VALUED_1:8; hence seq1.n=seq2.n-seq3.n; end; hence thesis; end; assume A3: for n holds seq1.n=seq2.n-seq3.n; now let n be Element of NAT; thus seq1.n = seq2.n-seq3.n by A3 .= seq2.n+-seq3.n .= seq2.n+(-seq3).n by VALUED_1:8 .= (seq2+(-seq3)).n by VALUED_1:1; end; hence thesis by FUNCT_2:63; end; theorem Th2: (seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) & (seq1 - seq2)*Ns = ( seq1*Ns) - (seq2*Ns) & (seq1 (#) seq2)*Ns = (seq1*Ns) (#) (seq2*Ns) proof now let n be Element of NAT; 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; end; hence (seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) by FUNCT_2:63; now let n be Element of NAT; 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; end; hence (seq1 - seq2)*Ns = (seq1*Ns) - (seq2*Ns) by FUNCT_2:63; now let n be Element of NAT; 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; end; hence thesis by FUNCT_2:63; end; theorem Th3: (g(#)seq)*Ns = g(#)(seq*Ns) proof now let n be Element of NAT; 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; end; hence thesis by FUNCT_2:63; end; theorem (-seq)*Ns = -(seq*Ns) & (|.seq.|)*Ns = |.(seq*Ns).| proof thus (-seq)*Ns = ((-1r)(#)seq)*Ns by COMSEQ_1:11 .= (-1r)(#)(seq*Ns) by Th3 .= -(seq*Ns) by COMSEQ_1:11; now let n be Element of NAT; 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; end; hence thesis by FUNCT_2:63; end; theorem Th5: (seq*Ns)" = (seq")*Ns proof now let n be Element of NAT; 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; end; hence thesis by FUNCT_2:63; end; theorem (seq1/"seq)*Ns = (seq1*Ns)/"(seq*Ns) proof thus (seq1/"seq)*Ns = (seq1*Ns)(#)((seq")*Ns) by Th2 .= (seq1*Ns)/"(seq*Ns) by Th5; end; theorem Th7: 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) proof 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; then A4: rng seq c= dom (h1 + h2) by VALUED_1:def 1; now let n be Element of NAT; 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; end; hence (h1+h2)/*seq=(h1/*seq)+(h2/*seq) by FUNCT_2:63; A6: rng seq c= dom (h1 - h2) by A3,CFUNCT_1:2; now let n; A7: n in NAT by ORDINAL1:def 12; A8: seq.n in rng seq by VALUED_0:28; thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A6,FUNCT_2:109,A7 .= h1/.(seq.n) - h2/.(seq.n) by A6,A8,CFUNCT_1:2 .= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A7 .= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A7; end; hence (h1-h2)/*seq=h1/*seq-h2/*seq by Th1; A9: rng seq c= dom (h1 (#) h2) by A3,VALUED_1:def 4; now let n be Element of NAT; A10: seq.n in rng seq by VALUED_0:28; thus ((h1(#)h2)/*seq).n = (h1(#)h2)/.(seq.n) by A9,FUNCT_2:109 .= (h1/.(seq.n)) * (h2/.(seq.n)) by A9,A10,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; end; hence thesis by FUNCT_2:63; end; theorem Th8: rng seq c= dom h implies (g(#)h)/*seq = g(#)(h/*seq) proof assume A1: rng seq c= dom h; then A2: rng seq c= dom (g(#)h) by VALUED_1:def 5; now let n be Element of NAT; 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; end; hence thesis by FUNCT_2:63; end; theorem rng seq c= dom h implies -(h/*seq) = (-h)/*seq by Th8; theorem Th10: rng seq c= dom (h^) implies h/*seq is non-zero proof assume A1: rng seq c= dom (h^); 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 given n being Element of NAT such that A3: (h/*seq).n=0c; 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; end; hence thesis by COMSEQ_1:4; end; theorem Th11: rng seq c= dom (h^) implies (h^)/*seq =(h/*seq)" proof assume A1: rng seq c= dom (h^); 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 let n be Element of NAT; 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; end; hence thesis by FUNCT_2:63; end; theorem rng seq c= dom h implies Re ( (h/*seq)*Ns ) = Re (h/*(seq*Ns)) proof assume A1: rng seq c= dom h; now let n be Element of NAT; (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; end; hence thesis by FUNCT_2:63; end; theorem rng seq c= dom h implies Im ( (h/*seq)*Ns ) = Im (h/*(seq*Ns)) proof assume A1: rng seq c= dom h; now let n be Element of NAT; (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; end; hence thesis by FUNCT_2:63; end; theorem 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) proof assume h1 is total & h2 is total; 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; thus (h1-h2)/*seq = h1/*seq - h2/*seq by A1,Th7; thus thesis by A1,Th7; end; theorem h is total implies (g(#)h)/*seq = g(#)(h/*seq) proof assume h is total; then dom h = COMPLEX by PARTFUN1:def 2; then rng seq c= dom h; hence thesis by Th8; end; theorem rng seq c= dom (h|X) & h"{0}={} implies ((h^)|X)/*seq = ((h|X)/*seq)" proof assume that A1: rng seq c= dom (h|X) and A2: h"{0}={}; now let x be object; assume x in rng seq; 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; end; then A5: rng seq c= dom ((h^)|X); now let n be Element of NAT; 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; end; hence thesis by FUNCT_2:63; end; theorem Th17: seq1 is subsequence of seq & seq is convergent implies seq1 is convergent proof assume that A1: seq1 is subsequence of seq and A2: seq is convergent; consider g being Complex such that A3: for p st 0

0 implies ex k st (seq ^\k) is non-zero proof assume that A1: seq is convergent and A2: lim seq<>0; consider n1 such that A3: for m st n1<=m holds |.(lim seq).|/2<|.(seq.m).| by A1,A2,COMSEQ_2:33; take k=n1; now let n be Element of NAT; 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; hence (seq ^\k).n<>0c by COMPLEX1:47; end; hence thesis by COMSEQ_1:4; end; theorem seq is convergent & lim seq<>0 implies ex seq1 st seq1 is subsequence of seq & seq1 is non-zero proof assume seq is convergent & lim seq <>0; then consider k such that A1: seq ^\k is non-zero by Th24; take seq ^\k; thus thesis by A1; end; theorem Th26: seq is constant implies seq is convergent proof assume seq is constant; 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; let p such that A2: 00 implies for seq1 st seq1 is subsequence of seq & seq1 is non-zero holds lim (seq1")=(lim seq)" proof assume that A1: seq is convergent and A2: lim seq<>0; let seq1 such that A3: seq1 is subsequence of seq and A4: seq1 is non-zero; lim seq1=lim seq by A1,A3,Th18; hence thesis by A1,A2,A3,A4,Th17,COMSEQ_2:35; end; theorem 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) proof assume that A1: seq is constant and A2: seq1 is convergent; 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; thus lim (seq-seq1) =(lim seq)-(lim seq1) by A2,A3,COMSEQ_2:26 .=(seq.0)-(lim seq1) by A1,Th27; thus lim (seq1-seq) =(lim seq1)-(lim seq) by A2,A3,COMSEQ_2:26 .=(lim seq1)-(seq.0) by A1,Th27; thus lim (seq(#)seq1) =(lim seq)*(lim seq1) by A2,A3,COMSEQ_2:30 .=(seq.0)*(lim seq1) by A1,Th27; end; scheme CompSeqChoice { P[object,object] }: ex s1 st for n holds P[n,s1.n] provided A1: for n ex g st P[n,g] proof A2: for t being Element of NAT ex ff being Element of COMPLEX st P[t,ff] proof let t be Element of NAT; consider g such that A3: P[t,g] by A1; reconsider g as Element of COMPLEX by XCMPLX_0:def 2; take g; thus P[t,g] by A3; end; consider f being sequence of COMPLEX such that A4: for t being Element of NAT holds P[t,f.t] from FUNCT_2:sch 3(A2); reconsider s=f as Complex_Sequence; take s; let n; n in NAT by ORDINAL1:def 12; hence thesis by A4; end; begin theorem f is_continuous_in x0 iff x0 in dom f & for s1 st rng s1 c= dom f & s1 is convergent & lim s1=x0 & (for n holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1) proof thus f is_continuous_in x0 implies x0 in dom f & for s1 st rng s1 c= dom f & s1 is convergent & lim s1=x0 & (for n holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1); assume that A1: x0 in dom f and A2: for s1 st rng s1 c=dom f & s1 is convergent & lim s1=x0 & (for n holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1); thus x0 in dom f by A1; let s2 such that A3: rng s2 c=dom f and A4: s2 is convergent & lim s2=x0; now per cases; suppose ex n st for m st n<=m holds s2.m=x0; then consider N be Nat such that A5: for m st N<=m holds s2.m=x0; A6: for n holds (s2^\N).n=x0 proof let n; s2.(n+N)=x0 by A5,NAT_1:12; hence thesis by NAT_1:def 3; 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 let p such that A10: p>0; reconsider n=0 as Nat; take n; let m such that n<=m; m in NAT by ORDINAL1:def 12; then |.(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.|

x0; defpred P[set,set] means for n,m st $1=n & $2=m holds nx0 & for k st nx0 holds m<=k; defpred R[set,set,set] means P[$2,$3]; defpred P[set] means s2.$1<>x0; ex m1 be Nat st 0<=m1 & s2.m1<>x0 by A12; then A13: ex m be Nat st P[m]; consider M be Nat such that A14: P[M] & for n be Nat st P[n] holds M<=n from NAT_1:sch 5(A13); reconsider M9 = M as Element of NAT by ORDINAL1:def 12; A15: now let n; consider m such that A16: n+1<=m & s2.m<>x0 by A12; take m; thus nx0 by A16,NAT_1:13; end; A17: for n being Nat for x be Element of NAT ex y be Element of NAT st R[n,x,y] proof let n be Nat; let x be Element of NAT; defpred P[Nat] means x<$1 & s2.$1<>x0; ex m st P[m] by A15; then A18: ex m be Nat st P[m]; consider l be Nat such that A19: P[l] & for k be Nat st P[k] holds l<=k from NAT_1:sch 5(A18); take l; l in NAT by ORDINAL1:def 12; hence thesis by A19; end; consider F be sequence of NAT such that A20: F.0=M9 & for n be Nat holds R[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A17); A21: for n holds F.n is real; dom F=NAT by FUNCT_2:def 1; then reconsider F as Real_Sequence by A21,SEQ_1:2; for n holds F.nx0 ex m st F.m=n proof defpred P[set] means s2.$1<>x0 & for m holds F.m<>$1; assume ex n st P[n]; then A25: ex n be Nat st P[n]; consider M1 be Nat such that A26: P[M1] & for n be Nat st P[n] holds M1<=n from NAT_1:sch 5(A25 ); defpred E[Nat] means $1x0 & ex m st F.m=$1; A27: ex n being Nat st E[n] proof take M; M<=M1 & M <> M1 by A14,A20,A26; hence Mx0 by A14; take 0; thus thesis by A20; end; A28: for n being Nat st E[n] holds n <= M1; consider MX be Nat such that A29: E[MX] & for n being Nat st E[n] holds n<=MX from NAT_1:sch 6( A28,A27 ); A30: for k st MXx0; now per cases; suppose ex m st F.m=k; hence contradiction by A29,A31,A32; end; suppose for m holds F.m<>k; hence contradiction by A26,A32; end; end; hence contradiction; end; consider m such that A33: F.m=MX by A29; A34: MXx0 by A20,A33; A35: F.(m+1)<=M1 by A20,A26,A29,A33; now assume F.(m+1)<>M1; then F.(m+1)x0; A36: for k st P[k] holds P[k+1] proof let k such that (s2*F).k<>x0; P[F.k,F.(k+1)] by A20; then s2.(F.(k+1))<>x0; hence thesis by FUNCT_2:15; end; A37: P[0] by A14,A20,FUNCT_2:15; A38: for n holds P[n] from NAT_1:sch 2(A37,A36); A39: rng (s2*F) c= rng s2 by A22,VALUED_0:21; then rng (s2*F) c= dom f by A3; then A40: f/*(s2*F) is convergent & f/.x0=lim(f/*(s2*F)) by A2,A38,A23; A41: now let p; assume A42: 0x0; then consider l be Nat such that A46: m=F.l by A24; A47: l in NAT by ORDINAL1:def 12; A48: m in NAT by ORDINAL1:def 12; n<=l by A44,A46,SEQM_3:1; then |.(f/*(s2*F)).l-f/.x0.|

0 implies f^ is_continuous_in x0 proof assume that A1: f is_continuous_in x0 and A2: f/.x0<>0; 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; then x0 in dom f \ f"{0c} by A3,XBOOLE_0:def 5; hence A4: x0 in dom (f^) by CFUNCT_1:def 2; let s1; assume that A5: rng s1 c= dom (f^) and A6: s1 is convergent & lim s1=x0; 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; then A7: f/*s1 is convergent & f/.x0 = lim (f/*s1) by A1,A6; 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; 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; end; theorem f1 is_continuous_in x0 & f1/.x0<>0 & f2 is_continuous_in x0 implies f2 /f1 is_continuous_in x0 proof assume that A1: f1 is_continuous_in x0 & f1/.x0<>0 and A2: f2 is_continuous_in x0; f1^ is_continuous_in x0 by A1,Th36; then f2(#)(f1^) is_continuous_in x0 by A2,Th33; hence thesis by CFUNCT_1:39; end; definition let f,X; pred f is_continuous_on X means X c= dom f & for x0 st x0 in X holds f|X is_continuous_in x0; end; theorem Th38: for X,f holds f is_continuous_on X iff X c= dom f & for s1 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,f; thus f is_continuous_on X implies X c= dom f & for s1 st rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) proof assume A1: f is_continuous_on X; then A2: X c= dom f; now let s1 such that A3: rng s1 c= X and A4: s1 is convergent and A5: lim s1 in X; A6: f|X is_continuous_in (lim s1) by A1,A5; A7: dom (f|X) = dom f /\ X by RELAT_1:61 .= X by A2,XBOOLE_1:28; now let n be Element of NAT; 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; 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; hence f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) by A3,A4,A7,A6,A9; end; hence thesis by A1; end; assume that A10: X c= dom f and A11: for s1 st rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1); now A12: dom (f|X) = dom f /\ X by RELAT_1:61 .= X by A10,XBOOLE_1:28; let x1 such that A13: x1 in X; now let s1 such that A14: rng s1 c= dom (f|X) and A15: s1 is convergent and A16: lim s1 = x1; now let n be Element of NAT; 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; 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; end; hence f|X is_continuous_in x1 by A13,A12; end; hence thesis by A10; end; theorem Th39: f is_continuous_on X iff X c= dom f & for x0,r st x0 in X & 00c by A14; 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 let n be Element of NAT; 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; end; then A20: ((f^)|X)/*s1 = ((f|X)/*s1)" by FUNCT_2:63; reconsider gg = g as Element of COMPLEX by XCMPLX_0:def 2; A21: now assume f/.g = 0c; then f/.gg in {0c} by TARSKI:def 1; hence contradiction by A2,A3,A4,A5,PARTFUN2:26; end; then lim ((f|X)/*s1) <> 0c by A6,A9,A10,A17; hence ((f^)|X)/*s1 is convergent by A11,A15,A20,COMSEQ_2:34; (f|X)/.g = lim ((f|X)/*s1) by A6,A9,A10; hence lim (((f^)|X)/*s1) = ((f|X)/.g)" by A11,A17,A21,A15,A20,COMSEQ_2:35 .= (f/.g)" by A16,PARTFUN2:15 .= (f^)/.gg by A4,A5,CFUNCT_1:def 2 .= ((f^)|X)/.g by A7,PARTFUN2:15; end; hence thesis by A7; end; theorem f is_continuous_on X & (f|X)"{0} = {} implies f^ is_continuous_on X proof assume that A1: f is_continuous_on X and A2: (f|X)"{0} = {}; 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 thesis by Th40; end; theorem f1 is_continuous_on X & f1"{0} = {} & f2 is_continuous_on X implies f2 /f1 is_continuous_on X proof assume that A1: f1 is_continuous_on X & f1"{0} = {} and A2: f2 is_continuous_on X; f1^ is_continuous_on X by A1,Th47; then f2(#)(f1^) is_continuous_on X by A2,Th43; hence thesis by CFUNCT_1:39; end; theorem f is total & (for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2) & (ex x0 st f is_continuous_in x0) implies f is_continuous_on COMPLEX proof assume that A1: f is total and A2: for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2 and A3: ex x0 st f is_continuous_in x0; A4: dom f = COMPLEX by A1,PARTFUN1:def 2; consider x0 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 let x1; 0c = f/.(x1+-x1) by A6 .= f/.x1+f/.(-x1) by A2; hence -(f/.x1)=f/.(-x1); end; A8: now let x1,x2; thus f/.(x1-x2)=f/.(x1+-x2) .= f/.x1 + f/.(-x2) by A2 .= f/.x1 +- f/.x2 by A7 .= f/.x1 - f/.x2; end; now let x1,r; assume that x1 in COMPLEX and A9: r>0; set y=x1-x0; consider s such that A10: 00 by A10; let x2 such that x2 in COMPLEX and A12: |.x2-x1.|