:: Property of Complex Sequence and Continuity of Complex Function
::  by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2019 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, ZFMISC_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_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 ZFMISC_1, 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<p ex n st for m st n<=m holds |.(seq.m)-g.|<p by A2;
  take t=g;
  let p;
  assume 0<p;
  then consider n1 such that
A4: for m st n1<=m holds |.(seq.m)-g.|<p by A3;
  take n=n1;
  let m such that
A5: n<=m;
  consider Nseq such that
A6: seq1=seq*Nseq by A1,VALUED_0:def 17;
  m<=Nseq.m by SEQM_3:14;
  then
A7: n<=Nseq.m by A5,XXREAL_0:2;
   m in NAT by ORDINAL1:def 12;
  then seq1.m=seq.(Nseq.m) by A6,FUNCT_2:15;
  hence |.(seq1.m)-t.|<p by A4,A7;
end;

theorem Th18:
  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;
  consider Nseq such that
A3: seq1=seq*Nseq by A1,VALUED_0:def 17;
A4: 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 6;
    take n=n1;
    let m such that
A6: n<=m;
    m<=Nseq.m by SEQM_3:14;
    then
A7: n<=Nseq.m by A6,XXREAL_0:2;
A8: m in NAT by ORDINAL1:def 12;
    seq1.m=seq.(Nseq.m) by A3,FUNCT_2:15,A8;
    hence |.(seq1.m)-(lim seq).|<p by A5,A7;
  end;
  seq1 is convergent by A1,A2,Th17;
  hence thesis by A4,COMSEQ_2:def 6;
end;

theorem Th19:
  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 being Complex such that
A3: for p st 0<p ex n st for m st n<=m holds |.(seq.m)-g1.|<p by A1;
  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: n1<=k;
    take n=k;
    let m;
    assume
A8: n<=m;
    then n1<=m by A7,XXREAL_0:2;
    then |.(seq.m)-g1.|<p by A5;
    hence |.(seq1.m)-g.|<p by A4,A8;
  end;
  now
    assume
A9: k<=n1;
    take n=n1;
    let m;
    assume
A10: n<=m;
    then seq1.m=seq.m by A4,A9,XXREAL_0:2;
    hence |.(seq1.m)-g.|<p by A5,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;
  consider k such that
A3: for n st k<=n holds seq1.n=seq.n by A2;
A4: 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 6;
A6: now
      assume
A7:   n1<=k;
      take n=k;
      let m;
      assume
A8:   n<=m;
      then n1<=m by A7,XXREAL_0:2;
      then |.(seq.m)-(lim seq).|<p by A5;
      hence |.(seq1.m)-(lim seq).|<p by A3,A8;
    end;
    now
      assume
A9:   k<=n1;
      take n=n1;
      let m;
      assume
A10:  n<=m;
      then seq1.m=seq.m by A3,A9,XXREAL_0:2;
      hence |.(seq1.m)-(lim seq).|<p by A5,A10;
    end;
    hence ex n st for m st n<=m holds |.seq1.m-(lim seq).|<p by A6;
  end;
  seq1 is convergent by A1,A2,Th19;
  hence thesis by A4,COMSEQ_2:def 6;
end;

theorem
  seq is convergent implies (seq ^\k) is convergent & lim (seq ^\k)=lim
  seq by Th17,Th18;

theorem Th22:
  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 being Complex such that
A4: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p by A1;
  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 being Nat such that
A7: m=n1+k+l by NAT_1:10;
  reconsider l as Element of NAT by ORDINAL1:def 12;
  m-k=n1+l+k+-k by A7;
  then consider m1 such that
A8: m1=m-k;
  now
    assume not n1<=m1;
    then m1+k<n1+k by XREAL_1:6;
    hence contradiction by A6,A8;
  end;
  then
A9: |.seq.m1-g1.|<p by A5;
  m1+k=m by A8;
  hence |.seq1.m-g.|<p by A3,A9,NAT_1:def 3;
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;
  consider k such that
A3: seq=seq1 ^\k by A2;
A4: 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 6;
    take n=n1+k;
    let m;
    assume
A6: n<=m;
    then consider l being Nat such that
A7: m=n1+k+l by NAT_1:10;
    reconsider l as Element of NAT by ORDINAL1:def 12;
    m-k=n1+l+k+-k by A7;
    then consider m1 such that
A8: m1=m-k;
    now
      assume not n1<=m1;
      then m1+k<n1+k by XREAL_1:6;
      hence contradiction by A6,A8;
    end;
    then
A9: |.seq.m1-(lim seq).|<p by A5;
    m1+k=m by A8;
    hence |.seq1.m-(lim seq).|<p by A3,A9,NAT_1:def 3;
  end;
  seq1 is convergent by A1,A2,Th22;
  hence thesis by A4,COMSEQ_2:def 6;
end;

theorem Th24:
  seq is convergent & lim seq<>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<p;
  take n=0;
  let m such that
  n<=m;
  |.(seq.m)-g.|=|.t-g.| by A1
    .=0 by COMPLEX1:44;
  hence |.(seq.m)-g.|<p by A2;
end;

theorem Th27:
  (seq is constant & g in rng seq or seq is constant & ex n st seq
  .n=g ) implies lim seq=g
proof
A1: now
    assume that
A2: seq is constant and
A3: g in rng seq;
    consider g1 being Element of COMPLEX such that
A4: rng seq={g1} by A2,FUNCT_2:111;
    consider g2 being Element of COMPLEX such that
A5: for n being Nat holds seq.n=g2 by A2,VALUED_0:def 18;
A6: g=g1 by A3,A4,TARSKI:def 1;
A7: now
      let p such that
A8:   0<p;
       reconsider n=0 as Nat;
      take n;
      let m such that
      n<=m;
      m in NAT by ORDINAL1:def 12;
      then m in dom seq by COMSEQ_1:2;
      then seq.m in rng seq by FUNCT_1:def 3;
      then g2 in rng seq by A5;
      then g2=g by A4,A6,TARSKI:def 1;
      then seq.m=g by A5;
      hence |.(seq.m)-g.|<p by A8,COMPLEX1:44;
    end;
    seq is convergent by A2,Th26;
    hence thesis by A7,COMSEQ_2:def 6;
  end;
A9: now
    assume that
 seq is constant and
A10: ex n st seq.n=g;
    consider n such that
A11: seq.n=g by A10;
    n in NAT by ORDINAL1:def 12;
    then n in dom seq by COMSEQ_1:2;
    hence thesis by A1,A11,FUNCT_1:def 3;
  end;
  assume seq is constant & g in rng seq or seq is constant &
   ex n being Nat st seq.n=g;
  hence thesis by A1,A9;
end;

theorem
  seq is constant implies for n holds lim seq=seq.n by Th27;

theorem
  seq is convergent & lim seq<>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.|<p by A10;
      end;
      then
A11:  f/*(s2^\N) is convergent;
      then f/.x0=lim((f/*s2)^\N) by A9,A7,COMSEQ_2:def 6;
      hence thesis by A11,A7,Th18,Th22;
    end;
    suppose
A12:  for n ex m st n<=m & s2.m<>x0;
      defpred P2[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 P2[$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 n<m & s2.m<>x0 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.n<F.(n+1) by A20;
      then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A22:  s2*F is subsequence of s2 by VALUED_0:def 17;
      then
A23:  s2*F is convergent & lim (s2*F)=x0 by A4,Th17,Th18;
A24:  for n st s2.n<>x0 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 $1<M1 & s2.$1<>x0 & 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 M<M1 by XXREAL_0:1;
          thus s2.M<>x0 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 MX<k & k<M1 holds s2.k=x0
        proof
          given k such that
A31:      MX<k and
A32:      k<M1 & s2.k<>x0;
          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:    MX<F.(m+1) & s2.(F.(m+1))<>x0 by A20,A33;
A35:    F.(m+1)<=M1 by A20,A26,A29,A33;
        now
          assume F.(m+1)<>M1;
          then F.(m+1)<M1 by A35,XXREAL_0:1;
          hence contradiction by A30,A34;
        end;
        hence contradiction by A26;
      end;
      defpred P[Nat] means (s2*F).$1<>x0;
A36:  for k st P[k] holds P[k+1]
      proof
        let k such that
        (s2*F).k<>x0;
        P2[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:    0<p;
        then consider n such that
A43:    for m st n<=m holds |.(f/*(s2*F)).m-f/.x0.|<p by A40,COMSEQ_2:def 6;
         reconsider k=F.n as Nat;
        take k;
        let m such that
A44:    k<=m;
          per cases;
          suppose
A45:         s2.m=x0;
            m in NAT by ORDINAL1:def 12;
            then |.(f/*s2).m-f/.x0.|=|.f/.x0-f/.x0.| by A3,FUNCT_2:109,A45
              .=0 by COMPLEX1:44;
            hence |.(f/*s2).m-f/.x0.|<p by A42;
          end;
          suppose
            s2.m<>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.|<p by A43;
            then |.f/.((s2*F).l)-f/.x0.|<p
              by A3,A39,FUNCT_2:109,XBOOLE_1:1,A47;
            then |.f/.(s2.m)-f/.x0.|<p by A46,FUNCT_2:15,A47;
            hence |.(f/*s2).m-f/.x0.|<p by A3,FUNCT_2:109,A48;
          end;
      end;
      hence f/*s2 is convergent;
      hence f/.x0=lim(f/*s2) by A41,COMSEQ_2:def 6;
    end;
  end;
  hence thesis;
end;

theorem Th32:
  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;
    given r such that
A2: 0<r and
A3: 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,Complex] means $2 in dom f & |.$2-x0.|
    < 1/($1+1) & not |.f/.$2-f/.x0.|<r;
A4: for n ex g st P[n,g]
    proof
      let n;
      0<1/(n+1);
      then consider g such that
A5:   g in dom f & |.g-x0.| < 1/(n+1) & not |.f/.g-f/.x0.|<r by A3;
      take g;
      thus thesis by A5;
    end;
    consider s1 such that
A6: for n holds P[n,s1.n] from CompSeqChoice(A4);
A7: rng s1 c= dom f
    proof
      let x be object;
      assume x in rng s1;
      then ex n being Element of NAT st x=s1.n by FUNCT_2:113;
      hence thesis by A6;
    end;
A8: now
      let n;
A9:   n in NAT by ORDINAL1:def 12;
      not |.f/.(s1.n)-f/.x0.|<r by A6;
      hence not |.(f/*s1).n-f/.x0.|<r by A7,FUNCT_2:109,A9;
    end;
A10: now
     let s;
      consider n such that
A11:  s"<n by SEQ_4:3;
      assume 0<s;
      then
A12:  0<s";
      s"+0 <n+1 by A11,XREAL_1:8;
      then 1/(n+1)<1/s" by A12,XREAL_1:76;
      then
A13:  1/(n+1)<s by XCMPLX_1:216;
      take k=n;
      let m;
      assume k<=m;
      then k+1<=m+1 by XREAL_1:6;
      then 1/(m+1)<=1/(k+1) by XREAL_1:118;
      then 1/(m+1)<s by A13,XXREAL_0:2;
      hence |.s1.m-x0.|<s by A6,XXREAL_0:2;
    end;
    then
A14: s1 is convergent;
    then lim s1=x0 by A10,COMSEQ_2:def 6;
    then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A14;
    then consider n such that
A15: for m st n<=m holds |.(f/*s1).m-f/.x0.|<r by A2,COMSEQ_2:def 6;
    |.(f/*s1).n-f/.x0.|<r by A15;
    hence contradiction by A8;
  end;
  assume that
A16: x0 in dom f and
A17: 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 and
A19: s1 is convergent & lim s1 = x0;
A20: now
      let p;
      assume 0<p;
      then consider s such that
A21:  0<s and
A22:  for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<p by A17;
      consider n such that
A23:  for m st n<=m holds |.s1.m-x0.|<s by A19,A21,COMSEQ_2:def 6;
      take k=n;
      let m;
A24:    m in NAT by ORDINAL1:def 12;
      assume k<=m;
      then s1.m in rng s1 & |.s1.m-x0.|<s by A23,VALUED_0:28;
      then |.f/.(s1.m)-f/.x0.|<p by A18,A22;
      hence |.(f/*s1).m - f/.x0.|<p by A18,FUNCT_2:109,A24;
    end;
    then f/*s1 is convergent;
    hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A20,COMSEQ_2:def 6;
  end;
  hence thesis by A16;
end;

theorem Th33:
  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 that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0;
A3: x0 in dom f1 & x0 in dom f2 by A1,A2;
  now
    x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
    hence
A4: x0 in dom (f1+f2) by VALUED_1:def 1;
    let s1;
    assume that
A5: rng s1 c= dom(f1+f2) and
A6: s1 is convergent & lim s1=x0;
A7: rng s1 c= dom f1 /\ dom f2 by A5,VALUED_1:def 1;
    dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
    then dom (f1+f2) c= dom f2 by XBOOLE_1:17;
    then
A8: rng s1 c= dom f2 by A5;
    then
A9: f2/*s1 is convergent by A2,A6;
    dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
    then dom (f1+f2) c= dom f1 by XBOOLE_1:17;
    then
A10: rng s1 c= dom f1 by A5;
    then
A11: f1/*s1 is convergent by A1,A6;
    then ((f1/*s1)+(f2/*s1)) is convergent by A9;
    hence (f1+f2)/*s1 is convergent by A7,Th7;
A12: f1/.x0 = lim (f1/*s1) by A1,A6,A10;
A13: f2/.x0 = lim (f2/*s1) by A2,A6,A8;
    thus (f1+f2)/.x0 = f1/.x0 + f2/.x0 by A4,CFUNCT_1:1
      .= lim ((f1/*s1) + (f2/*s1)) by A11,A12,A9,A13,COMSEQ_2:14
      .= lim ((f1+f2)/*s1) by A7,Th7;
  end;
  hence f1+f2 is_continuous_in x0;
  now
    x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
    hence
A14: x0 in dom (f1-f2) by CFUNCT_1:2;
    let s1;
    assume that
A15: rng s1 c= dom(f1-f2) and
A16: s1 is convergent & lim s1=x0;
A17: rng s1 c= dom f1 /\ dom f2 by A15,CFUNCT_1:2;
    dom (f1-f2) = dom f1 /\ dom f2 by CFUNCT_1:2;
    then dom (f1-f2) c= dom f2 by XBOOLE_1:17;
    then
A18: rng s1 c= dom f2 by A15;
    then
A19: f2/*s1 is convergent by A2,A16;
    dom (f1-f2) = dom f1 /\ dom f2 by CFUNCT_1:2;
    then dom (f1-f2) c= dom f1 by XBOOLE_1:17;
    then
A20: rng s1 c= dom f1 by A15;
    then
A21: f1/*s1 is convergent by A1,A16;
    then f1/*s1-f2/*s1 is convergent by A19;
    hence (f1-f2)/*s1 is convergent by A17,Th7;
A22: f1/.x0 = lim (f1/*s1) by A1,A16,A20;
A23: f2/.x0 = lim (f2/*s1) by A2,A16,A18;
    thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A14,CFUNCT_1:2
      .= lim (f1/*s1 - f2/*s1) by A21,A22,A19,A23,COMSEQ_2:26
      .= lim ((f1-f2)/*s1) by A17,Th7;
  end;
  hence f1-f2 is_continuous_in x0;
  x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
  hence
A24: x0 in dom (f1(#)f2) by VALUED_1:def 4;
  let s1;
  assume that
A25: rng s1 c= dom(f1(#)f2) and
A26: s1 is convergent & lim s1=x0;
  dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
  then dom (f1(#)f2) c= dom f2 by XBOOLE_1:17;
  then
A27: rng s1 c= dom f2 by A25;
  then
A28: f2/*s1 is convergent by A2,A26;
A29: rng s1 c= dom f1 /\ dom f2 by A25,VALUED_1:def 4;
  dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
  then dom (f1(#)f2) c= dom f1 by XBOOLE_1:17;
  then
A30: rng s1 c= dom f1 by A25;
  then
A31: f1/*s1 is convergent by A1,A26;
  then (f1/*s1)(#)(f2/*s1) is convergent by A28;
  hence (f1(#)f2)/*s1 is convergent by A29,Th7;
A32: f1/.x0 = lim (f1/*s1) by A1,A26,A30;
A33: f2/.x0 = lim (f2/*s1) by A2,A26,A27;
  thus (f1(#)f2)/.x0 = (f1/.x0) * (f2/.x0) by A24,CFUNCT_1:3
    .= lim ((f1/*s1)(#)(f2/*s1)) by A31,A32,A28,A33,COMSEQ_2:30
    .= lim ((f1(#)f2)/*s1) by A29,Th7;
end;

theorem Th34:
  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;
  hence
A2: x0 in dom (g(#)f) by VALUED_1:def 5;
  let s1;
  assume that
A3: rng s1 c= dom(g(#)f) and
A4: s1 is convergent & lim s1=x0;
A5: rng s1 c= dom f by A3,VALUED_1:def 5;
  then
A6: f/.x0 = lim (f/*s1) by A1,A4;
A7: f/*s1 is convergent by A1,A4,A5;
  then g(#)(f/*s1) is convergent;
  hence (g(#)f)/*s1 is convergent by A5,Th8;
  thus (g(#)f)/.x0 =g*(f/.x0) by A2,CFUNCT_1:4
    .= lim (g(#)(f/*s1)) by A7,A6,COMSEQ_2:18
    .= lim ((g(#)f)/*s1) by A5,Th8;
end;

theorem
  f is_continuous_in x0 implies -f is_continuous_in x0
by Th34;

theorem Th36:
  f is_continuous_in x0 & 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<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;
    hence X c= dom f;
A2: X c= dom f by A1;
    let x0,r;
    assume that
A3: x0 in X and
A4: 0<r;
    f|X is_continuous_in x0 by A1,A3;
    then consider s such that
A5: 0<s and
A6: for x1 st x1 in dom(f|X) & |.x1-x0.|<s holds |.(f|X)/.x1-(f|X)/.x0
    .| <r by A4,Th32;
    take s;
    thus 0<s by A5;
    let x1;
    assume that
A7: x1 in X and
A8: |.x1-x0.|<s;
A9: dom (f|X) = dom f /\ X by RELAT_1:61
      .= X by A2,XBOOLE_1:28;
    then |.f/.x1 - f/.x0.| = |.(f|X)/.x1 - f/.x0.| by A7,PARTFUN2:15
      .= |.(f|X)/.x1 - (f|X)/.x0.| by A3,A9,PARTFUN2:15;
    hence thesis by A6,A9,A7,A8;
  end;
  assume that
A10: X c= dom f and
A11: 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;
A12: dom (f|X) = dom f /\ X by RELAT_1:61
    .= X by A10,XBOOLE_1:28;
  now
    let x0 such that
A13: 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
A14:  0<s and
A15:  for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r by A11,A13;
      take s;
      thus 0<s by A14;
      let x1 such that
A16:  x1 in dom(f|X) and
A17:  |.x1-x0.|<s;
      |.(f|X)/.x1-(f|X)/.x0.| = |.(f|X)/.x1 - f/.x0.| by A12,A13,PARTFUN2:15
        .= |.f/.x1 - f/.x0.| by A16,PARTFUN2:15;
      hence thesis by A12,A15,A16,A17;
    end;
    hence f|X is_continuous_in x0 by A12,A13,Th32;
  end;
  hence thesis by A10;
end;

theorem Th40:
  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;
    then X c= dom f /\ X by XBOOLE_1:28;
    hence X c= dom (f|X) by RELAT_1:61;
    let g;
    assume g in X;
    then f|X is_continuous_in g by A1;
    hence thesis by RELAT_1:72;
  end;
  assume
A2: f|X is_continuous_on X;
  then X c= dom(f|X);
  then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
  hence X c= dom f;
  let g;
  assume g in X;
  then (f|X)|X is_continuous_in g by A2;
  hence thesis by RELAT_1:72;
end;

theorem Th41:
  f is_continuous_on X & X1 c= X implies f is_continuous_on X1
proof
  assume that
A1: f is_continuous_on X and
A2: X1 c= X;
  X c= dom f by A1;
  hence
A3: X1 c= dom f by A2;
  let g;
  assume
A4: g in X1;
  then
A5: f|X is_continuous_in g by A1,A2;
  thus f|X1 is_continuous_in g
  proof
    dom f /\ X1 c= dom f /\ X by A2,XBOOLE_1:26;
    then dom (f|X1) c= dom f /\ X by RELAT_1:61;
    then
A6: dom (f|X1) c= dom (f|X) by RELAT_1:61;
    g in dom f /\ X1 by A3,A4,XBOOLE_0:def 4;
    hence
A7: g in dom (f|X1) by RELAT_1:61;
    then
A8: (f|X)/.g = f/.g by A6,PARTFUN2:15
      .= (f|X1)/.g by A7,PARTFUN2:15;
    let s1 such that
A9: rng s1 c= dom (f|X1) and
A10: s1 is convergent & lim s1 = g;
A11: rng s1 c= dom (f|X) by A9,A6;
A12: now
      let n be Element of NAT;
A13:  s1.n in rng s1 by VALUED_0:28;
      thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A9,A6,FUNCT_2:109,XBOOLE_1:1
        .= f/.(s1.n) by A11,A13,PARTFUN2:15
        .= (f|X1)/.(s1.n) by A9,A13,PARTFUN2:15
        .= ((f|X1)/*s1).n by A9,FUNCT_2:109;
    end;
    (f|X)/*s1 is convergent & (f|X)/.g = lim ((f|X)/*s1) by A5,A10,A11;
    hence thesis by A8,A12,FUNCT_2:63;
  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
  by A1,TARSKI:def 1;
  let t such that
A2: t in {x0};
  thus f|{x0} is_continuous_in t
  proof
    t in dom f by A1,A2,TARSKI:def 1;
    then t in dom f /\ {x0} by A2,XBOOLE_0:def 4;
    hence t in dom (f|{x0}) by RELAT_1:61;
    let s1;
    assume that
A3: rng s1 c= dom(f|{x0}) and
    s1 is convergent and
    lim s1=t;
A4: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
    rng s1 c= dom f /\ {x0} by A3,RELAT_1:61;
    then
A5: rng s1 c= {x0} by A4;
A6: now
      let n;
      s1.n in rng s1 by VALUED_0:28;
      hence s1.n = x0 by A5,TARSKI:def 1;
    end;
A7: t=x0 by A2,TARSKI:def 1;
A8: now
      let r such that
A9:   0<r;
       reconsider n=0 as Nat;
      take n;
      let m such that
      n<=m;
A10:    m in NAT by ORDINAL1:def 12;
      |.((f|{x0})/*s1).m - (f|{x0})/.t.| = |.(f|{x0})/.(s1.m) - (f|{x0})
      /.x0.| by A7,A3,FUNCT_2:109,A10
        .= |.(f|{x0})/.x0 - (f|{x0})/.x0.| by A6
        .= 0 by COMPLEX1:44;
      hence |.((f|{x0})/*s1).m - (f|{x0})/.t.| < r by A9;
    end;
    hence (f|{x0})/*s1 is convergent;
    hence thesis by A8,COMSEQ_2:def 6;
  end;
end;

theorem Th43:
  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
A1: f1 is_continuous_on X & f2 is_continuous_on X;
  then X c= dom f1 & X c= dom f2;
  then
A2: X c= dom f1 /\ dom f2 by XBOOLE_1:19;
  then
A3: X c= dom (f1+f2) by CFUNCT_1:1;
  now
    let s1;
    assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f1/*s1 is convergent & f2/*s1 is convergent by A1,A4,A5,A6,Th38;
    then
A8: (f1/*s1)+(f2/*s1) is convergent;
A9: rng s1 c= dom f1 /\ dom f2 by A2,A4;
A10: lim s1 in dom (f1+f2) by A3,A6;
    f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A4,A5,A6
,Th38;
    then (f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A10,CFUNCT_1:1
      .= lim (f1/*s1 + f2/*s1) by A7,COMSEQ_2:14
      .= lim ((f1+f2)/*s1) by A9,Th7;
    hence
    (f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1) by A9,A8,Th7
;
  end;
  hence f1+f2 is_continuous_on X by A3,Th38;
A11: X c= dom (f1-f2) by A2,CFUNCT_1:2;
  now
    let s1;
    assume that
A12: rng s1 c= X and
A13: s1 is convergent and
A14: lim s1 in X;
A15: f1/*s1 is convergent & f2/*s1 is convergent by A1,A12,A13,A14,Th38;
    then
A16: (f1/*s1)-(f2/*s1) is convergent;
A17: rng s1 c= dom f1 /\ dom f2 by A2,A12;
A18: lim s1 in dom (f1-f2) by A11,A14;
    f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A12,A13,A14
,Th38;
    then (f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A18,CFUNCT_1:2
      .= lim (f1/*s1 - f2/*s1) by A15,COMSEQ_2:26
      .= lim ((f1-f2)/*s1) by A17,Th7;
    hence
    (f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1) by A17,A16
,Th7;
  end;
  hence f1-f2 is_continuous_on X by A11,Th38;
A19: X c= dom (f1(#)f2) by A2,CFUNCT_1:3;
  now
    let s1;
    assume that
A20: rng s1 c= X and
A21: s1 is convergent and
A22: lim s1 in X;
A23: f1/*s1 is convergent & f2/*s1 is convergent by A1,A20,A21,A22,Th38;
    then
A24: (f1/*s1)(#)(f2/*s1) is convergent;
A25: rng s1 c= dom f1 /\ dom f2 by A2,A20;
A26:  lim s1 in dom (f1(#)f2) by A19,A22;
    f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A20,A21,A22
,Th38;
    then (f1(#)f2)/.(lim s1) = lim (f1/*s1) * lim (f2/*s1) by A26,
CFUNCT_1:3
      .= lim ((f1/*s1) (#) (f2/*s1)) by A23,COMSEQ_2:30
      .= lim ((f1(#)f2)/*s1) by A25,Th7;
    hence (f1(#)f2)/*s1 is convergent & (f1(#)f2)/.(lim s1)=lim((f1(#)f2)/*s1)
    by A25,A24,Th7;
  end;
  hence thesis by A19,Th38;
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 f1 is_continuous_on X & f2 is_continuous_on X1;
  then f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 by Th41,
XBOOLE_1:17;
  hence thesis by Th43;
end;

theorem Th45:
  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;
  then
A3: X c= dom(g(#)f) by CFUNCT_1:4;
  now
    let s1;
    assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f/*s1 is convergent by A1,A4,A5,A6,Th38;
    then
A8: g(#)(f/*s1) is convergent;
A9: lim s1 in dom(g(#)f) by A3,A6;
    f/.(lim s1) = lim (f/*s1) by A1,A4,A5,A6,Th38;
    then (g(#)f)/.(lim s1) = g * lim (f/*s1) by CFUNCT_1:4,A9
      .= lim (g(#)(f/*s1)) by A7,COMSEQ_2:18
      .= lim ((g(#)f)/*s1) by A2,A4,Th8,XBOOLE_1:1;
    hence
    (g(#)f)/*s1 is convergent & (g(#)f)/.(lim s1)=lim((g(#)f)/*s1) by A2,A4,A8
,Th8,XBOOLE_1:1;
  end;
  hence thesis by A3,Th38;
end;

theorem
  f is_continuous_on X implies -f is_continuous_on X
by Th45;

theorem Th47:
  f is_continuous_on X & f"{0} = {} implies f^ is_continuous_on X
proof
  assume that
A1: f is_continuous_on X and
A2: f"{0} = {};
A3: dom(f^) = dom f \ {} by A2,CFUNCT_1:def 2
    .= dom f;
  hence
A4: X c= dom (f^) by A1;
  let g;
  assume
A5: g in X;
  then
A6: f|X is_continuous_in g by A1;
  g in dom(f^) /\ X by A4,A5,XBOOLE_0:def 4;
  then
A7: g in dom((f^)|X) by RELAT_1:61;
  now
    let s1;
    assume that
A8: rng s1 c= dom((f^)|X) and
A9: s1 is convergent & lim s1= g;
    rng s1 c= dom(f^) /\ X by A8,RELAT_1:61;
    then
A10: rng s1 c= dom(f|X) by A3,RELAT_1:61;
    then
A11: (f|X)/*s1 is convergent by A6,A9;
    now
      let n be Element of NAT;
A12:  s1.n in rng s1 by VALUED_0:28;
      rng s1 c= dom f /\ X & dom f /\ X c= dom f by A3,A8,RELAT_1:61
,XBOOLE_1:17;
      then
A13:  rng s1 c= dom f;
A14:  now
        assume f/.(s1.n)=0c;
        then f/.(s1.n) in {0c} by TARSKI:def 1;
        hence contradiction by A2,A13,A12,PARTFUN2:26;
      end;
      ((f|X)/*s1).n = (f|X)/.(s1.n) by A10,FUNCT_2:109
        .= f/.(s1.n) by A10,A12,PARTFUN2:15;
      hence ((f|X)/*s1).n <>0c by A14;
    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: 0<s and
A11: for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r by A5,A9,Th32;
    take s;
    thus s>0 by A10;
    let x2 such that
   x2 in COMPLEX and
A12: |.x2-x1.|<s;
A13: |.x2-y-x0.|=|.x2-x1.|;
A14: x2 - y in dom f by A4,XCMPLX_0:def 2;
    x1-x0+x0=x1;
    then |.f/.x2-f/.x1.| = |.f/.x2-(f/.y+f/.x0).| by A2
      .= |.f/.x2-f/.y-f/.x0.|
      .= |.f/.(x2-y)-f/.x0.| by A8;
    hence |.f/.x2-f/.x1.|<r by A11,A12,A13,A14;
  end;
  hence thesis by A4,Th39;
end;

definition
  let X;
  attr X is compact means

  for s1 st (rng s1) c= X ex s2 st s2 is
  subsequence of s1 & s2 is convergent & (lim s2) in X;
end;

theorem Th51:
  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[object,object] 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 VALUED_0:28;
      then consider g being Element of COMPLEX such that
A5:   g in dom f & s1.n=f.g by A3,PARTFUN1:3;
      take g;
      thus thesis by A5,PARTFUN1:def 6;
    end;
    consider q1 such that
A6: for n holds P[n,q1.n] from CompSeqChoice(A4);
    now
      let x be object;
      assume x in rng q1;
      then ex n being Element of NAT st x = q1.n by FUNCT_2:113;
      hence x in dom f by A6;
    end;
    then
A7: rng q1 c= dom f;
    then consider s2 such that
A8: s2 is subsequence of q1 and
A9: s2 is convergent and
A10: (lim s2) in dom f by A1;
    take q2 = f/*s2;
    rng s2 c= rng q1 by A8,VALUED_0:21;
    then
A11: rng s2 c= dom f by A7;
    now
      let n be Element of NAT;
      f/.(q1.n)=s1.n by A6;
      hence (f/*q1).n= s1.n by A7,FUNCT_2:109;
    end;
    then
A12: f/*q1=s1 by FUNCT_2:63;
    f|(dom f) is_continuous_in (lim s2) by A2,A10;
    then
A13: f is_continuous_in (lim s2) by RELAT_1:68;
    then f/.(lim s2) = lim (f/*s2) by A9,A11;
    then f.(lim s2) = lim (f/*s2) by A10,PARTFUN1:def 6;
    hence
    q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A7,A12,A8
,A9,A13,A11,FUNCT_1:def 3,VALUED_0:22;
  end;
  hence thesis;
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:61
    .= 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;
    hence thesis by RELAT_1:72;
  end;
  then rng (f|Y) is compact by A2,A4,Th51;
  hence thesis by RELAT_1:115;
end;