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: 0

0 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 n x0;
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 & 0~~0 by A10;
let x2 such that
x2 in COMPLEX and
A12: |.x2-x1.|~~