g2; reconsider p = |.g1 - g2.|/2 as Real; A5: |.g1-g2.| > 0 by A4,COMPLEX1:62; then consider n1 such that A6: for m st n1<=m holds |.s.m-g1.|

convergent for Complex_Sequence; coherence proof let t be Complex_Sequence such that A1: t = s*'; consider g such that A2: for p being Real st 0

convergent for Complex_Sequence; coherence proof let s be Complex_Sequence such that A1: s = s1 + s2; consider g such that A2: for p be Real st 0

0; then consider n1 such that A5: for m st n1<=m holds |.s1.m - g.|

convergent for Complex_Sequence; coherence proof A1: now let c be Element of COMPLEX; per cases; suppose A2: c =0c; now let n; thus (c(#)s).n = 0c*s.n by A2,VALUED_1:6 .= 0c; end; hence c(#)s is convergent by Th9; end; suppose A3: c <> 0c; thus c(#)s is convergent proof consider g such that A4: for p be Real st 0

0 by A3,COMPLEX1:47; consider n such that A7: for m st n<=m holds |.s.m-g.|

0c; for p be Real st p>0 holds ex n st for m st n<=m holds |.(r(#)s) .m-r*(lim s).|

0; A3: |.r.|>0 by A1,COMPLEX1:47; p / |.r.| > 0 by A3,A2; then consider n such that A4: for m st n<=m holds |.s.m-(lim s).|< p/|.r.| by Def6; take n; let m; assume n<=m; then |.s.m-(lim s).|

convergent for Complex_Sequence; coherence; end; ::$CT theorem Th16: for s being convergent Complex_Sequence holds lim(-s)=-(lim s) proof let s being convergent Complex_Sequence; lim(-s) = (-1)*(lim s) by Th14 .= - 1r*(lim s) by COMPLEX1:def 4; hence thesis by COMPLEX1:def 4; end; ::$CT theorem for s being convergent Complex_Sequence holds lim (-s)*' = -(lim s)*' proof let s being convergent Complex_Sequence; thus lim (-s)*' = (lim (-s))*' by Th11 .= (-(lim s))*' by Th16 .= -(lim s)*' by COMPLEX1:33; end; registration let s1,s2 be convergent Complex_Sequence; cluster s1 - s2 -> convergent for Complex_Sequence; coherence proof - s2 is convergent; hence thesis; end; end; ::$CT theorem Th18: for s,s9 being convergent Complex_Sequence holds lim(s - s9)=(lim s)-( lim s9) proof let s,s9 be convergent Complex_Sequence; lim(s - s9) = (lim s) + lim(-s9) by Th12 .= (lim s) + -(lim s9) by Th16; hence thesis; end; ::$CT theorem for s,s9 being convergent Complex_Sequence holds lim (s - s9)*' = (lim s)*' - (lim s9)*' proof let s,s9 be convergent Complex_Sequence; thus lim (s - s9)*' = (lim (s - s9))*' by Th11 .= ((lim s) - (lim s9))*' by Th18 .= (lim s)*' - (lim s9)*' by COMPLEX1:34; end; registration cluster convergent -> bounded for Complex_Sequence; coherence proof let s; assume s is convergent; then consider g such that A1: for p be Real st 0

non convergent for Complex_Sequence; coherence; end; registration let s1,s2 be convergent Complex_Sequence; cluster s1 (#) s2 -> convergent for Complex_Sequence; coherence proof let s be Complex_Sequence such that A1: s = s1 (#) s2; consider g1 such that A2: for p being Real st 0

0c ex n st for m st n <=m holds |.(lim s).|/2<|.s.m.| proof let s be convergent Complex_Sequence such that A1: (lim s)<>0c; 0<|.(lim s).| by A1,COMPLEX1:47; then 0<|.(lim s).|/2; then consider n1 such that A2: for m st n1<=m holds |.s.m-(lim s).|<|.(lim s).|/2 by Def6; take n=n1; let m; assume n<=m; then A3: |.s.m-(lim s).|<|.(lim s).|/2 by A2; A4: |.(lim s)-s.m.|=|.-(s.m-(lim s)).| .=|.s.m-(lim s).| by COMPLEX1:52; A5: |.(lim s).|/2+(|.s.m.|- |.(lim s).|/2) =|.s.m.| & |.(lim s).|- |.s.m.|+ (|.s. m.|- |.(lim s).|/2) =|.(lim s).|/2; |.(lim s).|- |.s.m.|<=|.(lim s)-s.m.| by COMPLEX1:59; then |.(lim s).|- |.s.m.|<|.(lim s).|/2 by A3,A4,XXREAL_0:2; hence thesis by A5,XREAL_1:6; end; theorem Th23: for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds s" is convergent proof let s be convergent Complex_Sequence; assume that A1: (lim s)<>0c and A2: s is non-zero; consider n1 such that A3: for m st n1<=m holds |.(lim s).|/2<|.s.m.| by A1,Th22; take(lim s)"; let p be Real; assume A4: 0

|.(lim s).|/2 by A1,COMPLEX1:47; A12: (p*(|.(lim s).|/2))/(|.(lim s).|/2 ) =(p*(|.(lim s).|/2))*(|.(lim s).|/ 2 )" by XCMPLX_0:def 9 .=p*((|.(lim s).|/2)*(|.(lim s).|/2 )") .=p*1 by A11,XCMPLX_0:def 7 .=p; A13: 0<>|.(lim s).| by A1,COMPLEX1:47; A14: (p*((|.(lim s).|*|.(lim s).|)/2))/(|.s.m.|*|.(lim s).|) =(p*(2"*(|.(lim s).|*|.(lim s).|)))* (|.s.m.|*|.(lim s).|)" by XCMPLX_0:def 9 .=p*2"*((|.(lim s).|*|.(lim s).|)*(|.(lim s).|*|.s.m.|)") .=p*2"*((|.(lim s).|*|.(lim s).|)* (|.(lim s).|"*|.s.m.|")) by XCMPLX_1:204 .=p*2"*(|.(lim s).|*(|.(lim s).|*|.(lim s).|")*|.s.m.|") .=p*2"*(|.(lim s).|*1*|.s.m.|") by A13,XCMPLX_0:def 7 .=p*(|.(lim s).|/2)*|.s.m.|" .=(p*(|.(lim s).|/2))/|.s.m.| by XCMPLX_0:def 9; m in NAT by ORDINAL1:def 12; then A15: s.m <> 0 by A2,COMSEQ_1:3; then s.m*(lim s)<>0c by A1; then 0<|.s.m*(lim s).| by COMPLEX1:47; then A16: 0<|.s.m.|*|.(lim s).| by COMPLEX1:65; n2<=n by NAT_1:12; then n2<=m by A7,XXREAL_0:2; then |.s.m-(lim s).|

0c & s is non-zero implies lim s"=( lim s)" proof assume that A1: s is convergent and A2: (lim s)<>0c and A3: s is non-zero; consider n1 such that A4: for m st n1<=m holds |.(lim s).|/2<|.s.m.| by A1,A2,Th22; A5: 0<|.(lim s).| by A2,COMPLEX1:47; then 0*0<|.(lim s).|*|.(lim s).|; then A6: 0<(|.(lim s).|*|.(lim s).|)/2; A7: 0<>|.(lim s).| by A2,COMPLEX1:47; A8: now let p be Real; A9: 0<>|.(lim s).|/2 by A2,COMPLEX1:47; A10: (p*(|.(lim s).|/2))/(|.(lim s).|/2 ) =(p*(|.(lim s).|/2))*(|.(lim s) .|/2 )" by XCMPLX_0:def 9 .=p*((|.(lim s).|/2)*(|.(lim s).|/2 )") .=p*1 by A9,XCMPLX_0:def 7 .=p; assume A11: 0

0 by A3,COMSEQ_1:3; then s.m*(lim s)<>0c by A2; then 0<|.s.m*(lim s).| by COMPLEX1:47; then A19: 0<|.s.m.|*|.(lim s).| by COMPLEX1:65; n2<=n by NAT_1:12; then n2<=m by A13,XXREAL_0:2; then |.s.m-(lim s).|

0c & s is non-zero implies lim (s")*' = ((
lim s)*')"
proof
assume
A1: s is convergent & (lim s)<>0c & s is non-zero;
then s" is convergent by Th23;
hence lim (s")*' = (lim s")*' by Th11
.= ((lim s)")*' by A1,Th24
.= ((lim s)*')" by COMPLEX1:36;
end;
theorem Th26:
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies s9/"s is convergent
proof
assume that
A1: s9 is convergent and
A2: s is convergent & (lim s)<>0c & s is non-zero;
s" is convergent by A2,Th23;
hence thesis by A1;
end;
theorem Th27:
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies lim(s9/"s)=(lim s9)/(lim s)
proof
assume that
A1: s9 is convergent and
A2: s is convergent & (lim s)<>0c & s is non-zero;
s" is convergent by A2,Th23;
then lim (s9(#)(s"))=(lim s9)*(lim s") by A1,Th20
.=(lim s9)*(lim s)" by A2,Th24
.=(lim s9)/(lim s) by XCMPLX_0:def 9;
hence thesis;
end;
::$CT
theorem
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies lim (s9/"s)*' = ((lim s9)*')/((lim s)*')
proof
assume
A1: s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero;
then s9/"s is convergent by Th26;
hence lim (s9/"s)*' = (lim (s9/"s))*' by Th11
.= ((lim s9)/(lim s))*' by A1,Th27
.= ((lim s9)*')/((lim s)*') by COMPLEX1:37;
end;
theorem Th29:
s is convergent & s1 is bounded & (lim s)=0c implies s(#)s1 is convergent
proof
assume that
A1: s is convergent and
A2: s1 is bounded and
A3: (lim s) = 0c;
take g=0c;
consider R such that
A4: 0