:: Monotone Real Sequences. Subsequences
::  by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990-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, XREAL_0, ORDINAL1, SEQ_1, ARYTM_3, NAT_1,
      CARD_1, FUNCT_1, XXREAL_0, PARTFUN1, ORDINAL2, RELAT_1, TARSKI, VALUED_0,
      FUNCT_3, ARYTM_1, VALUED_1, XXREAL_2, REAL_1, COMPLEX1, FINSEQ_1, SEQM_3,
      XBOOLE_0, FINSEQ_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_3, FINSEQ_1, FINSEQ_3, VALUED_1, SEQ_1,
      COMSEQ_2, SEQ_2,
      REAL_1, COMPLEX1, NAT_1, VALUED_0, XXREAL_0;
 constructors PARTFUN1, FUNCT_3, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1,
      VALUED_1, SEQ_1, SEQ_2, FINSEQ_1, RECDEF_1, RELSET_1, FINSEQ_3, COMSEQ_2;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
      XREAL_0, MEMBERED, VALUED_0, FUNCT_2, VALUED_1, SEQ_2, RFUNCT_1, RELAT_1,
      NAT_1, FINSEQ_1, CARD_1, COMSEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, SEQ_2, FUNCT_1, VALUED_0, VALUED_1;
 theorems FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, NAT_1, FUNCT_2, XREAL_1, XXREAL_0,
      ORDINAL1, VALUED_0, VALUED_1, RELAT_1, COMPLEX1, INT_1, FINSEQ_1,
      FINSEQ_3, XBOOLE_1, TARSKI;
 schemes NAT_1;

begin

reserve n,m,k for Element of NAT;
reserve r,r1 for real number;
reserve f,seq,seq1 for Real_Sequence;
reserve x,y for set;

Lm1: n<m implies ex k st m=n+1+k
proof
  assume
A1: n<m;
  then consider k1 be Nat such that
A2: m=n+k1 by NAT_1:10;
  k1 <> 0 by A1,A2;
  then consider n1 be Nat such that
A3: k1=n1+1 by NAT_1:6;
  reconsider n1 as Element of NAT by ORDINAL1:def 12;
  take n1;
  thus thesis by A2,A3;
end;

Lm2: ((for n holds seq.n<seq.(n+1)) implies for n,k holds seq.n<seq.(n+1+k)) &
((for n,k holds seq.n<seq.(n+1+k)) implies for n,m st n<m holds seq.n<seq.m) &
((for n,m st n<m holds seq.n<seq.m) implies for n holds seq.n<seq.(n+1))
proof
  thus (for n holds seq.n<seq.(n+1)) implies for n,k holds seq.n<seq.(n+1+k)
  proof
    assume
A1: for n holds seq.n<seq.(n+1);
    let n;
    defpred X[Element of NAT] means seq.n<seq.(n+1+$1);
A2: now
      let k such that
A3:   X[k];
      seq.(n+1+k)<seq.(n+1+k+1) by A1;
      hence X[k+1] by A3,XXREAL_0:2;
    end;
A4: X[0] by A1;
    thus for k holds X[k] from NAT_1:sch 1(A4,A2);
  end;
  thus (for n,k holds seq.n<seq.(n+1+k)) implies for n,m st n<m holds seq.n<
  seq.m
  proof
    assume
A5: for n,k holds seq.n<seq.(n+1+k);
    let n,m;
    assume n<m;
    then ex k st m=n+1+k by Lm1;
    hence thesis by A5;
  end;
  assume
A6: for n,m st n<m holds seq.n<seq.m;
  let n;
  n<n+1 by NAT_1:13;
  hence thesis by A6;
end;

Lm3: ((for n holds seq.(n+1)<seq.n) implies for n,k holds seq.(n+1+k)<seq.n) &
((for n,k holds seq.(n+1+k)<seq.n) implies for n,m st n<m holds seq.m<seq.n) &
((for n,m st n<m holds seq.m<seq.n) implies for n holds seq.(n+1)<seq.n)
proof
  thus (for n holds seq.(n+1)<seq.n) implies for n,k holds seq.(n+1+k)<seq.n
  proof
    assume
A1: for n holds seq.(n+1)<seq.n;
    let n;
    defpred X[Element of NAT] means seq.(n+1+$1)<seq.n;
A2: now
      let k such that
A3:   X[k];
      seq.(n+1+k+1)<seq.(n+1+k) by A1;
      hence X[k+1] by A3,XXREAL_0:2;
    end;
A4: X[0] by A1;
    thus for k holds X[k] from NAT_1:sch 1(A4,A2);
  end;
  thus (for n,k holds seq.(n+1+k)<seq.n) implies for n,m st n<m holds seq.m<
  seq.n
  proof
    assume
A5: for n,k holds seq.(n+1+k)<seq.n;
    let n,m;
    assume n<m;
    then ex k st m=n+1+k by Lm1;
    hence thesis by A5;
  end;
  assume
A6: for n,m st n<m holds seq.m<seq.n;
  let n;
  n<n+1 by NAT_1:13;
  hence thesis by A6;
end;

Lm4: ((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 st n<=m holds seq.n<=seq.m) &
((for n,m st n<=m holds seq.n<=seq.m) implies for n holds seq.n<=seq.(n+1))
proof
  thus (for n holds seq.n<=seq.(n+1)) implies for n,k holds seq.n<=seq.(n+k)
  proof
    assume
A1: for n holds seq.n<=seq.(n+1);
    let n;
    defpred X[Element of NAT] means seq.n<=seq.(n+$1);
A2: now
      let k such that
A3:   X[k];
      seq.(n+k)<=seq.(n+k+1) by A1;
      hence X[k+1] by A3,XXREAL_0:2;
    end;
A4: X[0];
    thus for k holds X[k] from NAT_1:sch 1(A4,A2);
  end;
  thus (for n,k holds seq.n<=seq.(n+k)) implies for n,m st n<=m holds seq.n<=
  seq.m
  proof
    assume
A5: for n,k holds seq.n<=seq.(n+k);
    let n,m;
    assume n<=m;
    then consider k1 be Nat such that
A6: m=n+k1 by NAT_1:10;
    k1 in NAT by ORDINAL1:def 12;
    hence thesis by A5,A6;
  end;
  assume
A7: for n,m st n<=m holds seq.n<=seq.m;
  let n;
  n<=n+1 by NAT_1:13;
  hence thesis by A7;
end;

Lm5: ((for n holds seq.(n+1)<=seq.n) implies for n,k holds seq.(n+k)<=seq.n) &
((for n,k holds seq.(n+k)<=seq.n) implies for n,m st n<=m holds seq.m<=seq.n) &
((for n,m st n<=m holds seq.m<=seq.n) implies for n holds seq.(n+1)<=seq.n)
proof
  thus (for n holds seq.(n+1)<=seq.n) implies for n,k holds seq.(n+k)<=seq.n
  proof
    assume
A1: for n holds seq.(n+1)<=seq.n;
    let n;
    defpred X[Element of NAT] means seq.(n+$1)<=seq.n;
A2: now
      let k such that
A3:   X[k];
      seq.(n+k+1)<=seq.(n+k) by A1;
      hence X[k+1] by A3,XXREAL_0:2;
    end;
A4: X[0];
    thus for k holds X[k] from NAT_1:sch 1(A4,A2);
  end;
  thus (for n,k holds seq.(n+k)<=seq.n) implies for n,m st n<=m holds seq.m<=
  seq.n
  proof
    assume
A5: for n,k holds seq.(n+k)<=seq.n;
    let n,m;
    assume n<=m;
    then consider k1 be Nat such that
A6: m=n+k1 by NAT_1:10;
    k1 in NAT by ORDINAL1:def 12;
    hence thesis by A5,A6;
  end;
  assume
A7: for n,m st n<=m holds seq.m<=seq.n;
  let n;
  n<=n+1 by NAT_1:13;
  hence thesis by A7;
end;

::
:: DEFINITIONS OF MONOTONE AND CONSTANT SEQUENCES
::

reserve e1,e2 for ext-real number;

definition
:::  let f be PartFunc of NAT, REAL;
  let f be NAT-defined REAL-valued Function;
  redefine attr f is increasing means
  :Def1:
  for m,n st m in dom f & n in dom f & m < n holds f.m < f.n;
  compatibility
  proof
    thus f is increasing implies for m,n st m in dom f & n in dom f & m < n
    holds f.m < f.n by VALUED_0:def 13;
    assume
A1: for m,n st m in dom f & n in dom f & m < n holds f.m < f.n;
    let e1,e2;
    dom f c= NAT by RELAT_1:def 18;
    hence thesis by A1;
  end;
  redefine attr f is decreasing means
  :Def2:
  for m,n st m in dom f & n in dom f & m < n holds f.m > f.n;
  compatibility
  proof
    thus f is decreasing implies for m,n st m in dom f & n in dom f & m < n
    holds f.m > f.n by VALUED_0:def 14;
    assume
A2: for m,n st m in dom f & n in dom f & m < n holds f.m > f.n;
    let e1,e2;
    dom f c= NAT by RELAT_1:def 18;
    hence thesis by A2;
  end;
  redefine attr f is non-decreasing means
  :Def3:
  for m,n st m in dom f & n in dom f & m <= n holds f.m <= f.n;
  compatibility
  proof
    thus f is non-decreasing implies for m,n st m in dom f & n in dom f & m <=
    n holds f.m <= f.n by VALUED_0:def 15;
    assume
A3: for m,n st m in dom f & n in dom f & m <= n holds f.m <= f.n;
    let e1,e2;
    dom f c= NAT by RELAT_1:def 18;
    hence thesis by A3;
  end;
  redefine attr f is non-increasing means
  :Def4:
  for m,n st m in dom f & n in dom f & m <= n holds f.m >= f.n;
  compatibility
  proof
    thus f is non-increasing implies for m,n st m in dom f & n in dom f & m <=
    n holds f.m >= f.n by VALUED_0:def 16;
    assume
A4: for m,n st m in dom f & n in dom f & m <= n holds f.m >= f.n;
    let e1,e2;
    dom f c= NAT by RELAT_1:def 18;
    hence thesis by A4;
  end;
end;

Lm6: f is increasing iff for n being Element of NAT holds f.n < f.(n+1)
proof
  thus f is increasing implies for n being Element of NAT holds f.n < f.(n+1 )
  proof
    assume
A1: f is increasing;
    let n be Element of NAT;
    dom f = NAT & n < n+1 by FUNCT_2:def 1,NAT_1:13;
    hence thesis by A1,Def1;
  end;
  assume
A2: for n being Element of NAT holds f.n < f.(n+1);
  let m,n;
  assume that
  m in dom f and
  n in dom f and
A3: m < n;
  ex k st n = m+1+k by A3,Lm1;
  hence thesis by A2,Lm2;
end;

Lm7: f is decreasing iff for n being Element of NAT holds f.n > f.(n+1)
proof
  thus f is decreasing implies for n being Element of NAT holds f.n > f.(n+1 )
  proof
    assume
A1: f is decreasing;
    let n be Element of NAT;
    dom f = NAT & n < n+1 by FUNCT_2:def 1,NAT_1:13;
    hence thesis by A1,Def2;
  end;
  assume
A2: for n being Element of NAT holds f.n > f.(n+1);
  let m,n;
  assume that
  m in dom f and
  n in dom f and
A3: m < n;
  ex k st n = m+1+k by A3,Lm1;
  hence thesis by A2,Lm3;
end;

Lm8: f is non-decreasing iff for n being Element of NAT holds f.n <= f.(n+1)
proof
  thus f is non-decreasing implies for n being Element of NAT holds f.n <= f.(
  n+1)
  proof
    assume
A1: f is non-decreasing;
    let n be Element of NAT;
    dom f = NAT & n < n+1 by FUNCT_2:def 1,NAT_1:13;
    hence thesis by A1,Def3;
  end;
  assume
A2: for n being Element of NAT holds f.n <= f.(n+1);
  let m,n;
  assume that
  m in dom f and
  n in dom f and
A3: m <= n;
  consider k be Nat such that
A4: n = m+k by A3,NAT_1:10;
  k in NAT by ORDINAL1:def 12;
  hence thesis by A2,A4,Lm4;
end;

Lm9: f is non-increasing iff for n being Element of NAT holds f.n >= f.(n+1)
proof
  thus f is non-increasing implies for n being Element of NAT holds f.n >= f.(
  n+1)
  proof
    assume
A1: f is non-increasing;
    let n be Element of NAT;
    dom f = NAT & n < n+1 by FUNCT_2:def 1,NAT_1:13;
    hence thesis by A1,Def4;
  end;
  assume
A2: for n being Element of NAT holds f.n >= f.(n+1);
  let m,n;
  assume that
  m in dom f and
  n in dom f and
A3: m <= n;
  consider k be Nat such that
A4: n = m+k by A3,NAT_1:10;
  k in NAT by ORDINAL1:def 12;
  hence thesis by A2,A4,Lm5;
end;

definition

  let seq;
  attr seq is monotone means
  :Def5:
  seq is non-decreasing or seq is non-increasing;
end;

theorem Th1:
  seq is increasing iff for n,m st n<m holds seq.n<seq.m
proof
  thus seq is increasing implies for n,m st n<m holds seq.n<seq.m
  proof
    assume seq is increasing;
    then for n holds seq.n<seq.(n+1) by Lm6;
    then for n,k holds seq.n<seq.(n+1+k) by Lm2;
    hence thesis by Lm2;
  end;
  assume
A1: for n,m st n<m holds seq.n<seq.m;
  let n,m;
  assume that
  n in dom seq and
  m in dom seq and
A2: n < m;
  thus thesis by A1,A2;
end;

theorem
  seq is increasing iff for n,k holds seq.n<seq.(n+1+k)
proof
  thus seq is increasing implies for n,k holds seq.n<seq.(n+1+k)
  proof
    assume seq is increasing;
    then for n holds seq.n<seq.(n+1) by Lm6;
    hence thesis by Lm2;
  end;
  assume for n,k holds seq.n<seq.(n+1+k);
  then for n,m st n<m holds seq.n<seq.m by Lm2;
  hence thesis by Th1;
end;

theorem Th3:
  seq is decreasing iff for n,k holds seq.(n+1+k)<seq.n
proof
  thus seq is decreasing implies for n,k holds seq.(n+1+k)<seq.n
  proof
    assume seq is decreasing;
    then for n holds seq.(n+1)<seq.n by Lm7;
    hence thesis by Lm3;
  end;
  assume
A1: for n,k holds seq.(n+1+k)<seq.n;
  let n,m;
  assume that
  n in dom seq and
  m in dom seq and
A2: n < m;
  thus thesis by A1,A2,Lm3;
end;

theorem Th4:
  seq is decreasing iff for n,m st n<m holds seq.m<seq.n
proof
  thus seq is decreasing implies for n,m st n<m holds seq.m<seq.n
  proof
    assume seq is decreasing;
    then for n,k holds seq.(n+1+k)<seq.n by Th3;
    hence thesis by Lm3;
  end;
  assume
A1: for n,m st n<m holds seq.m<seq.n;
  let n,m;
  assume that
  n in dom seq and
  m in dom seq and
A2: n < m;
  thus thesis by A1,A2;
end;

theorem Th5:
  seq is non-decreasing iff for n,k holds seq.n<=seq.(n+k)
proof
  thus seq is non-decreasing implies for n,k holds seq.n<=seq.(n+k)
  proof
    assume seq is non-decreasing;
    then for n holds seq.n<=seq.(n+1) by Lm8;
    hence thesis by Lm4;
  end;
  assume for n,k holds seq.n<=seq.(n+k);
  then for n holds seq.n<=seq.(n+1);
  hence thesis by Lm8;
end;

theorem Th6:
  seq is non-decreasing iff for n,m st n<=m holds seq.n<=seq.m
proof
  thus seq is non-decreasing implies for n,m st n<=m holds seq.n<=seq.m
  proof
    assume seq is non-decreasing;
    then for n,k holds seq.n<=seq.(n+k) by Th5;
    hence thesis by Lm4;
  end;
  assume
A1: for n,m st n<=m holds seq.n<=seq.m;
  let n,m;
  assume that
  n in dom seq and
  m in dom seq and
A2: n <= m;
  thus thesis by A1,A2;
end;

theorem Th7:
  seq is non-increasing iff for n,k holds seq.(n+k)<=seq.n
proof
  thus seq is non-increasing implies for n,k holds seq.(n+k)<=seq.n
  proof
    assume seq is non-increasing;
    then for n holds seq.(n+1)<=seq.n by Lm9;
    hence thesis by Lm5;
  end;
  assume for n,k holds seq.(n+k)<=seq.n;
  then for n holds seq.(n+1)<=seq.n;
  hence thesis by Lm9;
end;

theorem Th8:
  seq is non-increasing iff for n,m st n<=m holds seq.m<=seq.n
proof
  thus seq is non-increasing implies for n,m st n<=m holds seq.m<=seq.n
  proof
    assume seq is non-increasing;
    then for n,k holds seq.(n+k)<=seq.n by Th7;
    hence thesis by Lm5;
  end;
  assume
A1: for n,m st n<=m holds seq.m<=seq.n;
  let n,m;
  assume that
  n in dom seq and
  m in dom seq and
A2: n <= m;
  thus thesis by A1,A2;
end;

::
:: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES
::

theorem
  seq is increasing implies for n st 0<n holds seq.0<seq.n by Th1;

theorem
  seq is decreasing implies for n st 0<n holds seq.n<seq.0 by Th4;

theorem Th11:
  seq is non-decreasing implies for n holds seq.0<=seq.n by Th6;

theorem Th12:
  seq is non-increasing implies for n holds seq.n<=seq.0 by Th8;

registration
  cluster constant -> non-decreasing non-increasing for PartFunc of NAT, REAL;
  coherence
  proof
    let f be PartFunc of NAT, REAL such that
A1: f is constant;
    thus f is non-decreasing
    proof
      let m,n;
      assume that
A2:   m in dom f & n in dom f and
      m <= n;
      thus thesis by A1,A2,FUNCT_1:def 10;
    end;
    let m,n;
    assume that
A3: m in dom f & n in dom f and
    m <= n;
    thus thesis by A1,A3,FUNCT_1:def 10;
  end;
  cluster non-decreasing non-increasing -> constant for PartFunc of NAT, REAL;
  coherence
  proof
    let f be PartFunc of NAT, REAL such that
A4: f is non-decreasing non-increasing;
    let x,y;
    assume
A5: x in dom f & y in dom f;
    dom f c= NAT by RELAT_1:def 18;
    then reconsider m = x, n = y as Element of NAT by A5;
    m <= n or n <= m;
    then f.m <= f.n & f.n <= f.m by A4,A5,Def3,Def4;
    hence thesis by XXREAL_0:1;
  end;
end;

::  DEFINITIONS OF INCREASING SEQUENCE OF NATURAL NUMBERS,
::  RESTRICTION OF SEQUENCE.

Lm10: incl NAT is increasing natural-valued
proof
  set seq = incl NAT;
  now
    let n;
    seq.n=n & seq.(n+1)=n+1 by FUNCT_1:18;
    hence seq.n<seq.(n+1) by NAT_1:13;
  end;
  hence thesis by Lm6;
end;

Lm11: id NAT is increasing natural-valued;

registration
  cluster increasing natural-valued for Real_Sequence;
  existence by Lm10;
end;

registration
  cluster increasing for sequence of NAT;
  existence by Lm11;
end;

Lm12: for f being sequence of NAT holds f is increasing iff for n being
Element of NAT holds f.n < f.(n+1)
proof
  let f be sequence of NAT;
  reconsider f as Real_Sequence by FUNCT_2:7;
  f is increasing iff for n being Element of NAT holds f.n < f.(n+1) by Lm6;
  hence thesis;
end;

reserve Nseq for increasing sequence of NAT;

theorem
  seq is sequence of NAT iff for n holds seq.n is Element of NAT
proof
  thus seq is sequence of NAT implies for n holds seq.n is Element of NAT
  proof
    assume seq is sequence of NAT;
    then
A1: rng seq c= NAT by VALUED_0:def 6;
    let n;
    n in NAT;
    then n in dom seq by FUNCT_2:def 1;
    then seq.n in rng seq by FUNCT_1:def 3;
    hence thesis by A1;
  end;
  assume
A2: for n holds seq.n is Element of NAT;
  rng seq c= NAT
  proof
    let x be set;
    assume x in rng seq;
    then consider y such that
A3: y in dom seq and
A4: x = seq.y by FUNCT_1:def 3;
    reconsider y as Element of NAT by A3,FUNCT_2:def 1;
    x = seq.y by A4;
    then x is Element of NAT by A2;
    hence thesis;
  end;
  hence thesis by FUNCT_2:6;
end;

registration
  let Nseq,k;
  cluster Nseq ^\ k -> increasing natural-valued for ext-real-valued Function;
  coherence
  proof
    now
      let n;
      Nseq.(n+k)<Nseq.(n+k+1) by Lm12;
      then (Nseq ^\k).n<Nseq.(n+1+k) by NAT_1:def 3;
      hence (Nseq ^\k).n<(Nseq ^\k).(n+1) by NAT_1:def 3;
    end;
    hence thesis by Lm12;
  end;
end;

definition
  let f be Real_Sequence;
  redefine attr f is increasing means
  for n being Element of NAT holds f.n < f.(n+1);
  compatibility by Lm6;
  redefine attr f is decreasing means
  for n being Element of NAT holds f.n > f.(n+1);
  compatibility by Lm7;
  redefine attr f is non-decreasing means
  for n being Element of NAT holds f.n <= f.(n+1);
  compatibility by Lm8;
  redefine attr f is non-increasing means
  for n being Element of NAT holds f.n >= f.(n+1);
  compatibility by Lm9;
end;

theorem
  for n holds n<=Nseq.n
proof
  defpred X[Element of NAT] means $1<=Nseq.$1;
A1: now
    let k such that
A2: X[k];
    Nseq.k<Nseq.(k+1) by Lm12;
    then k<Nseq.(k+1) by A2,XXREAL_0:2;
    hence X[k+1] by NAT_1:13;
  end;
A3: X[0];
  thus for k holds X[k] from NAT_1:sch 1(A3,A1);
end;

registration
  let s be Real_Sequence, k be Nat;
  cluster s^\k ->real-valued;
  coherence;
end;

theorem Th15:
  (seq+seq1) ^\k=(seq ^\k) + (seq1 ^\k)
proof
  now
    let n;
    thus ((seq+seq1) ^\k).n=(seq+seq1).(n+k) by NAT_1:def 3
      .=seq.(n+k) + seq1.(n+k) by SEQ_1:7
      .=(seq ^\k).n +seq1.(n+k) by NAT_1:def 3
      .=(seq ^\k).n +(seq1 ^\k).n by NAT_1:def 3
      .=((seq ^\k) +(seq1 ^\k)).n by SEQ_1:7;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th16:
  (-seq) ^\k=-(seq ^\k)
proof
  now
    let n;
    thus ((-seq) ^\k).n=(-seq).(n+k) by NAT_1:def 3
      .=-(seq.(n+k)) by SEQ_1:10
      .=-((seq ^\ k).n) by NAT_1:def 3
      .=(-(seq ^\k)).n by SEQ_1:10;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (seq-seq1) ^\k=(seq ^\k)-(seq1 ^\k)
proof
  thus (seq-seq1) ^\k=(seq ^\k)+((-seq1) ^\k) by Th15
    .=(seq ^\k)-(seq1 ^\k) by Th16;
end;

theorem Th18:
  (seq") ^\k=(seq ^\k)"
proof
  now
    let n;
    thus ((seq") ^\k).n=(seq").(n+k) by NAT_1:def 3
      .=(seq.(n+k))" by VALUED_1:10
      .=((seq ^\k).n)" by NAT_1:def 3
      .=((seq ^\k)").n by VALUED_1:10;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th19:
  (seq(#)seq1) ^\k=(seq ^\k)(#)(seq1 ^\k)
proof
  now
    let n;
    thus ((seq(#)seq1) ^\k).n=(seq(#)seq1).(n+k) by NAT_1:def 3
      .=seq.(n+k)*seq1.(n+k) by SEQ_1:8
      .=(seq ^\k).n*seq1.(n+k) by NAT_1:def 3
      .=(seq ^\k).n*(seq1 ^\k).n by NAT_1:def 3
      .=((seq ^\k)(#)(seq1 ^\k)).n by SEQ_1:8;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (seq/"seq1) ^\k=(seq ^\k)/"(seq1 ^\k)
proof
  thus (seq/"seq1) ^\k=(seq ^\k)(#)((seq1") ^\k) by Th19
    .=(seq ^\k)/"(seq1 ^\k) by Th18;
end;

theorem
  (r(#)seq) ^\k=r(#)(seq ^\k)
proof
  now
    let n;
    thus ((r(#)seq) ^\k).n=(r(#)seq).(n+k) by NAT_1:def 3
      .=r*(seq.(n+k)) by SEQ_1:9
      .=r*((seq ^\k).n) by NAT_1:def 3
      .=(r(#)(seq ^\k)).n by SEQ_1:9;
  end;
  hence thesis by FUNCT_2:63;
end;

::
::  SUBSEQUENCES OF MONOTONE SEQUENCE
::    SUBSEQUENCE OF BOUNDED SEQUENCE
::

theorem
  seq is increasing & seq1 is subsequence of seq implies seq1 is increasing
proof
  assume that
A1: seq is increasing and
A2: seq1 is subsequence of seq;
  let n;
  consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
  Nseq.n<Nseq.(n+1) by Lm12;
  then (seq.(Nseq.n))<(seq.(Nseq.(n+1))) by A1,Th1;
  then (seq*Nseq).n<(seq.(Nseq.(n+1))) by FUNCT_2:15;
  hence thesis by A3,FUNCT_2:15;
end;

theorem
  seq is decreasing & seq1 is subsequence of seq implies seq1 is decreasing
proof
  assume that
A1: seq is decreasing and
A2: seq1 is subsequence of seq;
  let n;
  consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
  Nseq.n<Nseq.(n+1) by Lm12;
  then seq.(Nseq.(n+1))<seq.(Nseq.n) by A1,Th4;
  then (seq*Nseq).(n+1)<seq.(Nseq.n) by FUNCT_2:15;
  hence thesis by A3,FUNCT_2:15;
end;

theorem Th24:
  seq is non-decreasing & seq1 is subsequence of seq implies seq1
  is non-decreasing
proof
  assume that
A1: seq is non-decreasing and
A2: seq1 is subsequence of seq;
  let n;
  consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
  Nseq.n<=Nseq.(n+1) by Lm12;
  then (seq.(Nseq.n))<=(seq.(Nseq.(n+1))) by A1,Th6;
  then (seq*Nseq).n<=(seq.(Nseq.(n+1))) by FUNCT_2:15;
  hence thesis by A3,FUNCT_2:15;
end;

theorem Th25:
  seq is non-increasing & seq1 is subsequence of seq implies seq1
  is non-increasing
proof
  assume that
A1: seq is non-increasing and
A2: seq1 is subsequence of seq;
  let n;
  consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
  Nseq.n<=Nseq.(n+1) by Lm12;
  then (seq.(Nseq.(n+1)))<=(seq.(Nseq.n)) by A1,Th8;
  then (seq*Nseq).(n+1)<=(seq.(Nseq.n)) by FUNCT_2:15;
  hence thesis by A3,FUNCT_2:15;
end;

theorem
  seq is monotone & seq1 is subsequence of seq implies seq1 is monotone
proof
  assume that
A1: seq is monotone and
A2: seq1 is subsequence of seq;
A3: now
    assume seq is non-increasing;
    then seq1 is non-increasing by A2,Th25;
    hence thesis by Def5;
  end;
  now
    assume seq is non-decreasing;
    then seq1 is non-decreasing by A2,Th24;
    hence thesis by Def5;
  end;
  hence thesis by A1,A3,Def5;
end;

theorem Th27:
  seq is bounded_above & seq1 is subsequence of seq implies seq1
  is bounded_above
proof
  assume that
A1: seq is bounded_above and
A2: seq1 is subsequence of seq;
  consider r1 such that
A3: for n holds seq.n<r1 by A1,SEQ_2:def 3;
  consider Nseq such that
A4: seq1=seq*Nseq by A2,VALUED_0:def 17;
  take r=r1;
  let n be Element of NAT;
  seq1.n=seq.(Nseq.n) by A4,FUNCT_2:15;
  hence seq1.n<r by A3;
end;

theorem Th28:
  seq is bounded_below & seq1 is subsequence of seq implies seq1
  is bounded_below
proof
  assume that
A1: seq is bounded_below and
A2: seq1 is subsequence of seq;
  consider r1 such that
A3: for n holds r1<seq.n by A1,SEQ_2:def 4;
  consider Nseq such that
A4: seq1=seq*Nseq by A2,VALUED_0:def 17;
  take r=r1;
  let n be Element of NAT;
  seq1.n=seq.(Nseq.n) by A4,FUNCT_2:15;
  hence r<seq1.n by A3;
end;

theorem
  seq is bounded & seq1 is subsequence of seq implies seq1 is bounded
proof
  assume
A1: seq is bounded & seq1 is subsequence of seq;
  hence seq1 is bounded_above by Th27;
  thus thesis by A1,Th28;
end;

::
:: OPERATIONS ON MONOTONE SEQUENCES
::

theorem
  (seq is increasing & 0<r implies r(#)seq is increasing) & (0=r implies
r(#)seq is constant) & (seq is increasing & r<0 implies r(#)seq is decreasing)
proof
  thus seq is increasing & 0<r implies r(#)seq is increasing
  proof
    assume that
A1: seq is increasing and
A2: 0<r;
    let n;
    seq.n<seq.(n+1) by A1,Lm6;
    then r*seq.n<r*seq.(n+1) by A2,XREAL_1:68;
    then (r(#)seq).n<r*seq.(n+1) by SEQ_1:9;
    hence thesis by SEQ_1:9;
  end;
  thus 0=r implies r(#)seq is constant
  proof
    assume
A3: 0=r;
    now
      let n be Nat;
      n in NAT & r*seq.n=r*seq.(n+1) by A3,ORDINAL1:def 12;
      then (r(#)seq).n=r*seq.(n+1) by SEQ_1:9;
      hence (r(#)seq).n=(r(#)seq).(n+1) by SEQ_1:9;
    end;
    hence thesis by VALUED_0:25;
  end;
  assume that
A4: seq is increasing and
A5: r<0;
  let n;
  seq.n<seq.(n+1) by A4,Lm6;
  then r*seq.(n+1)<r*seq.n by A5,XREAL_1:69;
  then (r(#)seq).(n+1)<r*seq.n by SEQ_1:9;
  hence thesis by SEQ_1:9;
end;

theorem
  (seq is decreasing & 0<r implies r(#)seq is decreasing) & (seq is
  decreasing & r<0 implies r(#)seq is increasing)
proof
  thus seq is decreasing & 0<r implies r(#)seq is decreasing
  proof
    assume that
A1: seq is decreasing and
A2: 0<r;
    let n;
    seq.(n+1)<seq.n by A1,Lm7;
    then r*seq.(n+1)<r*seq.n by A2,XREAL_1:68;
    then (r(#)seq).(n+1)<r*seq.n by SEQ_1:9;
    hence thesis by SEQ_1:9;
  end;
  assume that
A3: seq is decreasing and
A4: r<0;
  let n;
  seq.(n+1)<seq.n by A3,Lm7;
  then r*seq.n<r*seq.(n+1) by A4,XREAL_1:69;
  then (r(#)seq).n<r*seq.(n+1) by SEQ_1:9;
  hence thesis by SEQ_1:9;
end;

theorem
  (seq is non-decreasing & 0<=r implies r(#)seq is non-decreasing) & (
  seq is non-decreasing & r<=0 implies r(#)seq is non-increasing)
proof
  thus seq is non-decreasing & 0<=r implies r(#)seq is non-decreasing
  proof
    assume that
A1: seq is non-decreasing and
A2: 0<=r;
    let n;
    seq.n<=seq.(n+1) by A1,Lm8;
    then r*seq.n<=r*seq.(n+1) by A2,XREAL_1:64;
    then (r(#)seq).n<=r*seq.(n+1) by SEQ_1:9;
    hence thesis by SEQ_1:9;
  end;
  assume that
A3: seq is non-decreasing and
A4: r<=0;
  let n;
  seq.n<=seq.(n+1) by A3,Lm8;
  then r*seq.(n+1)<=r*seq.n by A4,XREAL_1:65;
  then (r(#)seq).(n+1)<=r*seq.n by SEQ_1:9;
  hence thesis by SEQ_1:9;
end;

theorem
  (seq is non-increasing & 0<=r implies r(#)seq is non-increasing) & (
  seq is non-increasing & r<=0 implies r(#)seq is non-decreasing)
proof
  thus seq is non-increasing & 0<=r implies r(#)seq is non-increasing
  proof
    assume that
A1: seq is non-increasing and
A2: 0<=r;
    let n;
    seq.(n+1)<=seq.n by A1,Lm9;
    then r*seq.(n+1)<=r*seq.n by A2,XREAL_1:64;
    then (r(#)seq).(n+1)<=r*seq.n by SEQ_1:9;
    hence thesis by SEQ_1:9;
  end;
  assume that
A3: seq is non-increasing and
A4: r<=0;
  let n;
  seq.(n+1)<=seq.n by A3,Lm9;
  then r*seq.n<=r*seq.(n+1) by A4,XREAL_1:65;
  then (r(#)seq).n<=r*seq.(n+1) by SEQ_1:9;
  hence thesis by SEQ_1:9;
end;

theorem Th34:
  (seq is increasing & seq1 is increasing implies seq+seq1 is
  increasing) & (seq is decreasing & seq1 is decreasing implies seq+seq1 is
decreasing) & (seq is non-decreasing & seq1 is non-decreasing implies seq+seq1
  is non-decreasing) & (seq is non-increasing & seq1 is non-increasing implies
  seq+seq1 is non-increasing)
proof
  thus seq is increasing & seq1 is increasing implies seq+seq1 is increasing
  proof
    assume
A1: seq is increasing & seq1 is increasing;
    let n;
    seq.n<seq.(n+1) & seq1.n<seq1.(n+1) by A1,Lm6;
    then seq.n+seq1.n<seq.(n+1)+seq1.(n+1) by XREAL_1:8;
    then (seq+seq1).n<seq.(n+1)+seq1.(n+1) by SEQ_1:7;
    hence thesis by SEQ_1:7;
  end;
  thus seq is decreasing & seq1 is decreasing implies seq+seq1 is decreasing
  proof
    assume
A2: seq is decreasing & seq1 is decreasing;
    let n;
    seq.(n+1)<seq.n & seq1.(n+1)<seq1.n by A2,Lm7;
    then seq.(n+1)+seq1.(n+1)<seq.n+seq1.n by XREAL_1:8;
    then (seq+seq1).(n+1)<seq.n+seq1.n by SEQ_1:7;
    hence thesis by SEQ_1:7;
  end;
  thus seq is non-decreasing & seq1 is non-decreasing implies seq+seq1 is
  non-decreasing
  proof
    assume
A3: seq is non-decreasing & seq1 is non-decreasing;
    let n;
    seq.n<=seq.(n+1) & seq1.n<=seq1.(n+1) by A3,Lm8;
    then seq.n+seq1.n<=seq.(n+1)+seq1.(n+1) by XREAL_1:7;
    then (seq+seq1).n<=seq.(n+1)+seq1.(n+1) by SEQ_1:7;
    hence thesis by SEQ_1:7;
  end;
  assume
A4: seq is non-increasing & seq1 is non-increasing;
  let n;
  seq.(n+1)<=seq.n & seq1.(n+1)<=seq1.n by A4,Lm9;
  then seq.(n+1)+seq1.(n+1)<=seq.n+seq1.n by XREAL_1:7;
  then (seq+seq1).(n+1)<=seq.n+seq1.n by SEQ_1:7;
  hence thesis by SEQ_1:7;
end;

theorem
  (seq is increasing & seq1 is constant implies seq+seq1 is increasing)
& (seq is decreasing & seq1 is constant implies seq+seq1 is decreasing) & (seq
is non-decreasing & seq1 is constant implies seq+seq1 is non-decreasing) & (seq
  is non-increasing & seq1 is constant implies seq+seq1 is non-increasing)
proof
  thus seq is increasing & seq1 is constant implies seq+seq1 is increasing
  proof
    assume that
A1: seq is increasing and
A2: seq1 is constant;
    let n;
    consider r1 being Real such that
A3: for n being Nat holds seq1.n=r1 by A2,VALUED_0:def 18;
    seq.n<seq.(n+1) by A1,Lm6;
    then seq.n+r1<seq.(n+1)+r1 by XREAL_1:6;
    then seq.n+seq1.n<seq.(n+1)+r1 by A3;
    then seq.n+seq1.n<seq.(n+1)+seq1.(n+1) by A3;
    then (seq+seq1).n<seq.(n+1)+seq1.(n+1) by SEQ_1:7;
    hence thesis by SEQ_1:7;
  end;
  thus seq is decreasing & seq1 is constant implies seq+seq1 is decreasing
  proof
    assume that
A4: seq is decreasing and
A5: seq1 is constant;
    let n;
    consider r1 being Real such that
A6: for n being Nat holds seq1.n=r1 by A5,VALUED_0:def 18;
    seq.(n+1)<seq.n by A4,Lm7;
    then seq.(n+1)+r1<seq.n+r1 by XREAL_1:6;
    then seq.(n+1)+seq1.(n+1)<seq.n+r1 by A6;
    then seq.(n+1)+seq1.(n+1)<seq.n+seq1.n by A6;
    then (seq+seq1).(n+1)<seq.n+seq1.n by SEQ_1:7;
    hence thesis by SEQ_1:7;
  end;
  thus seq is non-decreasing & seq1 is constant implies seq+seq1 is
  non-decreasing by Th34;
  assume seq is non-increasing & seq1 is constant;
  hence thesis by Th34;
end;

::
:: OPERATIONS ON BOUNDED SEQUENCES
::

theorem Th36:
  (seq is bounded_above & 0<r implies r(#)seq is bounded_above) &
(0=r implies r(#)seq is bounded) & (seq is bounded_above & r<0 implies r(#)seq
  is bounded_below)
proof
  thus seq is bounded_above & 0<r implies r(#)seq is bounded_above;
  thus 0=r implies r(#)seq is bounded
  proof
    assume
A1: 0=r;
    now
      let n;
      (r(#)seq).n = 0*seq.n by A1,SEQ_1:9;
      hence (r(#)seq).n < 1;
    end;
    hence r(#)seq is bounded_above by SEQ_2:def 3;
    take p=-1;
    let n be Element of NAT;
    -1<0 & r*seq.n=0 by A1;
    hence p<(r(#)seq).n by SEQ_1:9;
  end;
  assume that
A2: seq is bounded_above and
A3: r<0;
  consider r1 such that
A4: for n holds seq.n<r1 by A2,SEQ_2:def 3;
  take p=r*abs r1;
  let n be Element of NAT;
  r1<=abs r1 by ABSVALUE:4;
  then seq.n<abs r1 by A4,XXREAL_0:2;
  then r*abs r1<r*seq.n by A3,XREAL_1:69;
  hence p<(r(#)seq).n by SEQ_1:9;
end;

theorem
  (seq is bounded implies for r holds r(#)seq is bounded) & (seq is
  bounded implies -seq is bounded) & (seq is bounded iff abs seq is bounded)
proof
  thus seq is bounded implies for r holds r(#)seq is bounded
  proof
    assume
A1: seq is bounded;
    let r;
    per cases;
    suppose
      0<r;
      hence thesis by A1;
    end;
    suppose
      0=r;
      hence thesis by Th36;
    end;
    suppose
      r<0;
      hence thesis by A1;
    end;
  end;
  thus seq is bounded implies -seq is bounded;
  thus seq is bounded implies abs seq is bounded;
  assume abs seq is bounded;
  then consider r be real number such that
A2: 0<r and
A3: for n be Element of NAT holds abs(abs seq.n)<r by SEQ_2:3;
  now
    let n be Element of NAT;
    abs(abs seq .n)=abs(abs(seq.n)) by SEQ_1:12
      .=abs(seq.n);
    hence abs(seq.n) < r by A3;
  end;
  hence thesis by A2,SEQ_2:3;
end;

::
:: OPERATIONS ON BOUNDED & MONOTONE SEQUENCES
::

theorem
  seq is bounded_above & seq1 is non-increasing implies seq+seq1 is
  bounded_above
proof
  assume that
A1: seq is bounded_above and
A2: seq1 is non-increasing;
  consider r1 such that
A3: for n holds seq.n<r1 by A1,SEQ_2:def 3;
  take r=r1+seq1.0;
  let n be Element of NAT;
  seq1.n<=seq1.0 by A2,Th12;
  then seq.n+seq1.n<r1+seq1.0 by A3,XREAL_1:8;
  hence (seq+seq1).n<r by SEQ_1:7;
end;

theorem
  seq is bounded_below & seq1 is non-decreasing implies seq+seq1 is
  bounded_below
proof
  assume that
A1: seq is bounded_below and
A2: seq1 is non-decreasing;
  consider r1 such that
A3: for n holds r1<seq.n by A1,SEQ_2:def 4;
  take r=r1+seq1.0;
  let n be Element of NAT;
  seq1.0<=seq1.n by A2,Th11;
  then r1+seq1.0<seq.n+seq1.n by A3,XREAL_1:8;
  hence r<(seq+seq1).n by SEQ_1:7;
end;

theorem
  incl NAT is increasing natural-valued by Lm10;

registration
  cluster -> natural-valued for FinSequence of NAT;
  coherence;
end;

begin :: moved from GOBOARD1, 2010.03.01, A.T.

reserve v for FinSequence of REAL,
  r,s for Real,
  n,m,i,j,k for Element of NAT;

theorem Th41:
  abs(r-s)=1 iff r>s & r=s+1 or r<s & s=r+1
proof
  thus abs(r-s)=1 implies r>s & r=s+1 or r<s & s=r+1
  proof
    assume
A1: abs(r-s) = 1;
    now
      per cases by XXREAL_0:1;
      case
A2:     r>s;
        then 0<r-s by XREAL_1:50;
        then r-s=1 by A1,ABSVALUE:def 1;
        hence thesis by A2;
      end;
      case
        r=s;
        hence contradiction by A1,ABSVALUE:2;
      end;
      case
A3:     r<s;
        then
A4:     0<s-r by XREAL_1:50;
        1=abs(-(r-s)) by A1,COMPLEX1:52
          .=s-r by A4,ABSVALUE:def 1;
        hence thesis by A3;
      end;
    end;
    hence thesis;
  end;
  assume
A5: r>s & r=s+1 or r<s & s=r+1;
  per cases by A5;
  suppose
    r>s & r=s+1;
    hence thesis by ABSVALUE:def 1;
  end;
  suppose
A6: s>r & s=r+1;
    thus abs(r-s)=abs(-(r-s)) by COMPLEX1:52
      .= 1 by A6,ABSVALUE:def 1;
  end;
end;

theorem
  abs(i-j)+abs(n-m)=1 iff abs(i-j)=1 & n=m or abs(n-m)=1 & i=j
proof
  thus abs(i-j)+abs(n-m)=1 implies abs(i-j)=1 & n=m or abs(n-m)=1 & i=j
  proof
    assume
A1: abs(i-j)+abs(n-m)=1;
    now
      per cases;
      suppose
A2:     n=m;
        then 1=abs(i-j)+0 by A1,ABSVALUE:2
          .= abs(i-j);
        hence thesis by A2;
      end;
      suppose
A3:     n<>m;
        now
          per cases by A3,XXREAL_0:1;
          suppose
A4:         n<m;
            then reconsider l=m-n as Element of NAT by INT_1:5;
            0<l by A4,XREAL_1:50;
            then
A5:         0+1<=l by NAT_1:13;
A6:         abs(-(m-n))=abs(l) by COMPLEX1:52;
            then
A7:         abs(n-m)=abs(l);
A8:         abs(l)=l by ABSVALUE:def 1;
            then
A9:         l<=1 by A1,A6,COMPLEX1:46,XREAL_1:31;
            then l=1 by A5,XXREAL_0:1;
            then i-j=0 by A1,A8,A7,ABSVALUE:2;
            hence thesis by A6,A5,A8,A9,XXREAL_0:1;
          end;
          suppose
A10:        n>m;
            then reconsider l=n-m as Element of NAT by INT_1:5;
            0<l by A10,XREAL_1:50;
            then
A11:        0+1<=l by NAT_1:13;
A12:        abs(n-m)=l by ABSVALUE:def 1;
            then
A13:        l<=1 by A1,COMPLEX1:46,XREAL_1:31;
            then l=1 by A11,XXREAL_0:1;
            then i-j=0 by A1,A12,ABSVALUE:2;
            hence thesis by A11,A12,A13,XXREAL_0:1;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  assume
A14: abs(i-j)=1 & n=m or abs(n-m)=1 & i=j;
  now
    per cases by A14;
    suppose
A15:  abs(i-j)=1 & n=m;
      then abs(n-m)=0 by ABSVALUE:2;
      hence thesis by A15;
    end;
    suppose
A16:  abs(n-m)=1 & i=j;
      then abs(i-j)=0 by ABSVALUE:2;
      hence thesis by A16;
    end;
  end;
  hence thesis;
end;

theorem
  n>1 iff ex m st n=m+1 & m>0
proof
  thus n>1 implies ex m st n=m+1 & m>0
  proof
    assume
A1: 1<n;
    then consider m being Nat such that
A2: n = m+1 by NAT_1:6;
    reconsider m as Element of NAT by ORDINAL1:def 12;
    take m;
    m <> 0 by A1,A2;
    hence thesis by A2;
  end;
  given m such that
A3: n=m+1 & m>0;
  0+1<n by A3,XREAL_1:6;
  hence thesis;
end;

theorem
  for f being FinSequence,n,m,k st len f = m+1 & n in dom f & k in
  Seg m holds Del(f,n).k = f.k or Del(f,n).k = f.(k+1)
proof
  let f be FinSequence,n,m,k such that
A1: len f = m+1 & n in dom f and
A2: k in Seg m;
  set X = dom f \ {n};
A3: dom f=Seg len f by FINSEQ_1:def 3;
  then
A4: n<=k & k<=m implies Sgm(X).k=k+1 by A1,A2,FINSEQ_3:108;
  X c= Seg len f by A3,XBOOLE_1:36;
  then rng Sgm(X) = X by FINSEQ_1:def 13;
  then
A5: dom (f*Sgm(X)) = dom Sgm(X) by RELAT_1:27,XBOOLE_1:36;
A6: dom Sgm(X)=Seg len Sgm(X) & Del(f,n) = f*Sgm(X) by FINSEQ_1:def 3
,FINSEQ_3:def 2;
A7: len Sgm(X) = m by A1,A3,FINSEQ_3:107;
  1<=k & k<n implies Sgm(X).k=k by A1,A2,A3,FINSEQ_3:108;
  hence thesis by A2,A6,A5,A7,A4,FINSEQ_3:25,FUNCT_1:12;
end;

definition
  let f be FinSequence;
  redefine attr f is constant means
  for n,m st n in dom f & m in dom f holds f.n=f.m;
  compatibility
  proof
    thus f is constant implies for n,m st n in dom f & m in dom f holds f.n=f.
    m by FUNCT_1:def 10;
    assume
A1: for n,m st n in dom f & m in dom f holds f.n=f.m;
    let n,m be set;
    assume n in dom f & m in dom f;
    hence thesis by A1;
  end;
end;

registration
  cluster -> real-valued for FinSequence of REAL;
  coherence;
end;

registration
  cluster non empty increasing for FinSequence of REAL;
  existence
  proof
    take v = <* 0 qua Real *>;
    thus v is non empty;
    let n,m;
    assume that
A1: n in dom v and
A2: m in dom v;
A3: dom<* 0 *> = { 1 } by FINSEQ_1:2,38;
    then n = 1 by A1,TARSKI:def 1;
    hence thesis by A3,A2,TARSKI:def 1;
  end;
end;

registration
  cluster constant for FinSequence of REAL;
  existence
  proof
    take v = <*>REAL;
    let n,m;
    assume that
 n in dom v and
    m in dom v;
    thus thesis;
  end;
end;

theorem Th45:
  v<>{} & rng v c= Seg n & v.(len v) = n & (for k st 1<=k & k<=len
v - 1 holds for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s) & i in
  Seg n & i+1 in Seg n & m in dom v & v.m = i & (for k st k in dom v & v.k = i
  holds k<=m) implies m+1 in dom v & v.(m+1)=i+1
proof
  assume that
A1: v<>{} and
A2: rng v c= Seg n and
A3: v.(len v) = n and
A4: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
  holds abs(r-s) = 1 or r=s and
A5: i in Seg n and
A6: i+1 in Seg n and
A7: m in dom v and
A8: v.m = i and
A9: for k st k in dom v & v.k = i holds k<=m;
A10: m<=len v by A7,FINSEQ_3:25;
  0+1<=len v by A1,NAT_1:13;
  then
A11: len v in dom v by FINSEQ_3:25;
  reconsider r=v.(m+1) as Real;
A12: i<=n by A5,FINSEQ_1:1;
A13: 1<=m by A7,FINSEQ_3:25;
A14: i+1<=n by A6,FINSEQ_1:1;
A15: now
    assume not m+1 in dom v;
    then 1>m+1 or m+1>len v by FINSEQ_3:25;
    then
A16: len v <=m by NAT_1:11,13;
    i<n by A14,NAT_1:13;
    hence contradiction by A3,A8,A10,A16,XXREAL_0:1;
  end;
  then
A17: m+1<=len v by FINSEQ_3:25;
  then
A18: m<len v by NAT_1:13;
A19: m<=len v - 1 by A17,XREAL_1:19;
  now
    per cases by A4,A8,A13,A19;
    case
A20:  abs(i - r) = 1;
      now
        per cases by A20,Th41;
        case
A21:      i>r & i=r+1;
          defpred P[set] means for k,r st k=$1 & k>0 & m+k in dom v & r=v.(m+k
          ) holds r<i;
A22:      for k st P[k] holds P[k+1]
          proof
            let k such that
A23:        P[k];
            let j,s such that
A24:        j=k+1 and
A25:        j>0 and
A26:        m+j in dom v and
A27:        s=v.(m+j);
            now
              per cases;
              suppose
                k=0;
                hence thesis by A21,A24,A27;
              end;
              suppose
A28:            k<>0;
A29:            m+k<=m+k+1 by NAT_1:11;
                m<=m+k by NAT_1:11;
                then
A30:            1<=m+k by A13,XXREAL_0:2;
A31:            m+(k+1)<=len v by A24,A26,FINSEQ_3:25;
                then m+k<=len v by A29,XXREAL_0:2;
                then
A32:            m+k in dom v by A30,FINSEQ_3:25;
                then v.(m+k) in rng v by FUNCT_1:def 3;
                then v.(m+k) in Seg n by A2;
                then reconsider r1=v.(m+k) as Element of NAT;
A33:            r1<i by A23,A28,A32;
A34:            m+k<=len v - 1 by A29,A31,XREAL_1:19;
                now
                  per cases by A4,A24,A27,A29,A30,A34;
                  suppose
A35:                abs(r1-s)=1;
                    now
                      per cases by A35,Th41;
                      suppose
                        r1>s & r1=s+1;
                        hence thesis by A33,XXREAL_0:2;
                      end;
                      suppose
                        r1<s & s=r1+1;
                        then
A36:                    s<=i by A33,NAT_1:13;
                        now
                          per cases by A36,XXREAL_0:1;
                          case
                            s<i;
                            hence thesis;
                          end;
                          case
                            s=i;
                            then m+j<=m by A9,A26,A27;
                            then j<=m-m by XREAL_1:19;
                            hence contradiction by A25;
                          end;
                        end;
                        hence thesis;
                      end;
                    end;
                    hence thesis;
                  end;
                  suppose
                    r1=s;
                    hence thesis by A23,A28,A32;
                  end;
                end;
                hence thesis;
              end;
            end;
            hence thesis;
          end;
          reconsider l = len v - m as Element of NAT by A18,INT_1:5;
A37:      0< len v - m & m+l = len v by A17,XREAL_1:19;
A38:      P[0];
          for k holds P[k] from NAT_1:sch 1(A38,A22);
          hence contradiction by A3,A11,A12,A37;
        end;
        case
          i<r & r=i+1;
          hence thesis by A15;
        end;
      end;
      hence thesis;
    end;
    case
      i=r;
      then m+1<=m by A9,A15;
      then 1<=m-m by XREAL_1:19;
      then 1<=0;
      hence contradiction;
    end;
  end;
  hence thesis;
end;

theorem
  v<>{} & rng v c= Seg n & v.1 = 1 & v.(len v) = n & (for k st 1<=k & k
  <=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s)
  implies (for i st i in Seg n ex k st k in dom v & v.k = i) & for m,k,i,r st m
  in dom v & v.m = i & (for j st j in dom v & v.j = i holds j<=m) & m<k & k in
  dom v & r = v.k
   holds i<r
proof
  assume that
A1: v<>{} and
A2: rng v c= Seg n and
A3: v.1 = 1 and
A4: v.(len v) = n and
A5: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
  holds abs(r-s) = 1 or r=s;
  defpred P[Element of NAT] means $1 in Seg n implies ex k st k in dom v & v.k
  = $1;
A6: 0+1<=len v by A1,NAT_1:13;
  then
A7: len v in dom v by FINSEQ_3:25;
A8: for i st P[i] holds P[i+1]
  proof
    let i such that
A9: i in Seg n implies ex k st k in dom v & v.k = i;
    assume
A10: i+1 in Seg n;
    now
      per cases;
      suppose
A11:    i = 0;
        take k=1;
        thus k in dom v & v.k = i+1 by A3,A6,A11,FINSEQ_3:25;
      end;
      suppose
A12:    i<>0;
        defpred R[set] means $1 in dom v & v.$1 = i;
A13:    for k be Nat holds R[k] implies k<=len v by FINSEQ_3:25;
        i+1<=n by A10,FINSEQ_1:1;
        then
A14:    i<=n by NAT_1:13;
A15:    0+1<=i by A12,NAT_1:13;
        then
A16:    ex k be Nat st R[k] by A9,A14,FINSEQ_1:1;
        consider m be Nat such that
A17:    R[m] & for k be Nat st R[k] holds k<=m from NAT_1:sch 6(A13,
        A16);
A18:    for k st R[k] holds k<=m by A17;
        reconsider m as Element of NAT by ORDINAL1:def 12;
        take k = m+1;
        i in Seg n by A15,A14,FINSEQ_1:1;
        hence k in dom v & v.k = i+1 by A1,A2,A4,A5,A10,A17,A18,Th45;
      end;
    end;
    hence thesis;
  end;
A19: P[0] by FINSEQ_1:1;
  thus for i holds P[i] from NAT_1:sch 1(A19,A8);
  let m,k,i,r;
  assume that
A20: m in dom v and
A21: v.m = i and
A22: for j st j in dom v & v.j = i holds j<=m and
A23: m<k and
A24: k in dom v and
A25: r = v.k;
A26: m<=len v & k<=len v by A20,A24,FINSEQ_3:25;
A27: 1<=m by A20,FINSEQ_3:25;
A28: i in rng v by A20,A21,FUNCT_1:def 3;
  then
A29: i<=n by A2,FINSEQ_1:1;
  now
    per cases;
    suppose
      i=n;
      then len v<=m by A4,A7,A22;
      hence thesis by A23,A26,XXREAL_0:1;
    end;
    suppose
A30:  i<>n;
      defpred P[set] means for j,s st j=$1 & j>0 & m+j in dom v & s=v.(m+j)
      holds i<s;
      i<n by A29,A30,XXREAL_0:1;
      then 1<=i+1 & i+1<=n by NAT_1:11,13;
      then i+1 in Seg n by FINSEQ_1:1;
      then
A31:  v.(m+1) = i+1 by A1,A2,A4,A5,A20,A21,A22,A28,Th45;
A32:  for k st P[k] holds P[k+1]
      proof
        let k such that
A33:    P[k];
        let j,s such that
A34:    j=k+1 and
A35:    j>0 and
A36:    m+j in dom v and
A37:    s=v.(m+j);
        per cases;
        suppose
          k=0;
          hence thesis by A31,A34,A37,NAT_1:13;
        end;
        suppose
A38:      k<>0;
          m<=m+k by NAT_1:11;
          then
A39:      1<=m+k by A27,XXREAL_0:2;
          s in rng v by A36,A37,FUNCT_1:def 3;
          then s in Seg n by A2;
          then reconsider s1=s as Element of NAT;
A40:      m+(k+1)<=len v by A34,A36,FINSEQ_3:25;
          m+k<=m+k+1 by NAT_1:11;
          then m+k<=len v by A40,XXREAL_0:2;
          then
A41:      m+k in dom v by A39,FINSEQ_3:25;
          then v.(m+k) in rng v by FUNCT_1:def 3;
          then v.(m+k) in Seg n by A2;
          then reconsider r1=v.(m+k) as Element of NAT;
A42:      i<r1 by A33,A38,A41;
A43:      m+k+1 = m+(k+1);
          then
A44:      m+k<= len v - 1 by A40,XREAL_1:19;
          now
            per cases by A5,A34,A37,A43,A39,A44;
            suppose
A45:          abs(r1-s)=1;
              now
                per cases by A45,Th41;
                suppose
                  r1>s & r1=s+1;
                  then
A46:              i<=s1 by A42,NAT_1:13;
                  now
                    per cases by A46,XXREAL_0:1;
                    case
                      i<s;
                      hence thesis;
                    end;
                    case
                      s=i;
                      then m+j<=m by A22,A36,A37;
                      then j<=m-m by XREAL_1:19;
                      hence contradiction by A35;
                    end;
                  end;
                  hence thesis;
                end;
                suppose
                  r1<s & s=r1+1;
                  hence thesis by A42,XXREAL_0:2;
                end;
              end;
              hence thesis;
            end;
            suppose
              r1=s;
              hence thesis by A33,A38,A41;
            end;
          end;
          hence thesis;
        end;
      end;
      reconsider l = k - m as Element of NAT by A23,INT_1:5;
A47:  0< k - m & m+l = k by A23,XREAL_1:50;
A48:  P[0];
      for k holds P[k] from NAT_1:sch 1(A48,A32);
      hence thesis by A24,A25,A47;
    end;
  end;
  hence thesis;
end;