:: Sequences in $R^n$
::  by Agnieszka Sakowicz , Jaros{\l}aw Gryko and Adam Grabowski
::
:: Received May 10, 1994
:: Copyright (c) 1994-2012 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, SEQ_1, NAT_1, EUCLID, REAL_1, PRE_TOPC,
      FUNCT_1, RELAT_1, VALUED_0, TARSKI, STRUCT_0, SUPINF_2, ARYTM_3, ARYTM_1,
      COMPLEX1, VALUED_1, CARD_1, XXREAL_0, XXREAL_2, SEQ_2, ORDINAL2,
      XBOOLE_0, PARTFUN1;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1, VALUED_1,
      PARTFUN1, COMPLEX1, REAL_1, PRE_TOPC, XXREAL_0, ORDINAL1, NAT_1, SEQ_1,
      STRUCT_0, RLVECT_1, VFUNCT_1, EUCLID;
 constructors REAL_1, COMPLEX1, MONOID_0, EUCLID, SEQ_1, RELSET_1, BINOP_2,
      VFUNCT_1;
 registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0,
      MONOID_0, EUCLID, XBOOLE_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, NAT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions FUNCT_2, STRUCT_0;
 theorems FUNCT_1, FUNCT_2, TARSKI, EUCLID, SEQ_1, NAT_1, XBOOLE_0, NORMSP_1,
      XCMPLX_0, XREAL_1, COMPLEX1, XXREAL_0, VFUNCT_1, ORDINAL1;
 schemes SEQ_1, NAT_1;

begin

definition
  let N be Nat;
  mode Real_Sequence of N is sequence of TOP-REAL N;
end;

reserve N,n,m,n1,n2 for Element of NAT;
reserve q,r,r1,r2 for Real;
reserve x,y for set;
reserve w,w1,w2,g,g1,g2 for Point of TOP-REAL N;
reserve seq,seq1,seq2,seq3,seq9 for Real_Sequence of N;

theorem Th1:
  for f being Function holds f is Real_Sequence of N iff (dom f=NAT
  & for n holds f.n is Point of TOP-REAL N)
proof
  let f be Function;
  thus f is Real_Sequence of N implies (dom f=NAT & for n holds f.n is Point
  of TOP-REAL N) by NORMSP_1:12;
  assume that
A1: dom f=NAT and
A2: for n holds f.n is Point of TOP-REAL N;
  for x holds x in NAT implies f.x is Point of TOP-REAL N by A2;
  hence thesis by A1,NORMSP_1:12;
end;

definition
  let N;
  let IT be Real_Sequence of N;
  attr IT is non-zero means
  :Def1:
  rng IT c= NonZero TOP-REAL N;
end;

theorem Th2:
  seq is non-zero iff for x st x in NAT holds seq.x<>0.TOP-REAL N
proof
  thus seq is non-zero implies for x st x in NAT holds seq.x<>0.TOP-REAL N
  proof
    assume seq is non-zero;
    then
A1: rng seq c= NonZero TOP-REAL N by Def1;
    let x;
    assume x in NAT;
    then x in dom seq by Th1;
    then seq.x in rng seq by FUNCT_1:def 3;
    then not seq.x in {0.TOP-REAL N} by A1,XBOOLE_0:def 5;
    hence thesis by TARSKI:def 1;
  end;
  assume
A2: for x st x in NAT holds seq.x<>0.TOP-REAL N;
  now
    let y;
    assume y in rng seq;
    then consider x such that
A3: x in dom seq and
A4: seq.x=y by FUNCT_1:def 3;
A5: x in NAT by A3,NORMSP_1:12;
    then y<>0.TOP-REAL N by A2,A4;
    then
A6: not y in {0.TOP-REAL N} by TARSKI:def 1;
    y is Point of TOP-REAL N by A4,A5,NORMSP_1:12;
    hence y in NonZero TOP-REAL N by A6,XBOOLE_0:def 5;
  end;
  then rng seq c= NonZero TOP-REAL N by TARSKI:def 3;
  hence thesis by Def1;
end;

theorem Th3:
  seq is non-zero iff for n holds seq.n<>0.TOP-REAL N
proof
  thus seq is non-zero implies for n holds seq.n<>0.TOP-REAL N by Th2;
  assume for n holds seq.n<>0.TOP-REAL N;
  then for x holds x in NAT implies seq.x<>0.TOP-REAL N;
  hence thesis by Th2;
end;

definition
  let N be Nat,seq1,seq2 be Real_Sequence of N;
  func seq1 + seq2 -> Real_Sequence of N equals
  seq1 + seq2;
  coherence
  proof
A1: dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1;
    dom (seq1+seq2) = dom seq1 /\ dom seq2 by VFUNCT_1:def 1;
    hence thesis by A1,FUNCT_2:67;
  end;
end;

definition
  let r;
  let N be Nat,seq be Real_Sequence of N;
  func r * seq -> Real_Sequence of N equals
  r(#)seq;
  coherence
  proof
A1: dom seq = NAT by FUNCT_2:def 1;
    dom (r(#)seq) = dom seq by VFUNCT_1:def 4;
    hence thesis by A1,FUNCT_2:67;
  end;
end;

definition
  let N be Nat,seq be Real_Sequence of N;
  func - seq -> Real_Sequence of N equals
  - seq;
  coherence
  proof
A1: dom seq = NAT by FUNCT_2:def 1;
    dom (-seq) = dom seq by VFUNCT_1:def 5;
    hence thesis by A1,FUNCT_2:67;
  end;
end;

definition
  let N be Nat,seq1,seq2 be Real_Sequence of N;
  func seq1 - seq2 -> Real_Sequence of N equals
  seq1 +- seq2;
  correctness;
end;

definition

  let N be Nat,seq be Real_Sequence of N;
  func |.seq.| -> Real_Sequence means
  :Def6:
  for n holds it.n = |.seq.n.|;
  existence
  proof
    deffunc U(Element of NAT) = |.seq.$1.|;
    thus ex s being Real_Sequence st for n holds s.n= U(n) from SEQ_1:sch 1;
  end;
  uniqueness
  proof
    let seq8,seq9 be Real_Sequence such that
A1: for n holds seq8.n=|.seq.n.| and
A2: for n holds seq9.n=|.seq.n.|;
    let n;
    seq9.n=|.seq.n.| by A2;
    hence seq8.n=seq9.n by A1;
  end;
end;

theorem Th4:
  for N,n be Nat,seq1,seq2 be Real_Sequence of N holds
  (seq1+seq2).n = seq1.n + seq2.n
  proof
    let N,n be Nat,seq1,seq2 be Real_Sequence of N;
    reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(seq1+seq2) = NAT by FUNCT_2:def 1;
    thus (seq1+seq2).n = (seq1+seq2)/.m
    .= seq1/.m + seq2/.m by A1,VFUNCT_1:def 1
    .= seq1.n + seq2.n;
  end;

theorem Th5:
  for N,n be Nat,seq be Real_Sequence of N holds
  (r*seq).n = r*seq.n
  proof
    let N,n be Nat,seq be Real_Sequence of N;
    reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(r*seq) = NAT by FUNCT_2:def 1;
    thus (r*seq).n = (r*seq)/.m
    .= r*seq/.m by A1,VFUNCT_1:def 4
    .= r*seq.n;
 end;

theorem Th6:
  for N,n be Nat,seq be Real_Sequence of N holds
  (-seq).n = -seq.n
  proof
    let N,n be Nat,seq be Real_Sequence of N;
    reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(-seq) = NAT by FUNCT_2:def 1;
    thus (-seq).n = (-seq)/.m
    .= -seq/.m by A1,VFUNCT_1:def 5
    .= -seq.n;
  end;

theorem Th7:
  abs(r)*|.w.| = |.r*w.| by EUCLID:11;

theorem
  |.r*seq.| = abs(r)(#)|.seq.|
proof
  let n;
  thus |.r*seq.|.n=|.(r*seq).n.| by Def6
    .=|.r*(seq.n).| by Th5
    .=abs(r)*|.seq.n.| by Th7
    .=abs(r)*(|.seq.|).n by Def6
    .=(abs(r)(#)|.seq.|).n by SEQ_1:9;
end;

theorem
  seq1 + seq2 = seq2 + seq1
proof
  let n;
  thus (seq1+seq2).n = seq1.n + seq2.n by Th4
    .= (seq2 + seq1).n by Th4;
end;

theorem Th10:
  (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof
  let n;
  thus ((seq1+seq2)+seq3).n = (seq1+seq2).n+ seq3.n by Th4
    .= seq1.n+seq2.n+seq3.n by Th4
    .=seq1.n+(seq2.n+seq3.n) by EUCLID:26
    .=seq1.n+(seq2+seq3).n by Th4
    .=(seq1+(seq2+seq3)).n by Th4;
end;

theorem Th11:
  -seq = (-1)*seq
proof
  let n;
  thus ((-1)*seq).n=(-1)*seq.n by Th5
    .=-seq.n by EUCLID:39
    .=(-seq).n by Th6;
end;

theorem Th12:
  r*(seq1 + seq2) = r*seq1 + r*seq2
proof
  let n;
  thus (r*(seq1 + seq2)).n=r*(seq1+seq2).n by Th5
    .=r*(seq1.n+seq2.n) by Th4
    .=r*seq1.n+r*seq2.n by EUCLID:32
    .=(r*seq1).n+r*seq2.n by Th5
    .=(r*seq1).n+(r*seq2).n by Th5
    .=((r*seq1)+(r*seq2)).n by Th4;
end;

theorem Th13:
  (r*q)*seq = r*(q*seq)
proof
  let n;
  thus ((r*q)*seq).n=(r*q)*seq.n by Th5
    .=r*(q*seq.n) by EUCLID:30
    .=r*(q*seq).n by Th5
    .=(r*(q*seq)).n by Th5;
end;

theorem Th14:
  r*(seq1 - seq2) = r*seq1 - r*seq2
proof
  thus r*(seq1-seq2)=r*seq1+r*(-seq2) by Th12
    .=r*seq1+r*((-1)*seq2) by Th11
    .=r*seq1+((-1)*r)*seq2 by Th13
    .=r*seq1+(-1)*(r*seq2) by Th13
    .=r*seq1-(r*seq2) by Th11;
end;

theorem
  seq1 - (seq2 + seq3) = seq1 - seq2 - seq3
proof
  thus seq1-(seq2+seq3)=seq1+(-1)*(seq2+seq3) by Th11
    .=seq1+((-1)*seq2+(-1)*seq3) by Th12
    .=seq1+(-seq2+(-1)*seq3) by Th11
    .=seq1+(-seq2+-seq3) by Th11
    .=seq1-seq2-seq3 by Th10;
end;

theorem Th16:
  1*seq=seq
proof
  let n;
  thus (1*seq).n=1*seq.n by Th5
    .=seq.n by EUCLID:29;
end;

theorem Th17:
  -(-seq) = seq
proof
  thus -(-seq)=(-1)*(-seq) by Th11
    .=(-1)*((-1)*seq) by Th11
    .=((-1)*(-1))*seq by Th13
    .=seq by Th16;
end;

theorem
  seq1 - (-seq2) = seq1 + seq2 by Th17;

theorem
  seq1 - (seq2 - seq3) = seq1 - seq2 + seq3
proof
  thus seq1-(seq2-seq3)=seq1+(-1)*(seq2-seq3) by Th11
    .=seq1+((-1)*seq2-((-1)*seq3)) by Th14
    .=seq1+(-seq2-((-1)*seq3)) by Th11
    .=seq1+(-seq2-(-seq3)) by Th11
    .=seq1+(-seq2+seq3) by Th17
    .=seq1-seq2+seq3 by Th10;
end;

theorem
  seq1 + (seq2 - seq3) = seq1 + seq2 - seq3 by Th10;

theorem Th21:
  r <> 0 & seq is non-zero implies r*seq is non-zero
proof
  assume that
A1: r<>0 and
A2: seq is non-zero and
A3: not r*seq is non-zero;
  consider n1 such that
A4: (r*seq).n1=0.TOP-REAL N by A3,Th3;
A5: seq.n1 <> 0.TOP-REAL N by A2,Th3;
  r*seq.n1=0.TOP-REAL N by A4,Th5;
  hence contradiction by A1,A5,EUCLID:31;
end;

theorem
  seq is non-zero implies -seq is non-zero
proof
  assume seq is non-zero;
  then (-1)*seq is non-zero by Th21;
  hence thesis by Th11;
end;

theorem Th23:
  |.0.TOP-REAL N.| = 0
proof
  thus |.0.TOP-REAL N.| = |.0*N.| by EUCLID:70
    .= 0 by EUCLID:7;
end;

theorem Th24:
  |.w.| = 0 implies w = 0.TOP-REAL N
proof
  reconsider s = w as Element of REAL N by EUCLID:22;
  assume |.w.| = 0;
  then s = 0*N by EUCLID:8
    .= 0.TOP-REAL N by EUCLID:70;
  hence thesis;
end;

theorem
  |.w.| >= 0;

theorem
  |.-w.| = |.w.| by EUCLID:71;

theorem Th27:
  |.w1 - w2.| = |.w2 - w1.|
proof
  thus |.w1 - w2.| = |.-(w1 - w2).| by EUCLID:71
    .= |.w2 - w1.| by EUCLID:44;
end;

Lm1: |.w1 - w2.| = 0 implies w1 = w2
proof
  assume |.w1 - w2.| = 0;
  then w1 - w2 = 0.TOP-REAL N by Th24;
  hence thesis by EUCLID:43;
end;

Lm2: w1 = w2 implies |.w1 - w2.| = 0
proof
  assume w1 = w2;
  then |.w1 - w2.| = |.0.TOP-REAL N.| by EUCLID:42
    .= 0 by Th23;
  hence thesis;
end;

theorem
  |.w1 - w2.| = 0 iff w1 = w2 by Lm1,Lm2;

theorem Th29:
  |.w1 + w2.| <= |.w1.| + |.w2.|
proof
  reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
  w1 + w2 = s1 + s2;
  hence thesis by EUCLID:12;
end;

theorem
  |.w1 - w2.| <= |.w1.| + |.w2.|
proof
  reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
  w1 - w2 = s1 - s2;
  hence thesis by EUCLID:13;
end;

theorem
  |.w1.| - |.w2.| <= |.w1 + w2.|
proof
  reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
  w1 + w2 = s1 + s2;
  hence thesis by EUCLID:14;
end;

theorem Th32:
  |.w1.| - |.w2.| <= |.w1 - w2.|
proof
  reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
  w1 - w2 = s1 - s2;
  hence thesis by EUCLID:15;
end;

theorem
  w1 <> w2 implies |.w1 - w2.| > 0
proof
  reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
  s1 - s2 = w1 - w2;
  hence thesis by EUCLID:17;
end;

theorem
  |.w1 - w2.| <= |.w1 - w.| + |.w - w2.|
proof
  0.TOP-REAL N = w - w by EUCLID:42
    .= -w + w by EUCLID:41;
  then |.w1 - w2.| = |.w1 + ((-w) + w) - w2.| by EUCLID:27
    .= |.w1 + (-w) + w - w2.| by EUCLID:26
    .= |.(w1 - w) + w - w2.| by EUCLID:41
    .= |.(w1 - w) + (w - w2).| by EUCLID:45;
  hence thesis by Th29;
end;

definition
  let N;
  let IT be Real_Sequence of N;
  attr IT is bounded means
  :Def7:
  ex r st for n holds |.IT.n.| < r;
end;

theorem Th35:
  for n ex r st (0<r & for m st m<=n holds |.seq.m.| < r)
proof
  defpred X[Element of NAT] means ex r1 st 0<r1 & for m st m<=$1 holds |.seq.m
  .|<r1;
A1: for n st X[n] holds X[n+1]
  proof
    let n;
    given r1 such that
A2: 0<r1 and
A3: for m st m<=n holds |.seq.m.|<r1;
A4: now
      assume
A5:   r1<=|.seq.(n+1).|;
      take r=|.seq.(n+1).|+1;
      thus 0<r;
      let m such that
A6:   m<=n+1;
A7:   now
        assume m<=n;
        then |.seq.m.|<r1 by A3;
        then |.seq.m.|<|.seq.(n+1).| by A5,XXREAL_0:2;
        then |.seq.m.|+0<r by XREAL_1:8;
        hence |.seq.m.|<r;
      end;
      now
        assume m=n+1;
        then |.seq.m.|+0<r by XREAL_1:8;
        hence |.seq.m.|<r;
      end;
      hence |.seq.m.|<r by A6,A7,NAT_1:8;
    end;
    now
      assume
A8:   |.seq.(n+1).|<=r1;
      take r=r1+1;
      thus 0<r by A2;
      let m such that
A9:   m<=n+1;
A10:  now
        assume m<=n;
        then
A11:    |.seq.m.|<r1 by A3;
        r1+0<r by XREAL_1:8;
        hence |.seq.m.|<r by A11,XXREAL_0:2;
      end;
      now
A12:    r1+0<r by XREAL_1:8;
        assume m=n+1;
        hence |.seq.m.|<r by A8,A12,XXREAL_0:2;
      end;
      hence |.seq.m.|<r by A9,A10,NAT_1:8;
    end;
    hence thesis by A4;
  end;
A13: X[0]
  proof
    take r=|.seq.0 .|+1;
    thus 0<r;
    let m;
    assume m<=0;
    then 0=m;
    then |.seq.m.|+0<r by XREAL_1:8;
    hence thesis;
  end;
  thus for n holds X[n] from NAT_1:sch 1(A13,A1);
end;

definition
  let N;
  let IT be Real_Sequence of N;
  attr IT is convergent means
  :Def8:
  ex g st for r st 0<r ex n st for m st n<= m holds |.IT.m-g.| < r;
end;

definition
  let N,seq;
  assume
A1: seq is convergent;
  func lim seq -> Point of TOP-REAL N means
  :Def9:
  for r st 0<r ex n st for m st n<=m holds |.seq.m-it.| < r;
  existence by A1,Def8;
  uniqueness
  proof
    given g1,g2 such that
A2: for r st 0<r ex n st for m st n<=m holds |.seq.m-g1.|<r and
A3: for r st 0<r ex n st for m st n<=m holds |.seq.m-g2.|<r and
A4: g1<>g2;
A5: now
      assume |.g1-g2.|=0;
      then 0.TOP-REAL N+g2=g1-g2+g2 by Th24;
      then g2=g1-g2+g2 by EUCLID:27
        .=g1-(g2-g2) by EUCLID:47
        .=g1-0.TOP-REAL N by EUCLID:42
        .=g1+ -0.TOP-REAL N by EUCLID:41
        .=g1+(-1)*0.TOP-REAL N by EUCLID:39
        .=g1+0.TOP-REAL N by EUCLID:28
        .=g1 by EUCLID:27;
      hence contradiction by A4;
    end;
    then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<|.g1-g2.|/4 by A2,XREAL_1:224;
    consider n2 such that
A7: for m st n2<=m holds |.seq.m-g2.|<|.g1-g2.|/4 by A3,A5,XREAL_1:224;
A8: |.seq.(n1+n2)-g2.|<|.g1-g2.|/4 by A7,NAT_1:12;
    |.seq.(n1+n2)-g1.|<|.g1-g2.|/4 by A6,NAT_1:12;
    then
A9: |.seq.(n1+n2)-g2.|+|.seq.(n1+n2)-g1.|<|.g1-g2.|/4+|.g1-g2.|/4 by A8,
XREAL_1:8;
    |.g1-g2.|=|.g1-g2+0.TOP-REAL N.| by EUCLID:27
      .=|.g1-g2+(-1)*0.TOP-REAL N.| by EUCLID:28
      .= |.g1-g2+-0.TOP-REAL N.| by EUCLID:39
      .= |.g1-g2-0.TOP-REAL N.| by EUCLID:41
      .=|.g1-g2-(seq.(n1+n2)-seq.(n1+n2)).| by EUCLID:42
      .=|.g1-g2-seq.(n1+n2)+seq.(n1+n2).| by EUCLID:47
      .=|.g1-(seq.(n1+n2)+g2)+seq.(n1+n2).| by EUCLID:46
      .=|.g1-seq.(n1+n2)-g2+seq.(n1+n2).| by EUCLID:46
      .=|.g1-seq.(n1+n2)-(g2-seq.(n1+n2)).| by EUCLID:47
      .=|.g1-seq.(n1+n2)+-(g2-seq.(n1+n2)).| by EUCLID:41
      .=|.g1-seq.(n1+n2)+(seq.(n1+n2)-g2).| by EUCLID:44
      .=|.-(seq.(n1+n2)-g1)+(seq.(n1+n2)-g2).| by EUCLID:44;
    then |.g1-g2.|<=|.-(seq.(n1+n2)-g1).|+|.seq.(n1+n2)-g2.| by Th29;
    then
A10: |.g1-g2.|<=|.seq.(n1+n2)-g1.|+|.seq.(n1+n2)-g2.| by EUCLID:71;
    |.g1-g2.|/2 <|.g1-g2.| by A5,XREAL_1:216;
    hence contradiction by A9,A10,XXREAL_0:2;
  end;
end;

theorem Th36:
  seq is convergent & seq9 is convergent implies seq + seq9 is convergent
proof
  assume that
A1: seq is convergent and
A2: seq9 is convergent;
  consider g1 such that
A3: for r st 0<r ex n st for m st n<=m holds |.seq.m-g1.|<r by A1,Def8;
  consider g2 such that
A4: for r st 0<r ex n st for m st n<=m holds |.seq9.m-g2.|<r by A2,Def8;
  take g=g1+g2;
  let r;
  assume
A5: 0<r;
  then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<r/2 by A3,XREAL_1:215;
  consider n2 such that
A7: for m st n2<=m holds |.seq9.m-g2.|<r/2 by A4,A5,XREAL_1:215;
  take k=n1+n2;
  let m;
  assume
A8: k<=m;
  n2<=k by NAT_1:12;
  then n2<=m by A8,XXREAL_0:2;
  then
A9: |.seq9.m-g2.|<r/2 by A7;
A10: |.(seq+seq9).m-g.|=|.seq.m+seq9.m-(g1+g2).| by Th4
    .=|.seq.m+(seq9.m-(g1+g2)).| by EUCLID:45
    .=|.seq.m+((-(g1+g2))+seq9.m).| by EUCLID:41
    .=|.seq.m+-(g1+g2)+seq9.m.| by EUCLID:26
    .=|.seq.m-(g1+g2)+seq9.m.| by EUCLID:41
    .=|.seq.m-g1-g2+seq9.m.| by EUCLID:46
    .=|.seq.m-g1+-g2+seq9.m.| by EUCLID:41
    .=|.seq.m-g1+(seq9.m+-g2).| by EUCLID:26
    .=|.seq.m-g1+(seq9.m-g2).| by EUCLID:41;
A11: |.seq.m-g1+(seq9.m-g2).|<=|.seq.m-g1.|+|.seq9.m-g2.| by Th29;
  n1<=n1+n2 by NAT_1:12;
  then n1<=m by A8,XXREAL_0:2;
  then |.seq.m-g1.|<r/2 by A6;
  then |.seq.m-g1.|+|.seq9.m-g2.|<r/2+r/2 by A9,XREAL_1:8;
  hence thesis by A10,A11,XXREAL_0:2;
end;

theorem Th37:
  seq is convergent & seq9 is convergent implies lim (seq + seq9)=
  (lim seq)+(lim seq9)
proof
  assume that
A1: seq is convergent and
A2: seq9 is convergent;
A3: now
    let r;
    assume 0<r;
    then
A4: 0<r/2 by XREAL_1:215;
    then consider n1 such that
A5: for m st n1<=m holds |.seq.m-lim (seq).|<r/2 by A1,Def9;
    consider n2 such that
A6: for m st n2<=m holds |.seq9.m-lim (seq9).|<r/2 by A2,A4,Def9;
    take k=n1+n2;
    let m such that
A7: k<=m;
    n2<=k by NAT_1:12;
    then n2<=m by A7,XXREAL_0:2;
    then
A8: |.seq9.m-(lim seq9).|<r/2 by A6;
A9: |.((seq+seq9).m)-((lim seq)+(lim seq9)).| =|.((seq+seq9).m)-(lim seq)
    -(lim seq9).| by EUCLID:46
      .=|.seq.m+seq9.m-(lim seq)-(lim seq9).| by Th4
      .=|.seq.m+(seq9.m-(lim seq))-(lim seq9).| by EUCLID:45
      .=|.seq.m+(-(lim seq)+seq9.m)-(lim seq9).| by EUCLID:41
      .=|.seq.m+-(lim seq)+seq9.m-(lim seq9).| by EUCLID:26
      .=|.seq.m-(lim seq)+seq9.m-(lim seq9).| by EUCLID:41
      .=|.seq.m-(lim seq)+(seq9.m-(lim seq9)).| by EUCLID:45;
A10: |.seq.m-(lim seq)+(seq9.m-(lim seq9)).|<= |.seq.m-(lim seq).|+|.seq9.
    m-(lim seq9).| by Th29;
    n1<=n1+n2 by NAT_1:12;
    then n1<=m by A7,XXREAL_0:2;
    then |.seq.m-lim(seq).|<r/2 by A5;
    then |.seq.m-(lim seq).|+|.seq9.m-(lim seq9).|<r/2+r/2 by A8,XREAL_1:8;
    hence |.((seq+seq9).m)-((lim seq)+(lim seq9)).|<r by A9,A10,XXREAL_0:2;
  end;
  seq+seq9 is convergent by A1,A2,Th36;
  hence thesis by A3,Def9;
end;

theorem Th38:
  seq is convergent implies r*seq is convergent
proof
  assume seq is convergent;
  then consider g1 such that
A1: for q st 0<q ex n st for m st n<=m holds |.seq.m-g1.|<q by Def8;
  set g=r*g1;
A2: now
A3: 0/abs(r)=0;
    assume
A4: r<>0;
    then
A5: 0<abs(r) by COMPLEX1:47;
    let q;
    assume 0<q;
    then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<q/abs(r) by A1,A5,A3,XREAL_1:74;
    take k=n1;
    let m;
    assume k<=m;
    then
A7: |.seq.m-g1.|<q/abs(r) by A6;
A8: 0<abs(r) by A4,COMPLEX1:47;
A9: abs(r)*(q/abs(r))=abs(r)*(abs(r)"*q) by XCMPLX_0:def 9
      .=abs(r)*abs(r)"*q
      .=1*q by A8,XCMPLX_0:def 7
      .=q;
    |.((r*seq).m)-g.|=|.r*seq.m-r*g1.| by Th5
      .=|.r*(seq.m-g1).| by EUCLID:49
      .=abs(r)*|.seq.m-g1.| by Th7;
    hence |.((r*seq).m)-g.|<q by A5,A7,A9,XREAL_1:68;
  end;
  now
    assume
A10: r=0;
    let q such that
A11: 0<q;
    take k=0;
    let m such that
    k<=m;
    |.((r*seq).m)-g.|=|.((0 *seq).m)-0.TOP-REAL N.| by A10,EUCLID:29
      .=|.0.TOP-REAL N-((0 * seq).m).| by Th27
      .=|.0.TOP-REAL N+-((0 * seq).m).| by EUCLID:41
      .=|.-((0 * seq).m).| by EUCLID:27
      .=|.(0 * seq).m.| by EUCLID:71
      .=|.0 * seq.m.| by Th5
      .=|.0.TOP-REAL N.| by EUCLID:29
      .=0 by Th23;
    hence |.((r*seq).m)-g.|<q by A11;
  end;
  hence thesis by A2,Def8;
end;

theorem Th39:
  seq is convergent implies lim(r*seq)=r*(lim seq)
proof
A1: now
    assume
A2: r=0;
    let q such that
A3: 0<q;
    take k=0;
    let m such that
    k<=m;
    r*(lim seq)=0.TOP-REAL N by A2,EUCLID:29;
    then |.((r*seq).m)-r*(lim seq).|=|.0 * seq.m-0.TOP-REAL N.| by A2,Th5
      .=|.0.TOP-REAL N-0 * seq.m.| by Th27
      .=|.0.TOP-REAL N+-0 * seq.m.| by EUCLID:41
      .=|.-0 * seq.m.| by EUCLID:27
      .=|.0 * seq.m.| by EUCLID:71
      .=|.0.TOP-REAL N.| by EUCLID:29
      .=0 by Th23;
    hence |.((r*seq).m)-r*(lim seq).|<q by A3;
  end;
  assume
A4: seq is convergent;
A5: now
A6: 0/abs(r)=0;
    assume
A7: r<>0;
    then
A8: 0<abs(r) by COMPLEX1:47;
    let q;
    assume 0<q;
    then 0<q/abs(r) by A8,A6,XREAL_1:74;
    then consider n1 such that
A9: for m st n1<=m holds |.seq.m-(lim seq).|<q/abs(r) by A4,Def9;
    take k=n1;
    let m;
    assume k<=m;
    then
A10: |.seq.m-(lim seq).|<q/abs(r) by A9;
A11: 0<>abs(r) by A7,COMPLEX1:47;
A12: abs(r)*(q/abs(r))=abs(r)*(abs(r)"*q) by XCMPLX_0:def 9
      .=abs(r)*abs(r)"*q
      .=1*q by A11,XCMPLX_0:def 7
      .=q;
    |.((r*seq).m)-r*(lim seq).|=|.r*seq.m-r*(lim seq).| by Th5
      .=|.r*(seq.m-(lim seq)).| by EUCLID:49
      .=abs(r)*|.seq.m-(lim seq).| by Th7;
    hence |.((r*seq).m)-r*(lim seq).|<q by A8,A10,A12,XREAL_1:68;
  end;
  r*seq is convergent by A4,Th38;
  hence thesis by A1,A5,Def9;
end;

theorem Th40:
  seq is convergent implies - seq is convergent
proof
  assume seq is convergent;
  then (-1)*seq is convergent by Th38;
  hence thesis by Th11;
end;

theorem Th41:
  seq is convergent implies lim(-seq)=-(lim seq)
proof
  assume seq is convergent;
  then lim ((-1)*seq)=(-1)*(lim seq) by Th39
    .=-(1*(lim seq)) by EUCLID:40
    .=-(lim seq) by EUCLID:29;
  hence thesis by Th11;
end;

theorem
  seq is convergent & seq9 is convergent implies seq - seq9 is convergent
proof
  assume that
A1: seq is convergent and
A2: seq9 is convergent;
  -seq9 is convergent by A2,Th40;
  hence thesis by A1,Th36;
end;

theorem
  seq is convergent & seq9 is convergent implies
  lim(seq - seq9) = (lim seq)-(lim seq9)
proof
  assume that
A1: seq is convergent and
A2: seq9 is convergent;
  - seq9 is convergent by A2,Th40;
  hence lim(seq - seq9)=(lim seq)+(lim(- seq9)) by A1,Th37
    .=(lim seq)+-(lim seq9) by A2,Th41
    .=(lim seq)-(lim seq9) by EUCLID:41;
end;

theorem
  seq is convergent implies seq is bounded
proof
  assume seq is convergent;
  then consider g such that
A1: for r st 0<r ex n st for m st n<=m holds |.seq.m-g.|<r by Def8;
  consider n1 such that
A2: for m st n1<=m holds |.seq.m-g.|<1 by A1;
A3: now
    take r=|.g.|+1;
    thus 0<r;
    let m;
A4: |.seq.m.|-|.g.|+|.g.|=|.seq.m.|;
    assume n1<=m;
    then
A5: |.seq.m-g.|<1 by A2;
    |.seq.m.|-|.g.|<=|.seq.m-g.| by Th32;
    then |.seq.m.|-|.g.|<1 by A5,XXREAL_0:2;
    hence |.seq.m.|<r by A4,XREAL_1:6;
  end;
  now
    consider r2 such that
A6: 0<r2 and
A7: for m st m<=n1 holds |.seq.m.|<r2 by Th35;
    consider r1 such that
A8: 0<r1 and
A9: for m st n1<=m holds |.seq.m.|<r1 by A3;
    take r=r1+r2;
    thus 0<r by A8,A6;
    let m;
A10: 0+r2<r by A8,XREAL_1:8;
A11: now
      assume m<=n1;
      then |.seq.m.|<r2 by A7;
      hence |.seq.m.|<r by A10,XXREAL_0:2;
    end;
A12: r1+0<r by A6,XREAL_1:8;
    now
      assume n1<=m;
      then |.seq.m.|<r1 by A9;
      hence |.seq.m.|<r by A12,XXREAL_0:2;
    end;
    hence |.seq.m.|<r by A11;
  end;
  hence thesis by Def7;
end;

theorem
  seq is convergent implies ((lim seq) <> 0.TOP-REAL N implies ex n st
  for m st n<=m holds |.(lim seq).|/2 < |.seq.m.|)
proof
  assume that
A1: seq is convergent and
A2: (lim seq)<>0.TOP-REAL N;
  0 <> |.(lim seq).| by A2,Th24;
  then 0<|.(lim seq).|/2 by XREAL_1:215;
  then consider n1 such that
A3: for m st n1<=m holds |.seq.m-(lim seq).|<|.(lim seq).|/2 by A1,Def9;
  take n=n1;
  let m;
  assume n<=m;
  then
A4: |.seq.m-(lim seq).|<|.(lim seq).|/2 by A3;
  |.(lim seq).|-|.seq.m.|<=|.(lim seq)-seq.m.| & |.(lim seq)-seq.m.|=|.seq
  .m-( lim seq).| by Th27,Th32;
  then
A5: |.(lim seq).|-|.seq.m.|<|.(lim seq).|/2 by A4,XXREAL_0:2;
  |.(lim seq).|/2+(|.seq.m.|-|.(lim seq).|/2) =|.seq.m.| & |.(lim seq).|-
  |.seq .m.|+(|.seq.m.|-|.(lim seq).|/2) =|.(lim seq).|/2;
  hence thesis by A5,XREAL_1:6;
end;