### The Mizar article:

### Property of Complex Sequence and Continuity of Complex Function

**by****Takashi Mitsuishi,****Katsumi Wasaki, and****Yasunari Shidama**

- Received December 7, 1999
Copyright (c) 1999 Association of Mizar Users

- MML identifier: CFCONT_1
- [ MML identifier index ]

environ vocabulary COMPLEX1, COMSEQ_1, PARTFUN1, ORDINAL2, SEQM_3, SEQ_1, RELAT_1, FUNCT_1, CFUNCT_1, FCONT_1, SEQ_2, FINSEQ_4, ARYTM_1, ANPROJ_1, BOOLE, FINSEQ_1, ARYTM_3, COMPTS_1, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, NUMBERS, XREAL_0, REAL_1, NAT_1, PARTFUN1, FUNCT_2, SEQ_1, RELSET_1, SEQM_3, COMPLEX1, FINSEQ_4, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3; constructors REAL_1, NAT_1, FINSEQ_4, SEQ_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, PARTFUN1, CFUNCT_1, COMPLEX1, MEMBERED; clusters FUNCT_1, RELSET_1, SEQM_3, COMSEQ_1, NAT_1, COMPLEX1, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, COMSEQ_2, COMSEQ_3, SEQM_3; theorems AXIOMS, TARSKI, NAT_1, REAL_1, FUNCT_1, COMPLEX1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, COMSEQ_1, COMSEQ_2, COMSEQ_3, PARTFUN1, CFUNCT_1, RELAT_1, FUNCT_2, FINSEQ_4, PARTFUN2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes NAT_1, RECDEF_1, SEQ_1, FUNCT_2; begin reserve n,n1,m,m1,l,k for Nat; reserve x,y,X,X1 for set; reserve g,g1,g2,t,x0,x1,x2 for Element of 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 Seq_of_Nat; reserve Rseq1 for Real_Sequence; :: :: COMPLEX SEQUENCE :: definition let h,seq; assume A1: rng seq c= dom h; func h*seq -> Complex_Sequence equals :Def1: (h qua Function)*seq; coherence proof dom seq = NAT by COMSEQ_1:2; then A2: dom ((h qua Function)*seq) = NAT by A1,RELAT_1:46; rng ((h qua Function)*seq) c= rng h by RELAT_1:45; then A3:rng ((h qua Function)*seq) c= COMPLEX by XBOOLE_1:1; for n holds ((h qua Function)*seq).n is Complex proof let n; ((h qua Function)*seq).n in rng ((h qua Function)*seq) by A2,FUNCT_1:def 5; hence thesis by A3; end; hence (h qua Function)*seq is Complex_Sequence by A2,COMSEQ_1:2; end; end; definition let f,x0; pred f is_continuous_in x0 means :Def2: 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; canceled; theorem Th2: 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 seq1=seq2-seq3; then A1: seq1=seq2+-seq3 by COMSEQ_1:def 10; now let n; seq1.n=seq2.n+(-seq3).n by A1,COMSEQ_1:def 4; then seq1.n=seq2.n+(-seq3.n) by COMSEQ_1:def 9; hence seq1.n=seq2.n-seq3.n by XCMPLX_0:def 8; end; hence thesis; end; assume A2: for n holds seq1.n=seq2.n-seq3.n; now let n; thus seq1.n = seq2.n-seq3.n by A2 .= seq2.n+-seq3.n by XCMPLX_0:def 8 .= seq2.n+(-seq3).n by COMSEQ_1:def 9 .= (seq2+(-seq3)).n by COMSEQ_1:def 4; end; then seq1=seq2+(-seq3) by COMSEQ_1:6; hence thesis by COMSEQ_1:def 10; end; theorem Th3: rng (seq^\n) c= rng seq proof let x; assume x in rng (seq^\n); then consider y such that A1: y in dom (seq^\n) & (seq^\n).y = x by FUNCT_1:def 5; reconsider y as Nat by A1; A2: (seq^\n).y = seq.(y+n) by COMSEQ_3:def 6; y+n in NAT; then y+n in dom seq by COMSEQ_1:2; hence x in rng seq by A1,A2,FUNCT_1:def 5; end; theorem Th4: rng seq c= dom f implies seq.n in dom f proof assume A1: rng seq c= dom f; n in NAT; then n in dom seq by COMSEQ_1:2; then seq.n in rng seq by FUNCT_1:def 5; hence thesis by A1; end; theorem Th5: x in rng seq iff ex n st x = seq.n proof thus x in rng seq implies ex n st x = seq.n proof assume x in rng seq; then consider y such that A1: y in dom seq & x = seq.y by FUNCT_1:def 5; reconsider m=y as Nat by A1; take m; thus thesis by A1; end; given n such that A2: x = seq.n; n in NAT; then n in dom seq by COMSEQ_1:2; hence thesis by A2,FUNCT_1:def 5; end; theorem seq.n in rng seq by Th5; theorem Th7: seq1 is_subsequence_of seq implies rng seq1 c= rng seq proof assume seq1 is_subsequence_of seq; then consider Ns such that A1: seq1 = seq (#) Ns by COMSEQ_3:def 9; let x; assume x in rng seq1; then consider n such that A2: x = (seq (#) Ns).n by A1,Th5; x = seq.(Ns.n) by A2,COMSEQ_3:def 5; hence x in rng seq by Th5; end; theorem seq1 is_subsequence_of seq & seq is non-zero implies seq1 is non-zero proof assume A1: seq1 is_subsequence_of seq & seq is non-zero; then consider Ns such that A2: seq1=seq(#)Ns by COMSEQ_3:def 9; now given n such that A3: seq1.n=0c; seq.(Ns.n) = 0c by A2,A3,COMSEQ_3:def 5; hence contradiction by A1,COMSEQ_1:4; end; hence thesis by COMSEQ_1:4; end; theorem Th9: (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; thus ((seq1 + seq2)(#)Ns).n = (seq1 + seq2).(Ns.n) by COMSEQ_3:def 5 .= seq1.(Ns.n) + seq2.(Ns.n) by COMSEQ_1:def 4 .= (seq1(#)Ns).n + seq2.(Ns.n) by COMSEQ_3:def 5 .= (seq1(#)Ns).n + (seq2(#)Ns).n by COMSEQ_3:def 5 .= (seq1(#)Ns + seq2(#)Ns).n by COMSEQ_1:def 4; end; hence (seq1 + seq2)(#)Ns = (seq1(#)Ns) + (seq2(#)Ns) by COMSEQ_1:6; now let n; thus ((seq1 - seq2)(#)Ns).n = (seq1 - seq2).(Ns.n) by COMSEQ_3:def 5 .= seq1.(Ns.n) - seq2.(Ns.n) by Th2 .= (seq1(#)Ns).n - seq2.(Ns.n) by COMSEQ_3:def 5 .= (seq1(#)Ns).n - (seq2(#)Ns).n by COMSEQ_3:def 5 .= (seq1(#)Ns - seq2(#)Ns).n by Th2; end; hence (seq1 - seq2)(#)Ns = (seq1(#)Ns) - (seq2(#)Ns) by COMSEQ_1:6; now let n; thus ((seq1 (#) seq2)(#)Ns).n = (seq1 (#) seq2).(Ns.n) by COMSEQ_3:def 5 .= seq1.(Ns.n) * seq2.(Ns.n) by COMSEQ_1:def 5 .= (seq1(#)Ns).n * seq2.(Ns.n) by COMSEQ_3:def 5 .= (seq1(#)Ns).n * (seq2(#)Ns).n by COMSEQ_3:def 5 .= ((seq1(#)Ns)(#)(seq2(#)Ns)).n by COMSEQ_1:def 5; end; hence thesis by COMSEQ_1:6; end; theorem Th10: (g(#)seq)(#)Ns = g(#)(seq(#)Ns) proof now let n; thus ((g(#)seq)(#)Ns).n = (g(#)seq).(Ns.n) by COMSEQ_3:def 5 .= g*(seq.(Ns.n)) by COMSEQ_1:def 7 .= g*((seq(#)Ns).n) by COMSEQ_3:def 5 .= (g(#)(seq(#)Ns)).n by COMSEQ_1:def 7; end; hence thesis by COMSEQ_1:6; end; theorem (-seq)(#)Ns = -(seq(#)Ns) & (|.seq.|)*Ns = |.(seq(#)Ns).| proof thus (-seq)(#)Ns = ((-1r)(#)seq)(#)Ns by COMSEQ_1:14 .= (-1r)(#)(seq(#)Ns) by Th10 .= -(seq(#)Ns) by COMSEQ_1:14; now let n; thus ((|.seq.|)*Ns).n = (|.seq.|).(Ns.n) by SEQM_3:31 .= |.seq.(Ns.n).| by COMSEQ_1:def 14 .= |.(seq(#)Ns).n.| by COMSEQ_3:def 5 .= (|.seq(#)Ns.|).n by COMSEQ_1:def 14; end; hence thesis by FUNCT_2:113; end; theorem Th12: (seq(#)Ns)" = (seq")(#)Ns proof now let n; thus ((seq(#)Ns)").n = ((seq(#)Ns).n)" by COMSEQ_1:def 11 .= (seq.(Ns.n))" by COMSEQ_3:def 5 .= (seq").(Ns.n) by COMSEQ_1:def 11 .= ((seq")(#)Ns).n by COMSEQ_3:def 5; end; hence thesis by COMSEQ_1:6; end; theorem (seq1/"seq)(#)Ns = (seq1(#)Ns)/"(seq(#)Ns) proof thus (seq1/"seq)(#)Ns = (seq1(#)(seq"))(#)Ns by COMSEQ_1:def 12 .= (seq1(#)Ns)(#)((seq")(#)Ns) by Th9 .= (seq1(#)Ns)(#)((seq(#)Ns)") by Th12 .= (seq1(#)Ns)/"(seq(#)Ns) by COMSEQ_1:def 12; end; theorem (for n holds seq.n in Y) implies rng seq c= Y proof assume A1: for n holds seq.n in Y; let x; assume x in rng seq; then ex n st seq.n=x by Th5; hence x in Y by A1; end; canceled; theorem Th16: rng seq c= dom f implies (f*seq).n = f/.(seq.n) proof assume A1: rng seq c= dom f; n in NAT; then A2: n in dom seq by COMSEQ_1:2; then A3:seq.n in rng seq by FUNCT_1:def 5; thus (f*seq).n = ((f qua Function)*seq).n by A1,Def1 .=f.(seq.n) by A2,FUNCT_1:23 .=f/.(seq.n) by A1,A3,FINSEQ_4:def 4; end; theorem Th17: rng seq c= dom f implies (f*seq)^\n=f*(seq^\n) proof assume A1: rng seq c= dom f; rng (seq^\n) c= rng seq by Th3; then A2: rng (seq^\n) c= dom f by A1,XBOOLE_1:1; now let m; thus ((f*seq)^\n).m = (f*seq).(m+n) by COMSEQ_3:def 6 .= f/.(seq.(m+n)) by A1,Th16 .= f/.((seq^\n).m) by COMSEQ_3:def 6 .= (f*(seq^\n)).m by A2,Th16; end; hence thesis by COMSEQ_1:6; end; theorem Th18: 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 assume A1: rng seq c= dom h1 /\ dom h2; dom h1 /\ dom h2 c= dom h1 & dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17; then A2: rng seq c= dom h1 & rng seq c= dom h2 by A1,XBOOLE_1:1; A3: rng seq c= dom (h1 + h2) by A1,COMSEQ_1:def 2; A4: rng seq c= dom (h1 - h2) by A1,CFUNCT_1:4; A5: rng seq c= dom (h1 (#) h2) by A1,COMSEQ_1:def 3; now let n; A6: seq.n in dom (h1 + h2) by A3,Th4; thus ((h1+h2)*seq).n = (h1+h2)/.(seq.n) by A3,Th16 .= h1/.(seq.n) + h2/.(seq.n) by A6,CFUNCT_1:3 .= (h1*seq).n + h2/.(seq.n) by A2,Th16 .= (h1*seq).n + (h2*seq).n by A2,Th16 .= ((h1*seq)+(h2*seq)).n by COMSEQ_1:def 4; end; hence (h1+h2)*seq=(h1*seq)+(h2*seq) by COMSEQ_1:6; now let n; A7: seq.n in dom (h1 - h2) by A4,Th4; thus ((h1-h2)*seq).n = (h1-h2)/.(seq.n) by A4,Th16 .= h1/.(seq.n) - h2/.(seq.n) by A7,CFUNCT_1:4 .= (h1*seq).n - h2/.(seq.n) by A2,Th16 .= (h1*seq).n - (h2*seq).n by A2,Th16; end; hence (h1-h2)*seq=h1*seq-h2*seq by Th2; now let n; A8: seq.n in dom (h1(#)h2) by A5,Th4; thus ((h1(#)h2)*seq).n = (h1(#)h2)/.(seq.n) by A5,Th16 .= (h1/.(seq.n)) * (h2/.(seq.n)) by A8,CFUNCT_1:5 .= ((h1*seq).n) * (h2/.(seq.n)) by A2,Th16 .= ((h1*seq).n) * ((h2*seq).n) by A2,Th16 .= ((h1*seq)(#)(h2*seq)).n by COMSEQ_1:def 5; end; hence thesis by COMSEQ_1:6; end; theorem Th19: 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 COMSEQ_1:def 6; now let n; A3: seq.n in dom (g(#)h) by A2,Th4; thus ((g(#)h)*seq).n = (g(#)h)/.(seq.n) by A2,Th16 .= g * (h/.(seq.n)) by A3,CFUNCT_1:7 .= g *((h*seq).n) by A1,Th16 .= (g(#)(h*seq)).n by COMSEQ_1:def 7; end; hence thesis by COMSEQ_1:6; end; theorem rng seq c= dom h implies -(h*seq) = (-h)*seq proof assume A1: rng seq c= dom h; thus -(h*seq) = (-1r)(#)(h*seq) by COMSEQ_1:14 .= ((-1r)(#)h)*seq by A1,Th19 .= (-h)*seq by CFUNCT_1:40; end; theorem Th21: rng seq c= dom (h^) implies h*seq is non-zero proof assume A1: rng seq c= dom (h^); A2: dom h \ h"{0c} c= dom h by XBOOLE_1:36; rng seq c= dom h \ h"{0c} by A1,CFUNCT_1:def 2; then A3: rng seq c= dom h by A2,XBOOLE_1:1; now given n such that A4: (h*seq).n=0c; seq.n in rng seq by Th5; 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 4; then A5: not h/.(seq.n) in {0c} by PARTFUN2:44; h/.(seq.n) =0c by A3,A4,Th16; hence contradiction by A5,TARSKI:def 1; end; hence thesis by COMSEQ_1:4; end; theorem Th22: rng seq c= dom (h^) implies (h^)*seq =(h*seq)" proof assume A1: rng seq c= dom (h^); A2: dom h \ h"{0c} c= dom h by XBOOLE_1:36; rng seq c= dom h \ h"{0c} by A1,CFUNCT_1:def 2; then A3: rng seq c= dom h by A2,XBOOLE_1:1; now let n; A4:seq.n in rng seq by Th5; thus ((h^)*seq).n = (h^)/.(seq.n) by A1,Th16 .= (h/.(seq.n))" by A1,A4,CFUNCT_1:def 2 .= ((h*seq).n)" by A3,Th16 .= ((h*seq)").n by COMSEQ_1:def 11; end; hence thesis by COMSEQ_1:6; end; theorem Th23: 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; (seq (#) Ns) is_subsequence_of seq by COMSEQ_3:def 9; then rng (seq(#)Ns) c= rng seq by Th7; then A2: rng (seq(#)Ns) c= dom h by A1,XBOOLE_1:1; thus (Re ( (h*seq)(#)Ns )).n = Re( ((h*seq)(#)Ns).n ) by COMSEQ_3:def 3 .= Re( (h*seq).(Ns.n) ) by COMSEQ_3:def 5 .= Re( h/.(seq.(Ns.n)) ) by A1,Th16 .=Re( h/.((seq(#)Ns).n) ) by COMSEQ_3:def 5 .=Re( (h*(seq(#)Ns)).n ) by A2,Th16 .=(Re (h*(seq(#)Ns)) ).n by COMSEQ_3:def 3; end; hence Re ( (h*seq)(#)Ns ) = Re (h*(seq(#)Ns)) by FUNCT_2:113; end; theorem Th24: 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; (seq (#) Ns) is_subsequence_of seq by COMSEQ_3:def 9; then rng (seq(#)Ns) c= rng seq by Th7; then A2: rng (seq(#)Ns) c= dom h by A1,XBOOLE_1:1; thus (Im ( (h*seq)(#)Ns )).n = Im( ((h*seq)(#)Ns).n ) by COMSEQ_3:def 4 .= Im( (h*seq).(Ns.n) ) by COMSEQ_3:def 5 .= Im( h/.(seq.(Ns.n)) ) by A1,Th16 .=Im( h/.((seq(#)Ns).n) ) by COMSEQ_3:def 5 .=Im( (h*(seq(#)Ns)).n ) by A2,Th16 .=(Im (h*(seq(#)Ns)) ).n by COMSEQ_3:def 4; end; hence Im ( (h*seq)(#)Ns ) = Im (h*(seq(#)Ns)) by FUNCT_2:113; end; theorem Th25: rng seq c= dom h implies (h*seq)(#)Ns = h * (seq(#)Ns) proof assume A1: rng seq c= dom h; then A2: Re ( (h*seq)(#)Ns ) = Re (h*(seq(#)Ns)) by Th23; Im ( (h*seq)(#)Ns ) = Im (h*(seq(#)Ns)) by A1,Th24; hence thesis by A2,COMSEQ_3:14; end; theorem Th26: rng seq1 c= dom h & seq2 is_subsequence_of seq1 implies h*seq2 is_subsequence_of h*seq1 proof assume A1: rng seq1 c= dom h & seq2 is_subsequence_of seq1; then consider Ns such that A2: seq2=seq1(#)Ns by COMSEQ_3:def 9; take Ns; thus thesis by A1,A2,Th25; end; theorem h is total implies (h*seq).n = h/.(seq.n) proof assume h is total; then dom h = COMPLEX by PARTFUN1:def 4; then rng seq c= dom h; hence thesis by Th16; end; theorem h is total implies h*(seq^\n) = (h*seq)^\n proof assume h is total; then dom h = COMPLEX by PARTFUN1:def 4; then rng seq c= dom h; hence thesis by Th17; 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 h1+h2 is total by CFUNCT_1:70; then dom (h1+h2) = COMPLEX by PARTFUN1:def 4; then dom h1 /\ dom h2 = COMPLEX by COMSEQ_1:def 2; then A1: rng seq c= dom h1 /\ dom h2; hence (h1+h2)*seq = h1*seq + h2*seq by Th18; thus (h1-h2)*seq = h1*seq - h2*seq by A1,Th18; thus thesis by A1,Th18; end; theorem h is total implies (g(#)h)*seq = g(#)(h*seq) proof assume h is total; then dom h = COMPLEX by PARTFUN1:def 4; then rng seq c= dom h; hence thesis by Th19; end; theorem rng seq c= dom (h|X) implies (h|X)*seq = h*seq proof assume A1: rng seq c= dom (h|X); dom (h|X) = dom h /\ X by RELAT_1:90; then dom (h|X) c= dom h by XBOOLE_1:17; then A2: rng seq c= dom h by A1,XBOOLE_1:1; now let n; A3: seq.n in rng seq by Th5; thus ((h|X)*seq).n = (h|X)/.(seq.n) by A1,Th16 .= h/.(seq.n) by A1,A3,PARTFUN2:32 .= (h*seq).n by A2,Th16; end; hence thesis by COMSEQ_1:6; end; theorem rng seq c= dom (h|X) & (rng seq c= dom (h|Y) or X c= Y) implies (h|X)*seq = (h|Y)*seq proof assume A1: rng seq c= dom (h|X) & (rng seq c= dom (h|Y) or X c= Y); now per cases by A1; suppose A2: rng seq c= dom (h|Y); now let n; A3: seq.n in rng seq by Th5; thus ((h|X)*seq).n = (h|X)/.(seq.n) by A1,Th16 .= h/.(seq.n) by A1,A3,PARTFUN2:32 .= (h|Y)/.(seq.n) by A2,A3,PARTFUN2:32 .= ((h|Y)*seq).n by A2,Th16; end; hence thesis by COMSEQ_1:6; suppose X c= Y; then dom h /\ X c= dom h /\ Y by XBOOLE_1:26; then dom (h|X) c= dom h /\ Y by RELAT_1:90; then dom (h|X) c= dom (h|Y) by RELAT_1:90; then A4: rng seq c= dom (h|Y) by A1,XBOOLE_1:1; now let n; A5: seq.n in rng seq by Th5; thus ((h|X)*seq).n = (h|X)/.(seq.n) by A1,Th16 .= h/.(seq.n) by A1,A5,PARTFUN2:32 .= (h|Y)/.(seq.n) by A4,A5,PARTFUN2:32 .= ((h|Y)*seq).n by A4,Th16; end; hence thesis by COMSEQ_1:6; end; hence thesis; end; theorem rng seq c= dom (h|X) & h"{0c}={} implies ((h^)|X)*seq = ((h|X)*seq)" proof assume A1: rng seq c= dom (h|X) & h"{0c}={}; now let x; assume x in rng seq; then x in dom (h|X) by A1; then x in dom h /\ X by RELAT_1:90; then x in dom h \ h"{0c} & x in X by A1,XBOOLE_0:def 3; then x in dom (h^) & x in X by CFUNCT_1:def 2; then x in dom (h^) /\ X by XBOOLE_0:def 3; hence x in dom ((h^)|X) by RELAT_1:90; end; then A2: rng seq c= dom ((h^)|X) by TARSKI:def 3; now let n; A3:seq.n in rng seq by Th5; then seq.n in dom (h|X) by A1; then seq.n in dom h /\ X by RELAT_1:90; then seq.n in dom h \ h"{0c} & seq.n in X by A1,XBOOLE_0:def 3; then A4: seq.n in dom (h^) & seq.n in X by CFUNCT_1:def 2; then seq.n in dom (h^) /\ X by XBOOLE_0:def 3; then A5:seq.n in dom((h^)|X) by FUNCT_1:68; thus (((h^)|X)*seq).n = ((h^)|X)/.(seq.n) by A2,Th16 .= (h^)/.(seq.n) by A5,PARTFUN2:32 .= (h/.(seq.n))" by A4,CFUNCT_1:def 2 .= ((h|X)/.(seq.n))" by A1,A3,PARTFUN2:32 .= (((h|X)*seq).n)" by A1,Th16 .= (((h|X)*seq)").n by COMSEQ_1:def 11; end; hence thesis by COMSEQ_1:6; end; definition let seq; redefine canceled; attr seq is constant means :Def4: ex g st for n holds seq.n=g; compatibility proof A1: dom seq = NAT by COMSEQ_1:2; hereby assume A2: seq is constant; consider n0 being Nat; take r = seq.n0; let n be Nat; thus seq.n = r by A1,A2,SEQM_3:def 5; end; given g such that A3: for n holds seq.n=g; let n1,n2 be set; assume A4: n1 in dom seq & n2 in dom seq; hence seq.n1 = g by A3 .= seq.n2 by A3,A4; end; end; Lm1:((ex g st for n holds seq.n=g) implies ex g st rng seq={g}) & ((ex g st rng seq={g}) implies for n holds seq.n=seq.(n+1)) & ((for n holds seq.n=seq.(n+1)) implies for n,k holds seq.n=seq.(n+k)) & ((for n,k holds seq.n=seq.(n+k)) implies for n,m holds seq.n=seq.m) & ((for n,m holds seq.n=seq.m) implies ex g st for n holds seq.n=g) proof thus (ex g st for n holds seq.n=g) implies ex g st rng seq={g} proof given g1 such that A1:for n holds seq.n=g1; take g=g1; now let y; assume y in rng seq; then consider x such that A2:x in dom seq and A3:seq.x=y by FUNCT_1:def 5; y=g1 by A1,A2,A3; hence y in {g} by TARSKI:def 1; end; then A4:rng seq c={g} by TARSKI:def 3; now let y; assume y in {g}; then A5:y=g by TARSKI:def 1; now assume A6:not y in rng seq; now let n; n in NAT; then n in dom seq by COMSEQ_1:2; then seq.n<>g by A5,A6,FUNCT_1:def 5; hence contradiction by A1; end; hence contradiction; end; hence y in rng seq; end; then {g} c= rng seq by TARSKI:def 3; hence thesis by A4,XBOOLE_0:def 10; end; thus (ex g st rng seq={g}) implies for n holds seq.n=seq.(n+1) proof given g1 such that A7:rng seq={g1}; let n; n in NAT & (n+1) in NAT; then n in dom seq & (n+1) in dom seq by COMSEQ_1:2; then seq.n in {g1} & seq.(n+1) in {g1} by A7,FUNCT_1:def 5; then seq.n=g1 & seq.(n+1)=g1 by TARSKI:def 1; hence seq.n=seq.(n+1); end; thus (for n holds seq.n=seq.(n+1)) implies for n,k holds seq.n=seq.(n+k) proof assume A8:for n holds seq.n=seq.(n+1); let n; defpred P[Nat] means seq.n=seq.(n+$1); A9:P[0]; A10:now let k such that A11:P[k]; seq.(n+k)=seq.(n+k+1) by A8; hence P[k+1] by A11,XCMPLX_1:1; end; thus for k holds P[k] from Ind(A9,A10); end; thus (for n,k holds seq.n=seq.(n+k)) implies for n,m holds seq.n=seq.m proof assume A12:for n,k holds seq.n=seq.(n+k); let n,m; A13:now assume n<=m; then ex k st m=n+k by NAT_1:28; hence seq.n=seq.m by A12; end; now assume m<=n; then ex k st n=m+k by NAT_1:28; hence seq.n=seq.m by A12; end; hence seq.n=seq.m by A13; end; assume that A14:for n,m holds seq.n=seq.m and A15:for g ex n st seq.n<>g; now let n; ex n1 st seq.n1<>seq.n by A15; hence contradiction by A14; end; hence thesis; end; theorem Th34: seq is constant iff ex g st rng seq={g} proof thus seq is constant implies ex g st rng seq={g} proof assume seq is constant; then ex g st for n holds seq.n=g by Def4; hence thesis by Lm1; end; assume ex g st rng seq={g}; then for n holds seq.n=seq.(n+1) by Lm1; then for n,k holds seq.n=seq.(n+k) by Lm1; then for n,m holds seq.n=seq.m by Lm1; hence ex g st for n holds seq.n=g by Lm1; end; theorem Th35: seq is constant iff for n holds seq.n=seq.(n+1) proof thus seq is constant implies for n holds seq.n=seq.(n+1) proof assume seq is constant; then ex g st rng seq={g} by Th34; hence thesis by Lm1; end; assume for n holds seq.n=seq.(n+1); then for n,k holds seq.n=seq.(n+k) by Lm1; then for n,m holds seq.n=seq.m by Lm1; hence ex g st for n holds seq.n=g by Lm1; end; theorem Th36: seq is constant iff for n,k holds seq.n=seq.(n+k) proof thus seq is constant implies for n,k holds seq.n=seq.(n+k) proof assume seq is constant; then for n holds seq.n=seq.(n+1) by Th35; hence thesis by Lm1; end; assume for n,k holds seq.n=seq.(n+k); then for n,m holds seq.n=seq.m by Lm1; hence ex g st for n holds seq.n=g by Lm1; end; theorem seq is constant iff for n,m holds seq.n=seq.m proof thus seq is constant implies for n,m holds seq.n=seq.m proof assume seq is constant; then for n,k holds seq.n=seq.(n+k) by Th36; hence thesis by Lm1; end; assume for n,m holds seq.n=seq.m; hence ex g st for n holds seq.n=g by Lm1; end; theorem Th38: seq ^\k is_subsequence_of seq proof deffunc f(Nat) = $1+k; consider Rseq1 such that A1:for n holds Rseq1.n=f(n) from ExRealSeq; now let n; A2:Rseq1.n=n+k & Rseq1.(n+1)=n+1+k by A1; n+k<n+k+1 by NAT_1:38; hence Rseq1.n<Rseq1.(n+1) by A2,XCMPLX_1:1; end; then A3:Rseq1 is increasing by SEQM_3:def 11; now let n; n+k is Nat; hence Rseq1.n is Nat by A1; end; then reconsider Rseq1 as increasing Seq_of_Nat by A3,SEQM_3:29; take Rseq=Rseq1; now let n; thus (seq(#)Rseq).n=seq.(Rseq.n) by COMSEQ_3:def 5 .=seq.(n+k) by A1 .=(seq ^\k).n by COMSEQ_3:def 6; end; hence thesis by COMSEQ_1:6; end; theorem Th39: 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 such that A3:for p st 0<p ex n st for m st n<=m holds |.(seq.m)-g.|<p by A2,COMSEQ_2:def 4; consider Nseq such that A4:seq1=seq(#)Nseq by A1,COMSEQ_3:def 9; take t=g; let p; assume 0<p; then consider n1 such that A5:for m st n1<=m holds |.(seq.m)-g.|<p by A3; take n=n1; let m such that A6:n<=m; m<=Nseq.m by SEQM_3:33; then A7:n<=Nseq.m by A6,AXIOMS:22; seq1.m=seq.(Nseq.m) by A4,COMSEQ_3:def 5; hence |.(seq1.m)-t.|<p by A5,A7; end; theorem Th40: seq1 is_subsequence_of seq & seq is convergent implies lim seq1=lim seq proof assume that A1:seq1 is_subsequence_of seq and A2:seq is convergent; A3:seq1 is convergent by A1,A2,Th39; consider Nseq such that A4:seq1=seq(#)Nseq by A1,COMSEQ_3:def 9; now let p; assume 0<p; then consider n1 such that A5:for m st n1<=m holds |.(seq.m)-(lim seq).|<p by A2,COMSEQ_2:def 5; take n=n1; let m such that A6:n<=m; m<=Nseq.m by SEQM_3:33; then A7:n<=Nseq.m by A6,AXIOMS:22; seq1.m=seq.(Nseq.m) by A4,COMSEQ_3:def 5; hence |.(seq1.m)-(lim seq).|<p by A5,A7; end; hence thesis by A3,COMSEQ_2:def 5; end; theorem Th41: seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n) implies seq1 is convergent proof assume that A1:seq is convergent and A2:ex k st for n st k<=n holds seq1.n=seq.n; consider g1 such that A3:for p st 0<p ex n st for m st n<=m holds |.(seq.m)-g1.|<p by A1,COMSEQ_2:def 4; consider k such that A4:for n st k<=n holds seq1.n=seq.n by A2; take g=g1; let p; assume 0<p; then consider n1 such that A5:for m st n1<=m holds |.(seq.m)-g1.|<p by A3; A6:now assume A7:k<=n1; take n=n1; let m; assume A8:n<=m; then k<=m by A7,AXIOMS:22; then seq1.m=seq.m by A4; hence |.(seq1.m)-g.|<p by A5,A8; end; now assume A9:n1<=k; take n=k; let m; assume A10:n<=m; then n1<=m by A9,AXIOMS:22; then |.(seq.m)-g1.|<p by A5; hence |.(seq1.m)-g.|<p by A4,A10; end; hence ex n st for m st n<=m holds |.seq1.m-g.|<p by A6; end; theorem seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n) implies lim seq=lim seq1 proof assume that A1:seq is convergent and A2:ex k st for n st k<=n holds seq1.n=seq.n; A3:seq1 is convergent by A1,A2,Th41; consider k such that A4:for n st k<=n holds seq1.n=seq.n by A2; now let p; assume 0<p; then consider n1 such that A5:for m st n1<=m holds |.(seq.m)-(lim seq).|<p by A1,COMSEQ_2:def 5; A6:now assume A7:k<=n1; take n=n1; let m; assume A8:n<=m; then k<=m by A7,AXIOMS:22; then seq1.m=seq.m by A4;hence |.(seq1.m)-(lim seq).|<p by A5,A8; end; now assume A9:n1<=k; take n=k; let m; assume A10:n<=m; then n1<=m by A9,AXIOMS:22; then |.(seq.m)-(lim seq).|<p by A5; hence |.(seq1.m)-(lim seq).|<p by A4,A10; end;hence ex n st for m st n<=m holds |.seq1.m-(lim seq).|<p by A6; end; hence thesis by A3,COMSEQ_2:def 5; end; theorem Th43: seq is convergent implies ((seq ^\k) is convergent & lim (seq ^\k)=lim seq) proof assume A1:seq is convergent; A2:seq^\k is_subsequence_of seq by Th38; hence seq^\k is convergent by A1,Th39; thus lim (seq ^\k)=lim seq by A1,A2,Th40; end; theorem Th44: seq is convergent & (ex k st seq=seq1 ^\k) implies seq1 is convergent proof assume that A1: seq is convergent and A2: ex k st seq=seq1 ^\k; consider k such that A3: seq=seq1 ^\k by A2; consider g1 such that A4: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p by A1,COMSEQ_2:def 4; take g=g1; let p; assume 0<p; then consider n1 such that A5: for m st n1<=m holds |.seq.m-g1.|<p by A4; take n=n1+k; let m; assume A6: n<=m; then consider l such that A7: m=n1+k+l by NAT_1:28; m-k=n1+k+l+-k by A7,XCMPLX_0:def 8; then m-k=n1+l+k+-k by XCMPLX_1:1; then m-k=n1+l+k-k by XCMPLX_0:def 8; then m-k=n1+l+(k-k) by XCMPLX_1:29; then m-k=n1+l+0 by XCMPLX_1:14; then consider m1 such that A8: m1=m-k; A9: now assume not n1<=m1; then m1+k<n1+k by REAL_1:53; then m-(k-k)<n1+k by A8,XCMPLX_1:37; then m-0<n1+k by XCMPLX_1:14; hence contradiction by A6; end; A10: m1+k=m-(k-k) by A8,XCMPLX_1:37 .=m-0 by XCMPLX_1:14 .=m; |.seq.m1-g1.|<p by A5,A9; hence |.seq1.m-g.|<p by A3,A10,COMSEQ_3:def 6; end; theorem seq is convergent & (ex k st seq=seq1 ^\k) implies lim seq1 =lim seq proof assume that A1: seq is convergent and A2: ex k st seq=seq1 ^\k; A3: seq1 is convergent by A1,A2,Th44; consider k such that A4: seq=seq1 ^\k by A2; now let p; assume 0<p; then consider n1 such that A5: for m st n1<=m holds |.seq.m-(lim seq).|<p by A1,COMSEQ_2:def 5; take n=n1+k; let m; assume A6: n<=m; then consider l such that A7: m=n1+k+l by NAT_1:28; m-k=n1+k+l+-k by A7,XCMPLX_0:def 8; then m-k=n1+l+k+-k by XCMPLX_1:1; then m-k=n1+l+k-k by XCMPLX_0:def 8; then m-k=n1+l+(k-k) by XCMPLX_1:29; then m-k=n1+l+0 by XCMPLX_1:14; then consider m1 such that A8: m1=m-k; A9: now assume not n1<=m1; then m1+k<n1+k by REAL_1:53; then m-(k-k)<n1+k by A8,XCMPLX_1:37; then m-0<n1+k by XCMPLX_1:14; hence contradiction by A6; end; A10: m1+k=m-(k-k) by A8,XCMPLX_1:37 .=m-0 by XCMPLX_1:14 .=m; |.seq.m1-(lim seq).|<p by A5,A9; hence |.seq1.m-(lim seq).|<p by A4,A10,COMSEQ_3:def 6; end; hence thesis by A3,COMSEQ_2:def 5; end; theorem Th46: seq is convergent & lim seq<>0c implies ex k st (seq ^\k) is non-zero proof assume that A1:seq is convergent and A2:lim seq<>0c; 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; 0<=n by NAT_1:18; then 0+k<=n+k by REAL_1:55; then |.(lim seq).|/2<|.(seq.(n+k)).| by A3; then A4:|.(lim seq).|/2<|.((seq ^\k).n).| by COMSEQ_3:def 6; 0<|.(lim seq).| by A2,COMPLEX1:133; then 0/2<|.(lim seq).|/2 by REAL_1:73; then 0 <|.((seq ^\k).n).| by A4,AXIOMS:22; hence (seq ^\k).n<>0c by COMPLEX1:133; end; hence thesis by COMSEQ_1:4; end; theorem seq is convergent & lim seq<>0c implies ex seq1 st seq1 is_subsequence_of seq & seq1 is non-zero proof assume that A1:seq is convergent and A2:lim seq <>0c; consider k such that A3:seq ^\k is non-zero by A1,A2,Th46; take seq ^\k; thus thesis by A3,Th38; end; theorem Th48: seq is constant implies seq is convergent proof assume seq is constant; then consider t such that A1:for n holds seq.n=t by Def4; take g=t; let p such that A2:0<p; take n=0; let m such that n<=m; |.(seq.m)-g.|=|.t-g.| by A1 .=0 by COMPLEX1:130,XCMPLX_1:14; hence |.(seq.m)-g.|<p by A2; end; theorem Th49: (seq is constant & g in rng seq or seq is constant & (ex n st seq.n=g)) implies lim seq=g proof assume A1: seq is constant & g in rng seq or seq is constant & (ex n st seq.n=g); A2:now assume that A3:seq is constant and A4:g in rng seq; consider g1 such that A5:rng seq={g1} by A3,Th34; consider g2 such that A6:for n holds seq.n=g2 by A3,Def4; A7: g=g1 by A4,A5,TARSKI:def 1; A8: seq is convergent by A3,Th48; now let p such that A9:0<p; take n=0; let m such that n<=m; m in NAT; then m in dom seq by COMSEQ_1:2; then seq.m in rng seq by FUNCT_1:def 5; then g2 in rng seq by A6; then g2=g by A5,A7,TARSKI:def 1; then seq.m=g by A6; hence |.(seq.m)-g.|<p by A9,COMPLEX1:130,XCMPLX_1:14; end; hence lim seq =g by A8,COMSEQ_2:def 5; end; now assume that A10: seq is constant and A11: ex n st seq.n=g; consider n such that A12: seq.n=g by A11; n in NAT; then n in dom seq by COMSEQ_1:2; hence lim seq= g by A2,A10,A12,FUNCT_1:def 5; end; hence thesis by A1,A2; end; theorem seq is constant implies for n holds lim seq=seq.n by Th49; theorem seq is convergent & lim seq<>0c 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<>0c; let seq1 such that A3:seq1 is_subsequence_of seq and A4:seq1 is non-zero; A5:seq1 is convergent by A1,A3,Th39; lim seq1=lim seq by A1,A3,Th40; hence lim seq1"=(lim seq)" by A2,A4,A5,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,Th48; hence lim (seq+seq1) =(lim seq)+(lim seq1) by A2,COMSEQ_2:14 .=(seq.0)+(lim seq1) by A1,Th49; thus lim (seq-seq1) =(lim seq)-(lim seq1) by A2,A3,COMSEQ_2:26 .=(seq.0)-(lim seq1) by A1,Th49; thus lim (seq1-seq) =(lim seq1)-(lim seq) by A2,A3,COMSEQ_2:26 .=(lim seq1)-(seq.0) by A1,Th49; thus lim (seq(#)seq1) =(lim seq)*(lim seq1) by A2,A3,COMSEQ_2:30 .=(seq.0)*(lim seq1) by A1,Th49; end; scheme CompSeqChoice { P[set,set] }: ex s1 st for n holds P[n,s1.n] provided A1: for n ex g st P[n,g] proof defpred R[set,set] means P[$1,$2]; A2: for t being Element of NAT ex ff being Element of COMPLEX st R[t,ff] by A1; consider f being Function of NAT,COMPLEX such that A3: for t being Element of NAT holds R[t,f.t] from FuncExD(A2); reconsider s=f as Complex_Sequence; take s; let n; thus thesis by A3; end; begin :: :: CONTINUITY OF COMPLEX FUNCTIONS :: 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) by Def2; assume A1: 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); hence x0 in dom f; let s2 such that A2: rng s2 c=dom f & 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 A3: for m st N<=m holds s2.m=x0; A4: for n holds (s2^\N).n=x0 proof let n; N<=n+N by NAT_1:37; then s2.(n+N)=x0 by A3; hence (s2^\N).n=x0 by COMSEQ_3:def 6; end; s2^\N is_subsequence_of s2 by Th38; then rng (s2^\N) c= rng s2 by Th7; then A5: rng (s2^\N) c= dom f by A2,XBOOLE_1:1; A6: now let p such that A7: p>0; take n=0; let m such that n<=m; |.(f*(s2^\N)).m-f/.x0.|=|.f/.((s2^\N).m)-f/.x0.| by A5,Th16 .=|.f/.x0-f/.x0.| by A4 .=0 by COMPLEX1:130,XCMPLX_1:14; hence |.(f*(s2^\N)).m-f/.x0.|<p by A7; end; then A8: f*(s2^\N) is convergent by COMSEQ_2:def 4; f*(s2^\N)=(f*s2)^\N by A2,Th17; then f*s2 is convergent & f/.x0=lim((f*s2)^\N) by A6,A8,Th44,COMSEQ_2:def 5; hence thesis by Th43; suppose A9: for n ex m st n<=m & s2.m<>x0; then consider m1 be Nat such that A10: 0<=m1 & s2.m1<>x0; defpred P[Nat] means s2.$1<>x0; A11: ex m st P[m] by A10; consider M be Element of NAT such that A12: P[M] & for n st P[n] holds M<=n from Min(A11); A13: now let n; consider m such that A14: n+1<=m & s2.m<>x0 by A9; take m; thus n<m & s2.m<>x0 by A14,NAT_1:38; end; defpred P[set,set] means for n,m st $1=n & $2=m holds n<m & s2.m<>x0 & for k st n<k & s2.k<>x0 holds m<=k; defpred R[set,set,set] means P[$2,$3]; A15: for n for x be Element of NAT ex y be Element of NAT st R[n,x,y] proof let n; let x be Element of NAT; defpred P[Nat] means x<$1 & s2.$1<>x0; A16: ex m st P[m] by A13; consider l be Nat such that A17: P[l] & for k st P[k] holds l<=k from Min(A16); take l; thus thesis by A17; end; reconsider M' = M as Element of NAT; consider F be Function of NAT,NAT such that A18: F.0=M' & for n be Element of NAT holds R[n,F.n,F.(n+1)] from RecExD(A15); A19: dom F=NAT & rng F c= NAT by FUNCT_2:def 1; now let n; thus F.n is real; end; then reconsider F as Real_Sequence by A19,SEQ_1:4; A20: now let n; F.n in rng F by A19,FUNCT_1:def 5;hence F.n is Nat by A19; end; now let n; F.n is Nat & F.(n+1) is Nat by A20; hence F.n<F.(n+1) by A18; end; then reconsider F as increasing Seq_of_Nat by A19,SEQM_3:def 8,def 11; A21: for n st s2.n<>x0 ex m st F.m=n proof defpred P[Nat] means s2.$1<>x0 & for m holds F.m<>$1; assume A22: ex n st P[n]; consider M1 be Nat such that A23: P[M1] & for n st P[n] holds M1<=n from Min(A22); defpred E[Nat] means $1<M1 & s2.$1<>x0 & ex m st F.m=$1; A24: ex n st E[n] proof take M; A25: M<=M1 by A12,A23; M <> M1 by A18,A23; hence M<M1 by A25,REAL_1:def 5; thus s2.M<>x0 by A12; take 0; thus thesis by A18; end; A26: for n st E[n] holds n <= M1; consider MX be Nat such that A27: E[MX] & for n st E[n] holds n<=MX from Max(A26,A24); A28: for k st MX<k & k<M1 holds s2.k=x0 proof given k such that A29: MX<k & k<M1 & s2.k<>x0; now per cases; suppose ex m st F.m=k; hence contradiction by A27,A29; suppose for m holds F.m<>k; hence contradiction by A23,A29; end; hence contradiction; end; consider m such that A30: F.m=MX by A27; A31: MX<F.(m+1) & s2.(F.(m+1))<>x0 & for k st MX<k & s2.k<>x0 holds F.(m+1)<=k by A18,A30; A32: F.(m+1)<=M1 by A18,A23,A27,A30; now assume F.(m+1)<>M1; then F.(m+1)<M1 by A32,REAL_1:def 5; hence contradiction by A28,A31; end;hence contradiction by A23; end; defpred P[Nat] means (s2(#)F).$1<>x0; A33: P[0] by A12,A18,COMSEQ_3:def 5; A34: 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 A18; then s2.(F.(k+1))<>x0; hence (s2(#)F).(k+1)<>x0 by COMSEQ_3:def 5; end; A35: for n holds P[n] from Ind(A33,A34); A36: s2(#)F is_subsequence_of s2 by COMSEQ_3:def 9; then A37: s2(#)F is convergent by A2,Th39; rng (s2(#)F) c= rng s2 by A36,Th7; then A38: rng (s2(#)F) c= dom f by A2,XBOOLE_1:1; lim (s2(#)F)=x0 by A2,A36,Th40; then A39: f*(s2(#)F) is convergent & f/.x0=lim(f*(s2(#)F)) by A1,A35,A37,A38; A40: now let p; assume A41: 0<p; then consider n such that A42: for m st n<=m holds |.(f*(s2(#)F)).m-f/.x0.|<p by A39,COMSEQ_2:def 5; take k=F.n; let m such that A43: k<=m; now per cases; suppose s2.m=x0; then |.(f*s2).m-f/.x0.|=|.f/.x0-f/.x0.| by A2,Th16 .=0 by COMPLEX1:130,XCMPLX_1:14; hence |.(f*s2).m-f/.x0.|<p by A41; suppose s2.m<>x0; then consider l be Nat such that A44: m=F.l by A21; n<=l by A43,A44,SEQM_3:7; then |.(f*(s2(#)F)).l-f/.x0.|<p by A42; then |.f/.((s2(#)F).l)-f/.x0.|<p by A38,Th16; then |.f/.(s2.m)-f/.x0.|<p by A44,COMSEQ_3:def 5; hence |.(f*s2).m-f/.x0.|<p by A2,Th16; end; hence |.(f*s2).m-f/.x0.|<p; end; hence f*s2 is convergent by COMSEQ_2:def 4; hence f/.x0=lim(f*s2) by A40,COMSEQ_2:def 5; end; hence thesis; end; theorem Th54: f is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r proof thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r proof assume A1: f is_continuous_in x0; hence x0 in dom f by Def2; given r such that A2: 0<r & for s holds not 0<s or ex x1 st x1 in dom f & |.x1-x0.|<s & not |.f/.x1-f/.x0.|<r; defpred P[Nat,Element of COMPLEX] means $2 in dom f & |.$2-x0.| < 1/($1+1) & not |.f/.$2-f/.x0.|<r; A3: for n ex g st P[n,g] proof let n; 0<n+1 by NAT_1:19; then 0<(n+1)" by REAL_1:72; then 0<1/(n+1) by XCMPLX_1:217; then consider g such that A4: g in dom f & |.g-x0.| < 1/(n+1) & not |.f/.g-f/.x0.|<r by A2; take g; thus thesis by A4; end; consider s1 such that A5: for n holds P[n,s1.n] from CompSeqChoice(A3); A6: rng s1 c= dom f proof let x; assume x in rng s1; then ex n st x=s1.n by Th5; hence thesis by A5; end; A7: now let n; not |.f/.(s1.n)-f/.x0.|<r by A5; hence not |.(f*s1).n-f/.x0.|<r by A6,Th16; end; A8: now let s; assume 0<s; then A9: 0<s" by REAL_1:72; consider n such that A10: s"<n by SEQ_4:10; take k=n; let m such that A11: k<=m; s"+0 <n+1 by A10,REAL_1:67; then 1/(n+1)<1/s" by A9,SEQ_2:10; then A12: 1/(n+1)<s by XCMPLX_1:218; A13: 0<n+1 by NAT_1:19; k+1<=m+1 by A11,AXIOMS:24; then 1/(m+1)<=1/(k+1) by A13,SEQ_4:1; then A14: 1/(m+1)<s by A12,AXIOMS:22; |.s1.m-x0.|<1/(m+1) by A5; hence |.s1.m-x0.|<s by A14,AXIOMS:22; end; then A15:s1 is convergent by COMSEQ_2:def 4; then lim s1=x0 by A8,COMSEQ_2:def 5; then f*s1 is convergent & f/.x0=lim(f*s1) by A1,A6,A15,Def2; then consider n such that A16: for m st n<=m holds |.(f*s1).m-f/.x0.|<r by A2,COMSEQ_2:def 5; |.(f*s1).n-f/.x0.|<r by A16; hence contradiction by A7; end; assume A17: x0 in dom f & for r st 0<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r; now let s1 such that A18: rng s1 c= dom f & s1 is convergent & lim s1 = x0; A19: now let p; assume 0<p; then consider s such that A20: 0<s & for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<p by A17; consider n such that A21: for m st n<=m holds |.s1.m-x0.|<s by A18,A20,COMSEQ_2:def 5; take k=n; let m such that A22: k<=m; A23:s1.m in rng s1 by Th5; |.s1.m-x0.|<s by A21,A22; then |.f/.(s1.m)-f/.x0.|<p by A18,A20,A23; hence |.(f*s1).m - f/.x0.|<p by A18,Th16; end; then f*s1 is convergent by COMSEQ_2:def 4; hence f*s1 is convergent & f/.x0 = lim (f*s1) by A19,COMSEQ_2:def 5; end; hence thesis by A17,Def2; end; theorem Th55: 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 proof assume A1: f1 is_continuous_in x0 & f2 is_continuous_in x0; then A2: x0 in dom f1 & for s1 st rng s1 c= dom f1 & s1 is convergent & lim s1 = x0 holds f1*s1 is convergent & f1/.x0 = lim (f1*s1) by Def2; A3: x0 in dom f2 & for s1 st rng s1 c= dom f2 & s1 is convergent & lim s1 = x0 holds f2*s1 is convergent & f2/.x0 = lim (f2*s1) by A1,Def2; now x0 in dom f1 /\ dom f2 by A2,A3,XBOOLE_0:def 3; hence A4: x0 in dom (f1+f2) by COMSEQ_1:def 2; let s1; assume A5: rng s1 c= dom(f1+f2) & s1 is convergent & lim s1=x0; then A6: rng s1 c= dom f1 /\ dom f2 by COMSEQ_1:def 2; dom (f1+f2) = dom f1 /\ dom f2 by COMSEQ_1:def 2; then dom (f1+f2) c= dom f1 by XBOOLE_1:17; then rng s1 c= dom f1 by A5,XBOOLE_1:1; then A7: f1*s1 is convergent & f1/.x0 = lim (f1*s1) by A1,A5,Def2; dom (f1+f2) = dom f1 /\ dom f2 by COMSEQ_1:def 2; then dom (f1+f2) c= dom f2 by XBOOLE_1:17; then rng s1 c= dom f2 by A5,XBOOLE_1:1; then A8: f2*s1 is convergent & f2/.x0 = lim (f2*s1) by A1,A5,Def2; then ((f1*s1)+(f2*s1)) is convergent by A7,COMSEQ_2:13; hence (f1+f2)*s1 is convergent by A6,Th18; thus (f1+f2)/.x0 = f1/.x0 + f2/.x0 by A4,CFUNCT_1:3 .= lim ((f1*s1) + (f2*s1)) by A7,A8,COMSEQ_2:14 .= lim ((f1+f2)*s1) by A6,Th18; end; hence f1+f2 is_continuous_in x0 by Def2; now x0 in dom f1 /\ dom f2 by A2,A3,XBOOLE_0:def 3; hence A9: x0 in dom (f1-f2) by CFUNCT_1:4; let s1; assume A10: rng s1 c= dom(f1-f2) & s1 is convergent & lim s1=x0; then A11: rng s1 c= dom f1 /\ dom f2 by CFUNCT_1:4; dom (f1-f2) = dom f1 /\ dom f2 by CFUNCT_1:4; then dom (f1-f2) c= dom f1 by XBOOLE_1:17; then rng s1 c= dom f1 by A10,XBOOLE_1:1; then A12: f1*s1 is convergent & f1/.x0 = lim (f1*s1) by A1,A10,Def2; dom (f1-f2) = dom f1 /\ dom f2 by CFUNCT_1:4; then dom (f1-f2) c= dom f2 by XBOOLE_1:17; then rng s1 c= dom f2 by A10,XBOOLE_1:1; then A13: f2*s1 is convergent & f2/.x0 = lim (f2*s1) by A1,A10,Def2; then f1*s1-f2*s1 is convergent by A12,COMSEQ_2:25; hence (f1-f2)*s1 is convergent by A11,Th18; thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A9,CFUNCT_1:4 .= lim (f1*s1 - f2*s1) by A12,A13,COMSEQ_2:26 .= lim ((f1-f2)*s1) by A11,Th18; end; hence f1-f2 is_continuous_in x0 by Def2; x0 in dom f1 /\ dom f2 by A2,A3,XBOOLE_0:def 3; hence A14: x0 in dom (f1(#)f2) by COMSEQ_1:def 3; let s1; assume A15: rng s1 c= dom(f1(#)f2) & s1 is convergent & lim s1=x0; then A16: rng s1 c= dom f1 /\ dom f2 by COMSEQ_1:def 3; dom (f1(#)f2) = dom f1 /\ dom f2 by COMSEQ_1:def 3; then dom (f1(#)f2) c= dom f1 by XBOOLE_1:17; then rng s1 c= dom f1 by A15,XBOOLE_1:1; then A17: f1*s1 is convergent & f1/.x0 = lim (f1*s1) by A1,A15,Def2; dom (f1(#)f2) = dom f1 /\ dom f2 by COMSEQ_1:def 3; then dom (f1(#)f2) c= dom f2 by XBOOLE_1:17; then rng s1 c= dom f2 by A15,XBOOLE_1:1; then A18: f2*s1 is convergent & f2/.x0 = lim (f2*s1) by A1,A15,Def2; then (f1*s1)(#)(f2*s1) is convergent by A17,COMSEQ_2:29; hence (f1(#)f2)*s1 is convergent by A16,Th18; thus (f1(#)f2)/.x0 = (f1/.x0) * (f2/.x0) by A14,CFUNCT_1:5 .= lim ((f1*s1)(#)(f2*s1)) by A17,A18,COMSEQ_2:30 .= lim ((f1(#)f2)*s1) by A16,Th18; end; theorem Th56: f is_continuous_in x0 implies g(#)f is_continuous_in x0 proof assume A1: f is_continuous_in x0; then 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) by Def2; hence A2: x0 in dom (g(#)f) by COMSEQ_1:def 6; let s1; assume A3: rng s1 c= dom(g(#)f) & s1 is convergent & lim s1=x0; then A4: rng s1 c= dom f by COMSEQ_1:def 6; then A5: f*s1 is convergent & f/.x0 = lim (f*s1) by A1,A3,Def2; then g(#)(f*s1) is convergent by COMSEQ_2:17; hence (g(#)f)*s1 is convergent by A4,Th19; thus (g(#)f)/.x0 =g*(f/.x0) by A2,CFUNCT_1:7 .= lim (g(#)(f*s1)) by A5,COMSEQ_2:18 .= lim ((g(#)f)*s1) by A4,Th19; end; theorem f is_continuous_in x0 implies -f is_continuous_in x0 proof assume A1: f is_continuous_in x0; -f=(-1r)(#)f by CFUNCT_1:40; hence thesis by A1,Th56; end; theorem Th58: f is_continuous_in x0 & f/.x0<>0c implies f^ is_continuous_in x0 proof assume A1: f is_continuous_in x0 & f/.x0<>0c; then A2: 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) by Def2; not f/.x0 in {0c} by A1,TARSKI:def 1; then not x0 in f"{0c} by PARTFUN2:44; then x0 in dom f \ f"{0c} by A2,XBOOLE_0:def 4; hence A3: x0 in dom (f^) by CFUNCT_1:def 2; A4: dom f \ f"{0c} c= dom f by XBOOLE_1:36; let s1; assume A5: rng s1 c= dom (f^) & s1 is convergent & lim s1=x0; then rng s1 c= dom f \ f"{0c} by CFUNCT_1:def 2; then rng s1 c= dom f by A4,XBOOLE_1:1; then A6: f*s1 is convergent & f/.x0 = lim (f*s1) by A1,A5,Def2; A7: f*s1 is non-zero by A5,Th21; then (f*s1)" is convergent by A1,A6,COMSEQ_2:34; hence (f^)*s1 is convergent by A5,Th22; thus (f^)/.x0 = (f/.x0)" by A3,CFUNCT_1:def 2 .= lim ((f*s1)") by A1,A6,A7,COMSEQ_2:35 .= lim ((f^)*s1) by A5,Th22; end; theorem f1 is_continuous_in x0 & f1/.x0<>0c & f2 is_continuous_in x0 implies f2/f1 is_continuous_in x0 proof assume f1 is_continuous_in x0 & f1/.x0<>0c & f2 is_continuous_in x0; then f1^ is_continuous_in x0 & f2 is_continuous_in x0 by Th58; then f2(#)(f1^) is_continuous_in x0 by Th55; hence thesis by CFUNCT_1:51; end; definition let f,X; pred f is_continuous_on X means :Def5: X c= dom f & for x0 st x0 in X holds f|X is_continuous_in x0; end; theorem Th60: 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 & for x1 st x1 in X holds f|X is_continuous_in x1 by Def5; now let s1 such that A3: rng s1 c= X & s1 is convergent & lim s1 in X; A4: dom (f|X) = dom f /\ X by FUNCT_1:68 .= X by A2,XBOOLE_1:28; A5: f|X is_continuous_in (lim s1) by A1,A3,Def5; now let n; A6:s1.n in rng s1 by Th5; A7: rng s1 c= dom f by A2,A3,XBOOLE_1:1; thus ((f|X)*s1).n = (f|X)/.(s1.n) by A3,A4,Th16 .= f/.(s1.n) by A3,A4,A6,PARTFUN2:32 .= (f*s1).n by A7,Th16; end; then A8: (f|X)*s1 = f*s1 by COMSEQ_1:6; f/.(lim s1) = (f|X)/.(lim s1) by A3,A4,PARTFUN2:32 .= lim (f*s1) by A3,A4,A5,A8,Def2; hence f*s1 is convergent & f/.(lim s1) = lim (f*s1) by A3,A4,A5,A8,Def2; end; hence thesis by A1,Def5; end; assume A9: 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); now let x1 such that A10: x1 in X; A11: dom (f|X) = dom f /\ X by FUNCT_1:68 .= X by A9,XBOOLE_1:28; now let s1 such that A12: rng s1 c= dom (f|X) & s1 is convergent & lim s1= x1 ; now let n; A13: s1.n in rng s1 by Th5; A14: rng s1 c= dom f by A9,A11,A12,XBOOLE_1:1; thus ((f|X)*s1).n = (f|X)/.(s1.n) by A12,Th16 .= f/.(s1.n) by A12,A13,PARTFUN2:32 .= (f*s1).n by A14,Th16; end; then A15: (f|X)*s1 = f*s1 by COMSEQ_1:6; (f|X)/.(lim s1) = f/.(lim s1) by A10,A11,A12,PARTFUN2:32 .= lim ((f|X)*s1) by A9,A10,A11,A12,A15; hence (f|X)*s1 is convergent & (f|X)/.x1 = lim ((f|X)*s1) by A9,A10,A11,A12, A15; end; hence f|X is_continuous_in x1 by A10,A11,Def2; end; hence thesis by A9,Def5; end; theorem Th61: f is_continuous_on X iff X c= dom f & for x0,r st x0 in X & 0<r ex s st 0<s & for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r proof thus f is_continuous_on X implies X c= dom f & for x0,r st x0 in X & 0<r ex s st 0<s & for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r proof assume A1: f is_continuous_on X; then A2: X c= dom f & for x1 st x1 in X holds f|X is_continuous_in x1 by Def5; thus X c= dom f by A1,Def5; let x0,r; assume A3: x0 in X & 0<r; then f|X is_continuous_in x0 by A1,Def5; then consider s such that A4: 0<s & for x1 st x1 in dom(f|X) & |.x1-x0.|<s holds |.(f|X)/.x1-(f|X)/.x0.|<r by A3,Th54; A5: dom (f|X) = dom f /\ X by FUNCT_1:68 .= X by A2,XBOOLE_1:28; take s; thus 0<s by A4; let x1; assume A6: x1 in X & |.x1-x0.|<s; then |.f/.x1 - f/.x0.| = |.(f|X)/.x1 - f/.x0.| by A5,PARTFUN2:32 .= |.(f|X)/.x1 - (f|X)/.x0.| by A3,A5,PARTFUN2:32; hence thesis by A4,A5,A6; end; assume that A7: X c= dom f and A8: for x0,r st x0 in X & 0<r ex s st 0<s & for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r; A9: dom (f|X) = dom f /\ X by FUNCT_1:68 .= X by A7,XBOOLE_1:28; now let x0 such that A10: x0 in X; for r st 0<r ex s st 0<s & for x1 st x1 in dom(f|X) & |.x1-x0.|<s holds |.(f|X)/.x1-(f|X)/.x0.|<r proof let r; assume 0<r; then consider s such that A11: 0<s & for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r by A8,A10; take s; thus 0<s by A11; let x1 such that A12: x1 in dom(f|X) & |.x1-x0.|<s; |.(f|X)/.x1-(f|X)/.x0.| = |.(f|X)/.x1 - f/.x0.| by A9,A10,PARTFUN2:32 .= |.f/.x1 - f/.x0.| by A12,PARTFUN2:32; hence thesis by A9,A11,A12; end; hence f|X is_continuous_in x0 by A9,A10,Th54; end; hence thesis by A7,Def5; end; theorem Th62: f is_continuous_on X iff f|X is_continuous_on X proof thus f is_continuous_on X implies f|X is_continuous_on X proof assume A1: f is_continuous_on X; then X c= dom f & for g st g in X holds f|X is_continuous_in g by Def5; then X c= dom f /\ X by XBOOLE_1:28; hence X c= dom (f|X) by RELAT_1:90; let g; assume g in X; then f|X is_continuous_in g by A1,Def5; hence (f|X)|X is_continuous_in g by RELAT_1:101; end; assume A2: f|X is_continuous_on X; then A3: X c= dom(f|X) & for g st g in X holds (f|X)|X is_continuous_in g by Def5; A4: dom f /\ X c= dom f by XBOOLE_1:17; X c= dom f /\ X by A3,RELAT_1:90; hence X c= dom f by A4,XBOOLE_1:1; let g; assume g in X; then (f|X)|X is_continuous_in g by A2,Def5; hence f|X is_continuous_in g by RELAT_1:101; end; theorem Th63: f is_continuous_on X & X1 c= X implies f is_continuous_on X1 proof assume A1: f is_continuous_on X & X1 c= X; then X c= dom f by Def5; hence A2: X1 c= dom f by A1,XBOOLE_1:1; let g; assume A3: g in X1; then A4: f|X is_continuous_in g by A1,Def5; thus f|X1 is_continuous_in g proof g in dom f /\ X1 by A2,A3,XBOOLE_0:def 3; hence A5: g in dom (f|X1) by RELAT_1:90; let s1 such that A6: rng s1 c= dom (f|X1) & s1 is convergent & lim s1 = g; dom f /\ X1 c= dom f /\ X by A1,XBOOLE_1:26; then dom (f|X1) c= dom f /\ X by RELAT_1:90; then A7: dom (f|X1) c= dom (f|X) by RELAT_1:90; then A8: rng s1 c= dom (f|X) by A6,XBOOLE_1:1; then A9: (f|X)*s1 is convergent & (f|X)/.g = lim ((f|X)*s1) by A4,A6,Def2; A10: (f|X)/.g = f/.g by A5,A7,PARTFUN2:32 .= (f|X1)/.g by A5,PARTFUN2:32; now let n; A11: s1.n in rng s1 by Th5; thus ((f|X)*s1).n = (f|X)/.(s1.n) by A8,Th16 .= f/.(s1.n) by A8,A11,PARTFUN2:32 .= (f|X1)/.(s1.n) by A6,A11,PARTFUN2:32 .= ((f|X1)*s1).n by A6,Th16; end; hence (f|X1)*s1 is convergent & (f|X1)/.g = lim ((f|X1)*s1) by A9,A10,COMSEQ_1:6; end; end; theorem x0 in dom f implies f is_continuous_on {x0} proof assume A1: x0 in dom f; thus {x0} c= dom f proof let x; assume x in {x0}; hence x in dom f by A1,TARSKI:def 1; end; let t such that A2: t in {x0}; thus f|{x0} is_continuous_in t proof A3: t=x0 by A2,TARSKI:def 1; t in dom f by A1,A2,TARSKI:def 1; then t in dom f /\ {x0} by A2,XBOOLE_0:def 3; hence t in dom (f|{x0}) by RELAT_1:90; let s1; assume A4: rng s1 c= dom(f|{x0}) & s1 is convergent & lim s1=t; then A5: rng s1 c= dom f /\ {x0} by RELAT_1:90; dom f /\ {x0} c= {x0} by XBOOLE_1:17; then A6: rng s1 c= {x0} by A5,XBOOLE_1:1; A7: now let n; s1.n in rng s1 by Th5; hence s1.n = x0 by A6,TARSKI:def 1; end; A8: now let r such that A9: 0<r; take n=0; let m such that n<=m; |.((f|{x0})*s1).m - (f|{x0})/.t.| = |.(f|{x0})/.(s1.m) - (f|{x0})/.x0.| by A3,A4,Th16 .= |.(f|{x0})/.x0 - (f|{x0})/.x0.| by A7 .= 0 by COMPLEX1:130,XCMPLX_1:14; hence |.((f|{x0})*s1).m - (f|{x0})/.t.| < r by A9; end; hence (f|{x0})*s1 is convergent by COMSEQ_2:def 4; hence (f|{x0})/.t = lim ((f|{x0})*s1) by A8,COMSEQ_2:def 5; end; end; theorem Th65: for X,f1,f2 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,f1,f2; assume that A1: f1 is_continuous_on X and A2: f2 is_continuous_on X; A3: X c= dom f1 by A1,Th60; X c= dom f2 by A2,Th60; then A4: X c= dom f1 /\ dom f2 by A3,XBOOLE_1:19; then A5: X c= dom (f1+f2) by CFUNCT_1:3; A6: X c= dom (f1-f2) by A4,CFUNCT_1:4; A7: X c= dom (f1(#)f2) by A4,CFUNCT_1:5; now let s1; assume A8: rng s1 c= X & s1 is convergent & lim s1 in X; then A9: rng s1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:1; A10: f1*s1 is convergent & f1/.(lim s1) = lim (f1*s1) by A1,A8,Th60; A11: f2*s1 is convergent & f2/.(lim s1) = lim (f2*s1) by A2,A8,Th60; then A12: (f1*s1)+(f2*s1) is convergent by A10,COMSEQ_2:13; (f1+f2)/.(lim s1) = lim (f1*s1) + lim (f2*s1) by A5,A8,A10,A11,CFUNCT_1:3 .= lim (f1*s1 + f2*s1) by A10,A11,COMSEQ_2:14 .= lim ((f1+f2)*s1) by A9,Th18; hence (f1+f2)*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)*s1) by A9,A12,Th18; end; hence f1+f2 is_continuous_on X by A5,Th60; now let s1; assume A13: rng s1 c= X & s1 is convergent & lim s1 in X; then A14: rng s1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:1; A15: f1*s1 is convergent & f1/.(lim s1) = lim (f1*s1) by A1,A13,Th60; A16: f2*s1 is convergent & f2/.(lim s1) = lim (f2*s1) by A2,A13,Th60; then A17: (f1*s1)-(f2*s1) is convergent by A15,COMSEQ_2:25; (f1-f2)/.(lim s1) = lim (f1*s1) - lim (f2*s1) by A6,A13,A15,A16,CFUNCT_1:4 .= lim (f1*s1 - f2*s1) by A15,A16,COMSEQ_2:26 .= lim ((f1-f2)*s1) by A14,Th18; hence (f1-f2)*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)*s1) by A14,A17,Th18; end; hence f1-f2 is_continuous_on X by A6,Th60; now let s1; assume A18: rng s1 c= X & s1 is convergent & lim s1 in X; then A19: rng s1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:1; A20: f1*s1 is convergent & f1/.(lim s1) = lim (f1*s1) by A1,A18,Th60; A21: f2*s1 is convergent & f2/.(lim s1) = lim (f2*s1) by A2,A18,Th60; then A22: (f1*s1)(#)(f2*s1) is convergent by A20,COMSEQ_2:29; (f1(#)f2)/.(lim s1) = lim (f1*s1) * lim (f2*s1) by A7,A18,A20,A21,CFUNCT_1: 5 .= lim ((f1*s1) (#) (f2*s1)) by A20,A21,COMSEQ_2:30 .= lim ((f1(#)f2)*s1) by A19,Th18; hence (f1(#)f2)*s1 is convergent & (f1(#)f2)/.(lim s1)=lim((f1(#)f2)*s1) by A19,A22,Th18; end; hence f1(#)f2 is_continuous_on X by A7,Th60; end; theorem for X,X1,f1,f2 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,f1,f2; assume A1: f1 is_continuous_on X & f2 is_continuous_on X1; X /\ X1 c= X & X /\ X1 c= X1 by XBOOLE_1:17; then f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 by A1,Th63; hence thesis by Th65; end; theorem Th67: for g,X,f st f is_continuous_on X holds g(#)f is_continuous_on X proof let g,X,f; assume A1: f is_continuous_on X; then A2: X c= dom f by Th60; then A3: X c= dom(g(#)f) by CFUNCT_1:7; now let s1; assume A4: rng s1 c= X & s1 is convergent & lim s1 in X; then A5: rng s1 c= dom f by A2,XBOOLE_1:1; A6: f*s1 is convergent & f/.(lim s1) = lim (f*s1) by A1,A4,Th60; then A7: g(#)(f*s1) is convergent by COMSEQ_2:17; (g(#)f)/.(lim s1) = g * lim (f*s1) by A3,A4,A6,CFUNCT_1:7 .= lim (g(#)(f*s1)) by A6,COMSEQ_2:18 .= lim ((g(#)f)*s1) by A5,Th19; hence (g(#)f)*s1 is convergent & (g(#)f)/.(lim s1)=lim((g(#)f)*s1) by A5,A7,Th19; end; hence thesis by A3,Th60; end; theorem f is_continuous_on X implies -f is_continuous_on X proof assume A1: f is_continuous_on X; -f=(-1r)(#)f by CFUNCT_1:40; hence thesis by A1,Th67; end; theorem Th69: f is_continuous_on X & f"{0c} = {} implies f^ is_continuous_on X proof assume that A1: f is_continuous_on X and A2: f"{0c} = {}; A3: dom(f^) = dom f \ {} by A2,CFUNCT_1:def 2 .= dom f; hence A4: X c= dom (f^) by A1,Def5; let g; assume A5: g in X; then A6: f|X is_continuous_in g by A1,Def5; g in dom(f^) /\ X by A4,A5,XBOOLE_0:def 3; then A7: g in dom((f^)|X) by RELAT_1:90; now let s1; assume A8: rng s1 c= dom((f^)|X) & s1 is convergent & lim s1=g; then rng s1 c= dom(f^) /\ X by RELAT_1:90; then A9: rng s1 c= dom(f|X) by A3,RELAT_1:90; then A10: (f|X)*s1 is convergent & (f|X)/.g = lim ((f|X)*s1) by A6,A8,Def2; g in dom f /\ X by A3,A4,A5,XBOOLE_0:def 3; then A11: g in dom(f|X) by RELAT_1:90; then A12: (f|X)/.g = f/.g by PARTFUN2:32; A13:now let n; A14: rng s1 c= dom f /\ X by A3,A8,RELAT_1:90; dom f /\ X c= dom f by XBOOLE_1:17; then A15: rng s1 c= dom f by A14,XBOOLE_1:1; A16: s1.n in rng s1 by Th5; A17: now assume f/.(s1.n)=0c; then f/.(s1.n) in {0c} by TARSKI:def 1; hence contradiction by A2,A15,A16,PARTFUN2:44; end; ((f|X)*s1).n = (f|X)/.(s1.n) by A9,Th16 .= f/.(s1.n) by A9,A16,PARTFUN2:32; hence ((f|X)*s1).n <>0c by A17; end; now assume f/.g = 0c; then f/.g in {0c} by TARSKI:def 1; hence contradiction by A2,A3,A4,A5,PARTFUN2:44; end; then A18: lim ((f|X)*s1) <> 0c & (f|X)*s1 is non-zero by A6,A8,A9,A12,A13,Def2,COMSEQ_1:4; now let n; A19: s1.n in rng s1 by Th5; then s1.n in dom((f^)|X) by A8; then s1.n in dom (f^) /\ X by RELAT_1:90; then A20: s1.n in dom (f^) by XBOOLE_0:def 3; thus (((f^)|X)*s1).n = ((f^)|X)/.(s1.n) by A8,Th16 .= (f^)/.(s1.n) by A8,A19,PARTFUN2:32 .= (f/.(s1.n))" by A20,CFUNCT_1:def 2 .= ((f|X)/.(s1.n))" by A9,A19,PARTFUN2:32 .= (((f|X)*s1).n)" by A9,Th16 .= (((f|X)*s1)").n by COMSEQ_1:def 11; end; then A21: ((f^)|X)*s1 = ((f|X)*s1)" by COMSEQ_1:6; hence ((f^)|X)*s1 is convergent by A10,A18,COMSEQ_2:34; thus lim (((f^)|X)*s1) = ((f|X)/.g)" by A10,A18,A21,COMSEQ_2:35 .= (f/.g)" by A11,PARTFUN2:32 .= (f^)/.g by A4,A5,CFUNCT_1:def 2 .= ((f^)|X)/.g by A7,PARTFUN2:32; end; hence thesis by A7,Def2; end; theorem f is_continuous_on X & (f|X)"{0c} = {} implies f^ is_continuous_on X proof assume f is_continuous_on X & (f|X)"{0c} = {}; then f|X is_continuous_on X & (f|X)"{0c} = {} by Th62; then (f|X)^ is_continuous_on X by Th69; then (f^)|X is_continuous_on X by CFUNCT_1:66; hence thesis by Th62; end; theorem f1 is_continuous_on X & f1"{0c} = {} & f2 is_continuous_on X implies f2/f1 is_continuous_on X proof assume f1 is_continuous_on X & f1"{0c} = {} & f2 is_continuous_on X; then f1^ is_continuous_on X & f2 is_continuous_on X by Th69; then f2(#)(f1^) is_continuous_on X by Th65; hence thesis by CFUNCT_1:51; 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 4; consider x0 such that A5: f is_continuous_in x0 by A3; f/.x0 + 0c = f/.x0 by COMPLEX1:22 .= f/.(x0+0c) by COMPLEX1:22 .= f/.x0+f/.0c by A2; then A6: f/.0c = 0c by XCMPLX_1:2; A7: now let x1; 0c = f/.(x1+-x1) by A6,XCMPLX_0:def 6 .= f/.x1+f/.(-x1) by A2; hence -(f/.x1)=f/.(-x1) by XCMPLX_0:def 6; end; A8: now let x1,x2; thus f/.(x1-x2)=f/.(x1+-x2) by XCMPLX_0:def 8 .= f/.x1 + f/.(-x2) by A2 .= f/.x1 +- f/.x2 by A7 .= f/.x1 - f/.x2 by XCMPLX_0:def 8; end; now let x1,r; assume x1 in COMPLEX & r>0; then consider s such that A9: 0<s & for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r by A5,Th54; take s; thus s>0 by A9; let x2 such that A10: x2 in COMPLEX & |.x2-x1.|<s; set y=x1-x0; A11: x1-x0+x0=x1-(x0-x0) by XCMPLX_1:37 .=x1-0c by XCMPLX_1:14 .=x1 by COMPLEX1:52; then A12: |.f/.x2-f/.x1.| = |.f/.x2-(f/.y+f/.x0).| by A2 .= |.f/.x2-f/.y-f/.x0.| by XCMPLX_1:36 .= |.f/.(x2-y)-f/.x0.| by A8; |.x2-y-x0.|=|.x2-x1.| by A11,XCMPLX_1:36; hence |.f/.x2-f/.x1.|<r by A4,A9,A10,A12; end; hence thesis by A4,Th61; end; definition let X; attr X is compact means :Def6: for s1 st (rng s1) c= X ex s2 st s2 is_subsequence_of s1 & s2 is convergent & (lim s2) in X; end; theorem Th73: for f st dom f is compact & f is_continuous_on (dom f) holds (rng f) is compact proof let f; assume that A1: dom f is compact and A2: f is_continuous_on (dom f); now let s1 such that A3: rng s1 c= rng f; defpred P[set,set] means $2 in dom f & f/.$2=s1.$1; A4: for n ex g st P[n,g] proof let n; s1.n in rng s1 by Th5; then consider g being Element of COMPLEX such that A5:g in dom f & s1.n=f.g by A3,PARTFUN1:26; take g; thus thesis by A5,FINSEQ_4:def 4; end; consider q1 such that A6: for n holds P[n,q1.n] from CompSeqChoice(A4); now let x; assume x in rng q1; then ex n st x = q1.n by Th5; hence x in dom f by A6; end; then A7: rng q1 c= dom f by TARSKI:def 3; now let n; q1.n in dom f & f/.(q1.n)=s1.n by A6; hence (f*q1).n= s1.n by A7,Th16; end; then A8: f*q1=s1 by COMSEQ_1:6; consider s2 such that A9: s2 is_subsequence_of q1 & s2 is convergent & (lim s2) in dom f by A1,A7,Def6; f|(dom f) is_continuous_in (lim s2) by A2,A9,Def5; then A10: f is_continuous_in (lim s2) by RELAT_1:97; rng s2 c= rng q1 by A9,Th7; then rng s2 c= dom f by A7,XBOOLE_1:1; then f*s2 is convergent & f/.(lim s2) = lim (f*s2) by A9,A10,Def2; then A11:f*s2 is convergent & f.(lim s2) = lim (f*s2) by A9,FINSEQ_4:def 4; take q2 = f*s2; thus q2 is_subsequence_of s1 & q2 is convergent & (lim q2) in rng f by A7,A8,A9,A11,Th26,FUNCT_1:def 5; end; hence thesis by Def6; end; theorem Y c= dom f & Y is compact & f is_continuous_on Y implies (f.:Y) is compact proof assume that A1: Y c= dom f and A2: Y is compact and A3: f is_continuous_on Y; A4: dom (f|Y) = dom f /\ Y by RELAT_1:90 .= Y by A1,XBOOLE_1:28; f|Y is_continuous_on Y proof thus Y c= dom (f|Y) by A4; let g; assume g in Y; then f|Y is_continuous_in g by A3,Def5; hence (f|Y)|Y is_continuous_in g by RELAT_1:101; end; then rng (f|Y) is compact by A2,A4,Th73; hence thesis by RELAT_1:148; end;

Back to top