:: Segments of Natural Numbers and Finite Sequences
::  by Grzegorz Bancerek and Krzysztof Hryniewiecki
::
:: Received April 1, 1989
:: Copyright (c) 1990-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, NAT_1, FUNCT_1, SUBSET_1, XXREAL_0, TARSKI, XCMPLX_0,
      XBOOLE_0, CARD_1, ARYTM_3, RELAT_1, FINSET_1, ZFMISC_1, ORDINAL1,
      PARTFUN1, FUNCOP_1, ORDINAL4, ARYTM_1, FINSEQ_1, ORDINAL2, VALUED_0,
      FUNCT_2, UPROOTS;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1,
      FUNCOP_1, WELLORD2, ORDINAL1, NAT_1, CARD_1, NUMBERS, PARTFUN1, FINSET_1,
      XXREAL_0, FUNCT_2, INT_1, VALUED_0;
 constructors WELLORD2, FUNCOP_1, FUNCT_4, XXREAL_0, XREAL_0, NAT_1, CARD_1,
      RELSET_1, XCMPLX_0, INT_1, VALUED_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
      XXREAL_0, XREAL_0, NAT_1, CARD_1, NUMBERS, VALUED_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, FINSET_1, FUNCT_1, WELLORD2, XBOOLE_0, RELAT_1, CARD_1;
 equalities CARD_1, ORDINAL1;
 expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, CARD_1;
 theorems TARSKI, AXIOMS, FUNCT_1, NAT_1, ZFMISC_1, RELAT_1, RELSET_1,
      WELLORD2, ORDINAL1, CARD_1, FINSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1,
      XREAL_1, XXREAL_0, SETFAM_1, ORDINAL3, SUBSET_1, VALUED_0, XTUPLE_0,
      FUNCT_2, CARD_2, ENUMSET1, GRFUNC_1, XREAL_0, NUMBERS;
 schemes FUNCT_1, SUBSET_1, NAT_1, XBOOLE_0, RELAT_1, CLASSES1;

begin

reserve
  a for natural Number,
  k,l,m,n,k1,b,c,i for Nat,
  x,y,z,y1,y2 for object, X,Y for set,
  f,g for Function;

::   Segments of Natural Numbers

definition
  let n be natural Number;
  func Seg n -> set equals
  { k where k is Nat: 1 <= k & k <= n };
  correctness;
end;

definition
  let n be Nat;
  redefine func Seg n -> Subset of NAT;
  coherence
  proof
    set X = Seg n;
    X c= NAT
    proof
      let x be object;
      assume x in X;
      then ex k being Nat st x = k & 1 <= k & k <= n;
      hence thesis by ORDINAL1:def 12;
    end;
    hence thesis;
  end;
end;

theorem Th1:
  for a,b being natural Number holds a in Seg b iff 1 <= a & a <= b
proof
  let a,b be natural Number;
A1: a is Nat & b is Nat by TARSKI:1;
  a in { m where m is Nat: 1 <= m & m <= b } iff
  ex m being Nat st a = m & 1 <= m & m <= b;
  hence thesis by A1;
end;

registration let n be zero natural Number;
  cluster Seg n -> empty;
  coherence
   proof
    assume Seg n is not empty;
     then consider x being object such that
A1:    x in Seg n;
     ex k being Nat st k = x & 1 <= k & k <= 0 by A1;
    hence contradiction;
   end;
end;

theorem Th2:
  Seg 1 = { 1 } & Seg 2 = { 1,2 }
proof
  now
    let x be object;
    thus x in Seg 1 implies x in { 1 }
    proof
      assume x in Seg 1;
      then consider k being Nat such that
A1:   x = k and
A2:   1 <= k & k <= 1;
      k = 1 by A2,XXREAL_0:1;
      hence thesis by A1,TARSKI:def 1;
    end;
    assume x in { 1 };
    then x = 1 by TARSKI:def 1;
    hence x in Seg 1;
  end;
  hence Seg 1 = { 1 } by TARSKI:2;
  now
    let x be object;
    thus x in Seg 2 implies x in { 1,2 }
    proof
      assume x in Seg 2;
      then consider k being Nat such that
A3:   x = k and
A4:   1 <= k and
A5:   k <= 2;
      k <= 1 + 1 by A5;
      then k = 1 or k = 2 by A4,NAT_1:9;
      hence thesis by A3,TARSKI:def 2;
    end;
    assume x in { 1,2 };
    then x = 1 or x = 2 by TARSKI:def 2;
    hence x in Seg 2;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th3:
  for a being natural Number holds a = 0 or a in Seg a
proof
  let a be natural Number;
  assume a <> 0;
  then ex b be Nat st a = b + 1 by NAT_1:6;
  then a in NAT & 1 <= a by NAT_1:11;
  hence thesis;
end;

registration let n be non zero natural Number;
  cluster Seg n -> non empty;
  coherence by Th3;
end;

theorem
  for a being natural Number holds a+1 in Seg(a+1) by Th3;

theorem Th5:
  for a,b being natural Number holds a <= b iff Seg a c= Seg b
proof
  let a,b be natural Number;
  thus a <= b implies Seg a c= Seg b
  proof
    assume
A1: a <= b;
    let x be object;
    assume
 x in Seg a;
    then consider c being Nat such that
A3: x = c & 1 <= c & c <= a;
    c <= b by A1,A3,XXREAL_0:2;
    hence thesis by A3;
  end;
  assume
A4: Seg a c= Seg b;
  now
    assume a <> 0;
    then a in Seg a by Th3;
    hence thesis by A4,Th1;
  end;
  hence thesis;
end;

theorem Th6:
  for a,b being natural Number holds Seg a = Seg b implies a = b
proof
  let a,b be natural Number;
  assume Seg a = Seg b;
  then a <= b & b <= a by Th5;
  hence thesis by XXREAL_0:1;
end;

theorem Th7:
  for a,b,c being natural Number holds
  c <= a implies Seg c = Seg a /\ Seg c by Th5,XBOOLE_1:28;

theorem
  for a,c being natural Number holds
  Seg c = Seg c /\ Seg a implies c <= a by Th6,Th7;

theorem Th9:
  for a being natural Number holds Seg a \/ { a+1 } = Seg (a+1)
proof
  let a be natural Number;
  thus Seg a \/ { a+1 } c= Seg (a+1)
  proof
    a+0<=a+1 by XREAL_1:7;
    then
A1: Seg a c= Seg(a+1) by Th5;
    let x be object;
    assume x in Seg a \/ { a+1 };
    then x in Seg a or x in { a+1 } by XBOOLE_0:def 3;
    then x in Seg (a+1) or x = a+1 by A1,TARSKI:def 1;
    hence thesis by Th3;
  end;
  let x be object;
  assume
A2: x in Seg (a+1);
  then reconsider x as Element of NAT;
A3: x<=a+1 by A2,Th1;
A4: 1<=x by A2,Th1;
  x<=a or x=a+1 by A3,NAT_1:8;
  then x in Seg a or x in {a+1} by A4,TARSKI:def 1;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  for k being natural Number holds Seg k = Seg(k + 1) \ {k + 1}
proof
  let k be natural Number;
A1: Seg(k + 1) = Seg k \/ {k + 1} by Th9;
  Seg k misses {k + 1}
  proof
    assume not thesis;
    then
A2: Seg k /\ {k + 1} <> {};
    set x = the Element of Seg k /\ {k + 1};
A3: x in Seg k by A2,XBOOLE_0:def 4;
    x in {k + 1} by A2,XBOOLE_0:def 4;
    then x = k + 1 by TARSKI:def 1;
    hence thesis by A3,Th1,XREAL_1:29;
  end;
  hence thesis by A1,XBOOLE_1:88;
end;

::  Finite Sequences

definition
  let IT be Relation;
  attr IT is FinSequence-like means
  :Def2:
  ex n st dom IT = Seg n;
end;

registration
  cluster empty -> FinSequence-like for Relation;
  coherence
  proof
    let R be Relation;
    assume
A1: R is empty;
    take 0;
    thus thesis by A1;
  end;
end;

definition
  mode FinSequence is FinSequence-like Function;
end;

reserve p,q,r,s,t for FinSequence;

defpred P[object,object] means ex k st $1 = k & $2 = k+1;

registration
  let n be natural Number;
  cluster Seg n -> finite;
  coherence
  proof
    reconsider n as Nat by TARSKI:1;
    Seg n is finite
    proof
A1:   n = { k where k is Nat: k < n } by AXIOMS:4;
A2:   for x being object st x in n ex y being object st P[x,y]
      proof
        let x be object;
        assume x in n;
        then ex k being Nat st x = k & k < n by A1;
        then reconsider k = x as Nat;
        take k+1;
        thus thesis;
      end;
      consider f such that
A3:   dom f = n and
A4:   for x being object st x in n holds P[x,f.x] from CLASSES1:sch 1(A2);
      take f;
      thus rng f = Seg n
      proof
        thus rng f c= Seg n
        proof
          let x be object;
          assume x in rng f;
          then consider y being object such that
A5:       y in dom f and
A6:       x = f.y by FUNCT_1:def 3;
          consider k such that
A7:       y = k and
A8:       x = k+1 by A3,A4,A5,A6;
          ex m being Nat st m = y & m < n by A1,A3,A5;
          then 1 <= k+1 & k+1 <= n by A7,NAT_1:11,13;
          hence thesis by A8;
        end;
        let x be object;
        assume x in Seg n;
        then consider k being Nat such that
A9:     x = k and
A10:    1 <= k and
A11:    k <= n;
        consider i being Nat such that
A12:    1+i = k by A10,NAT_1:10;
        i in NAT & i < n by A11,A12,NAT_1:13,ORDINAL1:def 12;
        then
A13:    i in n by A1;
        then P[i,f.i] by A4;
        hence thesis by A3,A9,A12,A13,FUNCT_1:def 3;
      end;
      thus thesis by A3,ORDINAL1:def 12;
    end;
    hence thesis;
  end;
end;

registration
  cluster FinSequence-like -> finite for Function;
  coherence
  proof
    let f be Function;
    given n such that
A1: dom f = Seg n;
    rng f is finite by A1,FINSET_1:8;
    then [:dom f, rng f:] is finite by A1;
    hence thesis by FINSET_1:1,RELAT_1:7;
  end;
end;

Lm1: Seg n,n are_equipotent
proof
  defpred P[Nat] means Seg $1,$1 are_equipotent;
A1: P[0];
A2: for n st P[n] holds P[n+1]
  proof
    let n such that
A3: Seg n,n are_equipotent;
A4: Segm(n+1) = succ Segm n by NAT_1:38
      .= n \/ { n };
    A5: Seg(n+1) = Seg n \/ { n+1 } & { n+1 },{ n } are_equipotent by Th9,
CARD_1:28;
A6: now
      assume n meets { n };
      then consider x being object such that
A7:   x in n and
A8:   x in { n } by XBOOLE_0:3;
A:    x = n by A8,TARSKI:def 1;
      reconsider xx = x as set by TARSKI:1;
      not xx in xx;
      hence contradiction by A7,A;
    end;
    now
      assume Seg n meets { n+1 };
      then consider x being object such that
A9:   x in Seg n and
A10:  x in { n+1 } by XBOOLE_0:3;
A11:  x = n+1 by A10,TARSKI:def 1;
      not n+1 <= n by NAT_1:13;
      hence contradiction by A9,A11,Th1;
    end;
    hence thesis by A3,A4,A5,A6,CARD_1:31;
  end;
  for n holds P[n] from NAT_1:sch 2(A1,A2);
  hence thesis;
end;

registration let n be natural Number;
  cluster Seg n -> n-element;
  coherence
  proof
    n is Nat by TARSKI:1;
    hence thesis by Lm1,CARD_1:def 2;
  end;
end;

notation
  let p;
  synonym len p for card p;
end;

definition
  let p;
  redefine func len p -> Element of NAT means
  :Def3:
  Seg it = dom p;
  coherence
  proof card p = card p;
    hence thesis;
  end;
  compatibility
  proof
    let k be Element of NAT;
    consider n such that
A1: dom p = Seg n by Def2;
    dom p,p are_equipotent
    proof
      deffunc F(object) = [$1,p.$1];
      consider g being Function such that
A2:   dom g = dom p and
A3:   for x being object st x in dom p holds g.x = F(x) from FUNCT_1:sch 3;
      take g;
      thus g is one-to-one
      proof
        let x,y be object;
        assume that
A4:     x in dom g and
A5:     y in dom g;
        assume g.x = g.y;
        then [x,p.x] = g.y by A2,A3,A4
          .= [y,p.y] by A2,A3,A5;
        hence thesis by XTUPLE_0:1;
      end;
      thus dom g = dom p by A2;
      thus rng g c= p
      proof
        let i be object;
        assume i in rng g;
        then consider x being object such that
A6:     x in dom g and
A7:     g.x = i by FUNCT_1:def 3;
        g.x = [x,p.x] by A2,A3,A6;
        hence thesis by A2,A6,A7,FUNCT_1:1;
      end;
      let x,y be object;
      assume
A8:   [x,y] in p;
      then
A9:   x in dom p by FUNCT_1:1;
      y = p.x by A8,FUNCT_1:1;
      then g.x = [x,y] by A3,A8,FUNCT_1:1;
      hence thesis by A2,A9,FUNCT_1:def 3;
    end;
    then
A10: card p = card dom p by CARD_1:5;
    thus k = card p implies Seg k = dom p by A1,A10,Lm1,CARD_1:def 2;
    assume Seg k = dom p;
    hence k = card p by A10,Lm1,CARD_1:def 2;
  end;
end;

definition
  let p;
  redefine func dom p -> Subset of NAT;
  coherence
  proof dom p = Seg len p by Def3;
    hence thesis;
  end;
end;

theorem
  (ex k st dom f c= Seg k) implies ex p st f c= p
proof
  given k such that
A1: dom f c= Seg k;
  deffunc F(object) = f.$1;
  consider g such that
A2: dom g = Seg k &
for x being object st x in Seg k holds g.x = F(x) from FUNCT_1:sch 3;
  reconsider g as FinSequence by A2,Def2;
  take g;
  let y,z be object;
  assume
A3: [y,z] in f;
  then
A4: y in dom f by XTUPLE_0:def 12;
  reconsider z as set by TARSKI:1;
A5: f.y = z by A3,FUNCT_1:def 2,A4;
  [y,g.y] in g by A1,A2,A4,FUNCT_1:1;
  hence thesis by A1,A2,A4,A5;
end;

scheme SeqEx{A()->Nat,P[object,object]}:
  ex p st dom p = Seg A() & for k st k in Seg A() holds P[k,p.k]
provided
A1: for k st k in Seg A() ex x st P[k,x]
proof
A2: for x being object st x in Seg A() ex y being object st P[x,y]
  by A1;
  consider f being Function such that
A3: dom f = Seg A() &
  for x being object st x in Seg A() holds P[x,f.x] from CLASSES1:sch 1(A2);
  reconsider p=f as FinSequence by A3,Def2;
  take p;
  thus thesis by A3;
end;

scheme SeqLambda{A()->Nat,F(object) -> object}:
  ex p being FinSequence st len p = A() & for k st k in dom p holds p.k=F(k)
proof
  consider f being Function such that
  A1: dom
 f = Seg A() &
for x being object st x in Seg A() holds f.x=F(x) from FUNCT_1:sch 3;
A2: A() in NAT by ORDINAL1:def 12;
  reconsider p=f as FinSequence by A1,Def2;
  take p;
  thus thesis by A1,A2,Def3;
end;

theorem
  z in p implies ex k st k in dom p & z=[k,p.k]
proof
  assume
A1: z in p;
  then consider x,y being object such that
A2: z=[x,y] by RELAT_1:def 1;
  x in dom p by A1,A2,FUNCT_1:1;
  then reconsider k = x as Nat;
  take k;
  thus thesis by A1,A2,FUNCT_1:1;
end;

theorem
  dom p = dom q & (for k st k in dom p holds p.k = q.k) implies p=q;

theorem Th14:
  len p = len q & (for k st 1 <= k & k <= len p holds p.k = q.k) implies p=q
proof
  assume that
A1: len p = len q and
A2: for k st 1<=k & k<=len p holds p.k = q.k;
A3: dom p = Seg len p by Def3;
A4: dom q = Seg len q by Def3;
  now
    let x be object;
    assume
A5: x in dom p;
    then reconsider k=x as Nat;
    1 <= k & k <= len p by A3,A5,Th1;
    hence p.x = q.x by A2;
  end;
  hence thesis by A1,A3,A4;
end;

theorem Th15:
  p|(Seg a) is FinSequence
proof
A0: a is Nat by TARSKI:1;
A1: dom(p|Seg a) = dom p /\ Seg a by RELAT_1:61
    .=Seg len p /\ Seg a by Def3;
  len p <= a or a <= len p;
  then dom(p|Seg a) = Seg len p or dom(p|Seg a) = Seg a by A1,Th5,XBOOLE_1:28;
  hence thesis by A0,Def2;
end;

theorem
  rng p c= dom f implies f*p is FinSequence
proof
  assume rng p c= dom f;
  then dom(f*p) = dom p by RELAT_1:27
    .= Seg len p by Def3;
  hence thesis by Def2;
end;

theorem Th17:
  a <= len p & q = p|(Seg a) implies len q = a & dom q = Seg a
proof
  assume that
A1: a <= len p and
A2: q = p|(Seg a);
  Seg a c= Seg len p by A1,Th5;
  then Seg a c= dom p by Def3;
  then a in NAT & dom q = Seg a by A2,ORDINAL1:def 12,RELAT_1:62;
  hence thesis by Def3;
end;

::                             ::
::    FinSequences of D        ::
::                             ::

definition
  let D be set;
  mode FinSequence of D -> FinSequence means
    :Def4:
    rng it c= D;
  existence
  proof
    rng {} c= D;
    hence thesis;
  end;
end;

registration
  let D be set;
  cluster -> D-valued for FinSequence of D;
  coherence
  proof
    let f be FinSequence of D;
    thus rng f c= D by Def4;
  end;
end;

Lm2: for D being set, f being FinSequence of D holds f is PartFunc of NAT,D
proof
  let D be set, f be FinSequence of D;
  dom f c= NAT & rng f c= D by Def4;
  hence thesis by RELSET_1:4;
end;

registration
  cluster empty -> FinSequence-like for Relation;
  coherence;
end;

registration
  let D be set;
  cluster FinSequence-like for PartFunc of NAT,D;
  existence
  proof {} is PartFunc of NAT,D by RELSET_1:12;
    hence thesis;
  end;
end;

definition
  let D be set;
  redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D;
  coherence by Lm2;
end;

reserve D for set;

theorem Th18:
  for p being FinSequence of D holds p|(Seg a) is FinSequence of D
proof
  let p be FinSequence of D;
A1: p|(Seg a) is FinSequence by Th15;
  rng(p|(Seg a)) c= rng p & rng p c= D by Def4,RELAT_1:70;
  hence thesis by A1,Def4,XBOOLE_1:1;
end;

theorem
  for D being non empty set ex p being FinSequence of D st len p = a
proof
  let D be non empty set;
  reconsider a as Element of NAT by ORDINAL1:def 12;
  set y = the Element of D;
  set p = Seg a --> y;
A1: dom p = Seg a by FUNCOP_1:13;
  then reconsider p as FinSequence by Def2;
  rng p c= {y} & {y} c= D by FUNCOP_1:13,ZFMISC_1:31;
  then reconsider q=p as FinSequence of D by Def4,XBOOLE_1:1;
  take q;
  thus thesis by A1,Def3;
end;

::                                ::
::    The Empty FinSequence       ::
::                                ::

Lm3: q = {} iff len q = 0;

theorem
  p <> {} iff len p >= 1
proof
  hereby
    assume p <> {};
    then len p+1 > 0+1 by XREAL_1:8;
    hence len p >=1 by NAT_1:13;
  end;
  assume len p >= 1;
  hence thesis;
end;

definition
  let x be object;
  func <*x*> -> set equals
  { [1,x] };
  coherence;
end;

definition
  let D be set;
  func <*>D -> FinSequence of D equals
  {};
  coherence
  proof
    rng {} c= D;
    hence thesis by Def4;
  end;
end;

registration
  let D be set;
  cluster <*>D -> empty;
  coherence;
end;

registration
  let D be set;
  cluster empty for FinSequence of D;
  existence
  proof
    take <*>D;
    thus thesis;
  end;
end;

definition
  let p,q;
  func p^q -> FinSequence means
  :Def7:
  dom it = Seg (len p + len q) & (for k st k in dom p holds it.k=p.k) &
  for k st k in dom q holds it.(len p + k) = q.k;
  existence
  proof
    defpred P[object,object] means
    (for k st k=$1 & 1 <= k & k <= len p holds $2=p.k) &
    (for k st k=$1 & len p + 1 <= k & k <= len p + len q
    holds $2=q.(k-len p));
A1: for x being object st x in Seg(len p + len q) ex y being object st P[x,y]
    proof
      let x be object;
      assume x in Seg(len p + len q);
      then reconsider m=x as Element of NAT;
A2:   now
        assume
A3:     len p + 1 <= m;
        set y = q.(m-len p);
A4:     for k st k=x & 1 <= k & k <= len p holds y=p.k
        proof
          let k;
          assume that
A5:       k=x and 1 <= k and
A6:       k <= len p;
          m + (len p + 1) <= m + len p by A3,A5,A6,XREAL_1:7;
          then m + len p + 1 <= m + len p + 0;
          hence thesis by XREAL_1:6;
        end;
        for k st k=x & len p + 1 <= k & k <= len p + len q holds y=q.(k-len p);
        hence thesis by A4;
      end;
      now
        assume
A7:     not len p + 1 <= m;
        set y=p.m;
( for k st k=x & 1 <= k & k <= len p holds y=p.k)& for k st k=x & len p + 1 <=
        k & k <= len p + len q holds y=q.(k-len p) by A7;
        hence thesis;
      end;
      hence thesis by A2;
    end;
    consider f such that
A8: dom f=Seg(len p + len q) &
    for x being object st x in Seg(len p + len q) holds P[x,f.x]
      from CLASSES1:sch 1
    (A1);
A9: for k st k in dom p holds f.k=p.k
    proof
      let k;
      assume k in dom p;
      then
A10:  k in Seg len p by Def3;
      then
A11:  1 <= k & k <= len p by Th1;
      Seg len p c= Seg(len p + len q) by Th5,NAT_1:11;
      hence thesis by A8,A10,A11;
    end;
A12: for n st n in dom q holds f.(len p+n)=q.n
    proof
      let n;
      assume n in dom q;
      then
A13:  n in Seg len q by Def3;
      then
A14:  1 <= n by Th1;
A15:  n <= len q by A13,Th1;
A16:  len p + 1 <= len p + n by A14,XREAL_1:7;
A17:  len p + n <= len p + len q by A15,XREAL_1:7;
      len p + n <= len p + n + len p by NAT_1:11;
      then len p + 1 <= len p + n + len p by A16,XXREAL_0:2;
      then 1 <= len p + n by XREAL_1:6;
      then (len p + n) in Seg(len p + len q) by A17;
      then f.(len p + n)=q.(n + len p - len p) by A8,A16,A17;
      hence thesis;
    end;
    reconsider r=f as FinSequence by A8,Def2;
    take r;
    thus thesis by A8,A9,A12;
  end;
  uniqueness
  proof
    let f,g be FinSequence such that
A18: dom f = Seg(len p + len q) and
A19: for k st k in dom p holds f.k=p.k and
A20: for k st k in dom q holds f.(len p + k)=q.k and
A21: dom g = Seg(len p + len q) and
A22: for k st k in dom p holds g.k=p.k and
A23: for k st k in dom q holds g.(len p + k)=q.k;
    for x being object st x in Seg(len p + len q) holds f.x=g.x
    proof
      let x be object;
      assume
A24:  x in Seg(len p + len q);
      then reconsider k=x as Element of NAT;
A25:  1 <= k by A24,Th1;
A26:  now
        assume len p + 1 <= k;
        then consider m be Nat such that
A27:    len p + 1 + m = k by NAT_1:10;
        len p + (1 + m) <= len p + len q by A24,A27,Th1;
        then 1+0<=1+m & 1 + m <= len q by XREAL_1:6;
        then (1+m) in Seg len q;
        then
A28:    (1+m) in dom q by Def3;
        then g.(len p +(1+m)) = q.(1+m) by A23;
        hence thesis by A20,A27,A28;
      end;
      now
        assume not len p + 1 <= k;
        then k <= len p by NAT_1:8;
        then k in Seg len p by A25;
        then
A29:    k in dom p by Def3;
        then f.k=p.k by A19;
        hence thesis by A22,A29;
      end;
      hence thesis by A26;
    end;
    hence thesis by A18,A21;
  end;
end;

theorem Th21:
  p = (p ^ q) | (dom p)
proof
A1: dom(p ^ q) = Seg(len p + len q) by Def7;
A2: dom p = Seg len p by Def3;
  then
A3: dom p = dom(p ^ q) /\ Seg len p by A1,Th7,NAT_1:12;
  for x being object st x in dom p holds p.x = (p ^ q).x by Def7;
  hence thesis by A2,A3,FUNCT_1:46;
end;

theorem Th22:
  len(p^q) = len p + len q
proof
  dom(p^q) = Seg(len p + len q) by Def7;
  hence thesis by Def3;
end;

theorem Th23:
  for k being Nat st
  len p + 1 <= k & k <= len p + len q holds (p^q).k=q.(k-len p)
proof
  let k be Nat;
  assume that
A1: len p + 1 <= k and
A2: k <= len p + len q;
  consider m be Nat such that
A3: (len p + 1)+m=k by A1,NAT_1:10;
A4: len p+(1+m) = k by A3;
  1+m = k - len p by A3;
  then
A5: 1 <= 1+m by A1,XREAL_1:19;
  k-len p <= len q by A2,XREAL_1:20;
  then 1+m in Seg len q by A3,A5;
  then 1+m in dom q by Def3;
  hence thesis by A4,Def7;
end;

theorem Th24:
  for k being Nat st len p < k & k <= len(p^q) holds (p^q).k = q.(k - len p)
proof
  let k be Nat;
  assume len p < k & k <= len(p^q);
  then len p + 1 <= k & k <= len p + len q by Th22,NAT_1:13;
  hence thesis by Th23;
end;

theorem Th25:
  for k being Nat st k in dom (p^q) holds
  (k in dom p or ex n st n in dom q & k=len p + n )
proof
  let k be Nat;
  assume k in dom(p^q);
  then
A1: k in Seg len (p^q) by Def3;
  then
A2: k in Seg(len p + len q) by Th22;
A3: k in NAT & 1 <= k by A1,Th1;
A4: now
    assume not len p+1 <= k;
    then k <= len p by NAT_1:8;
    then k in Seg len p by A3;
    hence thesis by Def3;
  end;
  now
    assume len p + 1 <= k;
    then consider n be Nat such that
A5: k=len p + 1 + n by NAT_1:10;
    len p + (1 + n) <= len p + len q by A2,A5,Th1;
    then
A6: 1+n <= len q by XREAL_1:6;
    1 <= 1+n by NAT_1:11;
    then 1+n in Seg len q by A6;
    then
A7: 1+n in dom q by Def3;
    k=len p + (1+n) by A5;
    hence thesis by A7;
  end;
  hence thesis by A4;
end;

theorem Th26:
  dom p c= dom(p^q)
proof
  Seg len p c= Seg(len p + len q) by Th5,NAT_1:11;
  then Seg len p c= dom(p^q) by Def7;
  hence thesis by Def3;
end;

theorem Th27:
  x in dom q implies ex k st k=x & len p + k in dom(p^q)
proof
  assume
A1: x in dom q;
  then
A2: x in Seg len q by Def3;
  reconsider k=x as Element of NAT by A1;
  take k;
A3: 1 <= k by A2,Th1;
A4: k <= len q by A2,Th1;
  k <= len p + k by NAT_1:11;
  then
A5: 1 <= len p + k by A3,XXREAL_0:2;
  len p + k <= len p + len q by A4,XREAL_1:7;
  then len p + k in Seg(len p + len q) by A5;
  hence thesis by Def7;
end;

theorem Th28:
  k in dom q implies len p + k in dom(p^q)
proof
  assume k in dom q;
  then ex n st n=k & len p + n in dom(p^q) by Th27;
  hence thesis;
end;

theorem Th29:
  rng p c= rng(p^q)
proof
    let x be object;
    assume x in rng p;
    then consider y being object such that
A1: y in dom p and
A2: x=p.y by FUNCT_1:def 3;
    reconsider k=y as Element of NAT by A1;
A3: dom p c= dom(p^q) by Th26;
    (p^q).k=p.k by A1,Def7;
    hence x in rng(p^q) by A1,A2,A3,FUNCT_1:def 3;
end;

theorem Th30:
  rng q c= rng(p^q)
proof
    let x be object;
    assume x in rng q;
    then consider y being object such that
A1: y in dom q and
A2: x=q.y by FUNCT_1:def 3;
    reconsider k=y as Element of NAT by A1;
    len p + k in dom(p^q) & (p^q).(len p + k) = q.k by A1,Def7,Th28;
    hence x in rng(p^q) by A2,FUNCT_1:def 3;
end;

theorem Th31:
  rng(p^q) = rng p \/ rng q
proof
  now
    let x be object;
    assume x in rng(p^q);
    then consider y being object such that
A1: y in dom(p^q) and
A2: x=(p^q).y by FUNCT_1:def 3;
A3: y in Seg(len p + len q) by A1,Def7;
    reconsider k=y as Element of NAT by A1;
A4: 1 <= k by A3,Th1;
A5: k <= len p + len q by A3,Th1;
A6: now
      assume
A7:   len p + 1 <= k;
      then
A8:   q.(k-len p) = x by A2,A5,Th23;
      consider m be Nat such that
A9:   (len p+1)+m = k by A7,NAT_1:10;
      len p +(1+m) = k by A9;
      then 1+0<=1+m & 1+m <= len q by A3,Th1,XREAL_1:6;
      then 1+m in Seg len q;
      then k-len p in dom q by A9,Def3;
      hence x in rng q by A8,FUNCT_1:def 3;
    end;
    now
      assume not len p + 1 <= k;
      then k <= len p by NAT_1:8;
      then k in Seg len p by A4;
      then
A10:  k in dom p by Def3;
      then p.k = x by A2,Def7;
      hence x in rng p by A10,FUNCT_1:def 3;
    end;
    hence x in rng p \/ rng q by A6,XBOOLE_0:def 3;
  end;
  then
A11: rng(p^q) c= rng p \/ rng q;
  rng p c= rng(p^q) & rng q c= rng(p^q) by Th29,Th30;
  then (rng p \/ rng q) c= rng(p^q) by XBOOLE_1:8;
  hence thesis by A11;
end;

theorem Th32:
  p^q^r = p^(q^r)
proof
A1: dom ((p^q)^r) = Seg(len (p^q) + len r) by Def7
    .= Seg(len p + len q + len r) by Th22
    .= Seg(len p + (len q + len r))
    .= Seg(len p + len(q^r)) by Th22;
A2: for k st k in dom p holds ((p^q)^r).k=p.k
  proof
    let k;
    assume
A3: k in dom p;
    dom p c= dom(p^q) by Th26;
    hence (p^q^r).k=(p^q).k by A3,Def7
      .=p.k by A3,Def7;
  end;
  for k st k in dom(q^r) holds ((p^q)^r).(len p + k)=(q^r).k
  proof
    let k;
    assume
A4: k in dom(q^r);
A5: now
      assume
A6:   k in dom q;
      then (len p + k) in dom(p^q) by Th28;
      hence (p^q^r).(len p + k) = (p^q).(len p + k) by Def7
        .=q.k by A6,Def7
        .=(q^r).k by A6,Def7;
    end;
    now
      assume not k in dom q;
      then consider n such that
A7:   n in dom r and
A8:   k=len q + n by A4,Th25;
      thus (p^q^r).(len p + k) =(p^q^r).(len p + len q + n) by A8
        .=(p^q^r).(len(p^q) + n) by Th22
        .=r.n by A7,Def7
        .=(q^r).k by A7,A8,Def7;
    end;
    hence thesis by A5;
  end;
  hence thesis by A1,A2,Def7;
end;

theorem
  p^r = q^r or r^p = r^q implies p = q
proof
  assume
A1: p^r = q^r or r^p = r^q;
A2: now
    assume
A3: p^r = q^r;
    then len p + len r = len(q^r) by Th22;
    then len p + len r = len q + len r by Th22;
    then
A4: dom p = Seg len q by Def3
      .= dom q by Def3;
    for k st k in dom p holds p.k=q.k
    proof
      let k;
      assume
A5:   k in dom p;
      hence p.k=(q^r).k by A3,Def7
        .=q.k by A4,A5,Def7;
    end;
    hence thesis by A4;
  end;
  now
    assume
A6: r^p=r^q;
    then len r + len p = len(r^q) by Th22
      .=len r + len q by Th22;
    then
A7: dom p = Seg len q by Def3
      .= dom q by Def3;
    for k st k in dom p holds p.k=q.k
    proof
      let k;
      assume
A8:   k in dom p;
      hence p.k = (r^q).(len r + k) by A6,Def7
        .= q.k by A7,A8,Def7;
    end;
    hence thesis by A7;
  end;
  hence thesis by A1,A2;
end;

theorem Th34:
  p^{} = p & {}^p = p
proof
A1: dom(p^{}) = Seg len (p^{}) by Def3
    .= Seg (len p + len {}) by Th22
    .= dom p by Def3;
  for k st k in dom p holds p.k=(p^{}).k by Def7;
  hence p^{} = p by A1;
A2: dom({}^p) = Seg len ({}^p) by Def3
    .= Seg (len {} + len p) by Th22
    .= dom p by Def3;
  for k st k in dom p holds p.k = ({}^p).k
  proof
    let k;
    assume
A3: k in dom p;
    thus ({}^p).k =({}^p).(len {} + k) .=p.k by A3,Def7;
  end;
  hence {}^p=p by A2;
end;

theorem Th35:
  p^q = {} implies p={} & q={}
proof
  assume p^q={};
  then 0 = len (p^q) .= len p + len q by Th22;
  hence thesis;
end;

definition
  let D be set;
  let p,q be FinSequence of D;
  redefine func p^q -> FinSequence of D;
  coherence
  proof
A1: rng(p^q) = rng p \/ rng q & rng p c= D by Def4,Th31;
    rng q c= D by Def4;
    hence rng(p^q) c= D by A1,XBOOLE_1:8;
  end;
end;

Lm4: for x1, y1 being object holds [x,y] in {[x1,y1]} implies x = x1 & y = y1
proof
  let x1, y1 be object;
  assume [x,y] in {[x1,y1]};
  then [x,y] = [x1,y1] by TARSKI:def 1;
  hence thesis by XTUPLE_0:1;
end;

definition
  let x be object;
  redefine func <*x*> -> Function means
  :Def8:
  dom it = Seg 1 & it.1 = x;
  coherence;
  compatibility
  proof
    let f be Function;
    hereby
      assume
A1:   f = <*x*>;
      hence dom f = Seg 1 by Th2,RELAT_1:9;
      [1,x] in f by A1,TARSKI:def 1;
      hence f.1 = x by FUNCT_1:1;
    end;
    assume that
A2: dom f = Seg 1 and
A3: f.1 = x;
    reconsider g = { [1,f.1] } as Function;
    for y,z being object holds [y,z] in f iff [y,z] in g
    proof let y,z be object;
      hereby
        assume
A4:     [y,z] in f;
        then
A5:     y in {1} by A2,Th2,XTUPLE_0:def 12;
A6:     z in rng f by A4,XTUPLE_0:def 13;
A7:     rng f = {f.1} by A2,Th2,FUNCT_1:4;
A8:     y = 1 by A5,TARSKI:def 1;
        z = f.1 by A6,A7,TARSKI:def 1;
        hence [y,z] in g by A8,TARSKI:def 1;
      end;
      assume [y,z] in g;
      then
A9:   y = 1 & z = f.1 by Lm4;
      1 in dom f by A2;
      hence thesis by A9,FUNCT_1:def 2;
    end;
    hence thesis by A3,RELAT_1:def 2;
  end;
end;

registration
  let x be object;
  cluster <*x*> -> Function-like Relation-like;
  coherence;
end;

registration
  let x be object;
  cluster <*x*> -> FinSequence-like;
  coherence by Def8;
end;

theorem Th36:
  p^q is FinSequence of D implies p is FinSequence of D & q is FinSequence of D
proof
  assume p^q is FinSequence of D;
  then rng(p^q) c= D by Def4;
  then
A1: rng p \/ rng q c= D by Th31;
  rng p c= rng p \/ rng q by XBOOLE_1:7;
  hence p is FinSequence of D by Def4,A1,XBOOLE_1:1;
  rng q c= rng p \/ rng q by XBOOLE_1:7;
  hence thesis by Def4,A1,XBOOLE_1:1;
end;

definition
  let x,y be object;
  func <*x,y*> -> set equals
  <*x*>^<*y*>;
  correctness;
  let z be object;
  func <*x,y,z*> -> set equals
  <*x*>^<*y*>^<*z*>;
  correctness;
end;

registration
  let x,y be object;
  cluster <*x,y*> -> Function-like Relation-like;
  coherence;
  let z be object;
  cluster <*x,y,z*> -> Function-like Relation-like;
  coherence;
end;

registration
  let x,y be object;
  cluster <*x,y*> -> FinSequence-like;
  coherence;
  let z be object;
  cluster <*x,y,z*> -> FinSequence-like;
  coherence;
end;

theorem
 for x being object holds <*x*> = { [1,x] };

theorem Th38:
 for x being object holds p=<*x*> iff dom p = Seg 1 & rng p = {x}
proof let x be object;
  thus p = <*x*> implies dom p = Seg 1 & rng p = {x}
  proof
    assume
A1: p = <*x*>;
    hence dom p = Seg 1 by Def8;
    dom p = {1} by A1,Def8,Th2;
    then rng p = {p.1} by FUNCT_1:4;
    hence thesis by A1,Def8;
  end;
  assume that
A2: dom p = Seg 1 and
A3: rng p = {x};
  1 in dom p by A2;
  then p.1 in {x} by A3,FUNCT_1:def 3;
  then p.1 = x by TARSKI:def 1;
  hence thesis by A2,Def8;
end;

theorem Th39:
  for x being object holds p=<*x*> iff len p = 1 & rng p = {x}
proof let x be object;
  len p = 1 iff dom p = Seg 1 by Def3;
  hence thesis by Th38;
end;

theorem Th40:
  for x being object holds p = <*x*> iff len p = 1 & p.1 = x
proof let x be object;
  len p = 1 iff dom p = Seg 1 by Def3;
  hence thesis by Def8;
end;

theorem
  for x being object holds (<*x*>^p).1 = x
proof let x be object;
  1 in Seg 1;
  then 1 in dom <*x*> by Def8;
  then (<*x*>^p).1 = <*x*>.1 by Def7;
  hence thesis by Def8;
end;

theorem Th42:
  for x being object holds (p^<*x*>).(len p + 1)=x
proof let x be object;
  dom <*x*> = Seg 1 by Def8;
  then 1 in dom <*x*>;
  hence (p^<*x*>).(len p + 1) = <*x*>.1 by Def7
    .=x by Def8;
end;

theorem
  for x,y,z being object
    holds <*x,y,z*>=<*x*>^<*y,z*> & <*x,y,z*>=<*x,y*>^<*z*> by Th32;

theorem Th44:
  for x,y being object holds p = <*x,y*> iff len p = 2 & p.1=x & p.2=y
proof let x,y be object;
  thus
  p = <*x,y*> implies len p = 2 & p.1=x & p.2=y
  proof
    assume
A1: p=<*x,y*>;
    hence len p = len <*x*> + len <*y*> by Th22
      .= 1 + len <*y*> by Th39
      .= 1 + 1 by Th39
      .=2;
A2: 1 in {1} by TARSKI:def 1;
    then 1 in dom <*x*> by Def8,Th2;
    hence p.1 = <*x*>.1 by A1,Def7
      .= x by Def8;
A3: 1 in dom <*y*> by A2,Def8,Th2;
    thus p.2 = (<*x*>^<*y*>).(1+1) by A1
      .= (<*x*>^<*y*>).(len <*x*> + 1) by Th39
      .= <*y*>.1 by A3,Def7
      .= y by Def8;
  end;
  assume that
A4: len p = 2 and
A5: p.1=x and
A6: p.2=y;
A7: dom p = Seg(1+1) by A4,Def3
    .= Seg(len <*x*> + 1) by Th39
    .= Seg(len <*x*> + len <*y*>) by Th39;
A8: for k st k in dom <*x*> holds p.k=<*x*>.k
  proof
    let k;
    assume k in dom <*x*>;
    then k in {1} by Def8,Th2;
    then k=1 by TARSKI:def 1;
    hence thesis by A5,Def8;
  end;
  for k st k in dom <*y*> holds p.((len <*x*>)+k)=<*y*>.k
  proof
    let k;
    assume k in dom <*y*>;
    then
A9: k in {1} by Def8,Th2;
    thus p.((len <*x*>) + k) = p.(1+k) by Th39
      .=p.(1+1) by A9,TARSKI:def 1
      .=<*y*>.1 by A6,Def8
      .= <*y*>.k by A9,TARSKI:def 1;
  end;
  hence thesis by A7,A8,Def7;
end;

theorem Th45:
  for x,y,z being object
   holds p = <*x,y,z*> iff len p = 3 & p.1 = x & p.2 = y & p.3 = z
proof let x,y,z be object;
  thus p = <*x,y,z*> implies len p = 3 & p.1 = x & p.2 = y & p.3 = z
  proof
    assume
A1: p =<*x,y,z*>;
    hence len p =len <*x,y*> + len <*z*> by Th22
      .=2 + len <*z*> by Th44
      .=2+1 by Th39
      .=3;
A2: 1 in {1} by TARSKI:def 1;
    then
A3: 1 in dom <*x*> by Def8,Th2;
    thus p.1 = (<*x*>^<*y,z*>).1 by A1,Th32
      .=<*x*>.1 by A3,Def7
      .=x by Def8;
    2 in Seg 2 & len <*x,y*> = 2 by Th44;
    then 2 in dom <*x,y*> by Def3;
    hence p.2 =<*x,y*>.2 by A1,Def7
      .=y by Th44;
A4: 1 in dom <*z*> by A2,Def8,Th2;
    thus p.3 = (<*x,y*>^<*z*>).(2+1) by A1
      .=(<*x,y*>^<*z*>).(len (<*x,y*>) + 1) by Th44
      .= <*z*>.1 by A4,Def7
      .= z by Def8;
  end;
  assume that
A5: len p = 3 and
A6: p.1 = x and
A7: p.2 = y and
A8: p.3 = z;
A9: dom p = Seg(2+1) by A5,Def3
    .= Seg((len <*x,y*>) + 1) by Th44
    .= Seg((len <*x,y*>) + len <*z*>) by Th39;
A10: for k st k in dom <*x,y*> holds p.k=<*x,y*>.k
  proof
    let k such that
A11: k in dom <*x,y*>;
    len <*x,y*> = 2 by Th44;
    then
A12: k in Seg 2 by A11,Def3;
A13: k=1 implies p.k=<*x,y*>.k by A6,Th44;
    k=2 implies p.k=<*x,y*>.k by A7,Th44;
    hence thesis by A12,A13,Th2,TARSKI:def 2;
  end;
  for k st k in dom <*z*> holds p.( (len <*x,y*>) + k) = <*z*>.k
  proof
    let k;
    assume k in dom <*z*>;
    then k in {1} by Def8,Th2;
    then
A14: k = 1 by TARSKI:def 1;
    hence p.( (len <*x,y*>) + k) = p.(2+1) by Th44
      .=<*z*>.k by A8,A14,Def8;
  end;
  hence thesis by A9,A10,Def7;
end;

theorem Th46:
  for x being object holds p <> {} implies ex q,x st p=q^<*x*>
proof let x be object;
  assume p <> {};
  then consider n be Nat such that
A1: len p = n + 1 by NAT_1:6;
  reconsider n as Element of NAT by ORDINAL1:def 12;
  reconsider q=p|Seg n as FinSequence by Th15;
  take q;
  take p.(len p);
A2: dom q = dom p /\ Seg n by RELAT_1:61
    .= Seg len p /\ Seg n by Def3;
  Seg n c= Seg len p by Th5,A1,NAT_1:11;
  then
A3: dom q = Seg n by A2,XBOOLE_1:28;
A4: dom(q^<*p.(len p)*>) = Seg len (q^<*p.(len p)*>) by Def3
    .= Seg(len q + len <*p.(len p)*>) by Th22
    .= Seg(len q + 1) by Th39
    .= Seg len p by A1,A3,Def3
    .= dom p by Def3;
  for x being object st x in dom p holds p.x = (q^<*p.(len p)*>).x
  proof
    let x be object;
    assume
A5: x in dom p;
    then reconsider k = x as Element of NAT;
    k in Seg(n+1) by A1,A5,Def3;
    then
A6: k in Seg n \/ {n+1} by Th9;
A7: now
      assume
A8:   k in Seg n;
      hence p.k=q.k by A3,FUNCT_1:47
        .=(q^<*p.(len p)*>).k by A3,A8,Def7;
    end;
    now
      assume
A9:   k in {n+1};
      1 in Seg 1;
      then
A10:  1 in dom <*p.(len p)*> by Def8;
      thus (q^<*p.(len p)*>).k =(q^<*p.(len p)*>).(n+1) by A9,TARSKI:def 1
        .=(q^<*p.(len p)*>).(len q + 1) by A3,Def3
        .=<*p.(len p)*>.1 by A10,Def7
        .=p.(n+1) by A1,Def8
        .=p.k by A9,TARSKI:def 1;
    end;
    hence thesis by A6,A7,XBOOLE_0:def 3;
  end;
  hence q^<*p.(len p)*>=p by A4;
end;

definition
  let D be non empty set;
  let x be Element of D;
  redefine func <*x*> -> FinSequence of D;
  coherence
  proof
    let y be object;
    assume y in rng <*x*>;
    then y in {x} by Th39;
    then y = x by TARSKI:def 1;
    hence thesis;
  end;
end;

:: scheme of induction for finite sequences ::

scheme IndSeq{P[FinSequence]}: for p holds P[p]
provided
A1: P[{}] and
A2: for p,x st P[p] holds P[p^<*x*>]
proof
  let p;
  defpred R[set] means for p st len p = $1 holds P[p];
  consider X being Subset of REAL such that
A3: for x being Element of REAL holds x in X iff R[x] from SUBSET_1:sch 3;
  for k holds k in X
  proof
A4: 0 in REAL by XREAL_0:def 1;
    defpred S[Nat] means $1 in X;
    for q st len q = 0 holds P[q] by A1,Lm3;
    then
A5: S[0] by A3,A4;
    now
      let n such that
A6:   n in X;
A7:  n+1 in REAL by NUMBERS:19;
      now
        let q;
        assume
A8:     len q = n+1;
        then q <> {};
        then consider r,x such that
A9:     q=r^<*x*> by Th46;
        len q = len r + len <*x*> by A9,Th22
          .= len r + 1 by Th39;
        hence P[q] by A2,A9,A3,A6,A8;
      end;
      hence n+1 in X by A3,A7;
    end;
    then
A10: for n st S[n] holds S[n+1];
    thus for n holds S[n] from NAT_1:sch 2(A5,A10);
  end;
  then len p in X;
  hence thesis by A3;
end;

theorem
  for p,q,r,s being FinSequence st p^q = r^s & len p <= len r
  ex t being FinSequence st p^t = r
proof
  defpred S[FinSequence] means
  for p,q,s st p^q=$1^s & len p <= len $1 holds ex t st p^t=$1;
A1: S[{}]
  proof
    let p,q,s;
    assume that
    p^q={}^s and
A2: len p <= len {};
    take {};
    thus p^{} = p by Th34
      .= {} by A2;
  end;
A3: for r,x st S[r] holds S[r^<*x*>]
  proof
    let r,x;
    assume
A4: for p,q,s st p^q=r^s & len p <= len r ex t st p^t=r;
    let p,q,s;
    assume that
A5: p^q=(r^<*x*>)^s and
A6: len p <= len (r^<*x*>);
A7: now
      assume len p = len(r^<*x*>);
      then
A8:   dom p = Seg len(r^<*x*>) by Def3
        .= dom(r^<*x*>) by Def3;
A9:   for k st k in dom p holds p.k=(r^<*x*>).k
      proof
        let k;
        assume
A10:    k in dom p;
        hence p.k = (r^<*x*>^s).k by A5,Def7
          .=(r^<*x*>).k by A8,A10,Def7;
      end;
      p^{} = p by Th34
        .=r^<*x*> by A8,A9;
      hence thesis;
    end;
    now
      assume len p <> len(r^<*x*>);
      then len p <> len r + len <*x*> by Th22;
      then
A11:  len p <> len r + 1 by Th39;
      len p <= len r + len <*x*> by A6,Th22;
      then
A12:  len p <= len r + 1 by Th39;
      p^q=r^(<*x*>^s) by A5,Th32;
      then consider t being FinSequence such that
A13:  p^t = r by A4,A11,A12,NAT_1:8;
      p^(t^<*x*>) = r^<*x*> by A13,Th32;
      hence thesis;
    end;
    hence thesis by A7;
  end;
  for r holds S[r] from IndSeq(A1,A3);
  hence thesis;
end;

registration
 cluster -> NAT-defined for FinSequence;
 coherence
  proof let f be FinSequence;
   thus dom f c= NAT;
  end;
end;

definition
  let D be set;
  func D* -> set means
  :Def11:
  x in it iff x is FinSequence of D;
  existence
  proof
    defpred P[object] means $1 is FinSequence of D;
    consider X such that
A1: for x being object holds x in X iff x in bool [:NAT,D:] & P[x]
     from XBOOLE_0:sch 1;
    take X;
    let x;
    thus x in X implies x is FinSequence of D by A1;
    assume x is FinSequence of D;
    then reconsider p = x as FinSequence of D;
    p c= [:NAT,D:];
    hence thesis by A1;
  end;
  uniqueness
  proof
    let D1,D2 be set such that
A2: x in D1 iff x is FinSequence of D and
A3: x in D2 iff x is FinSequence of D;
    now
      let x be object;
      thus x in D1 implies x in D2
      proof
        assume x in D1;
        then x is FinSequence of D by A2;
        hence thesis by A3;
      end;
      assume x in D2;
      then x is FinSequence of D by A3;
      hence x in D1 by A2;
    end;
    hence thesis by TARSKI:2;
  end;
end;

registration
  let D be set;
  cluster D* -> non empty;
  coherence
  proof
    set f = the FinSequence of D;
    f in D* by Def11;
    hence thesis;
  end;
end;

theorem
  rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q
proof
  defpred P[FinSequence] means $1 is one-to-one implies
  for q st rng $1 = rng q & q is one-to-one holds len $1 = len q;
A1: P[{}] by RELAT_1:41;
  now
    let p,x;
    assume
A2: p is one-to-one implies
    for q st rng p = rng q & q is one-to-one holds len p = len q;
    assume
A3: p ^ <* x *> is one-to-one;
    let q;
    assume that
A4: rng(p ^ <* x *>) = rng q and
A5: q is one-to-one;
A6: rng(p ^ <* x *>) = rng p \/ rng<* x *> by Th31
      .= rng p \/ {x} by Th38;
    x in {x} by TARSKI:def 1;
    then x in rng q by A4,A6,XBOOLE_0:def 3;
    then consider y being object such that
A7: y in dom q and
A8: x = q.y by FUNCT_1:def 3;
A9: y in Seg(len q) by A7,Def3;
    reconsider y as Element of NAT by A7;
A10: 1 <= y by A9,Th1;
    then consider k be Nat such that
A11: 1 + k = y by NAT_1:10;
A12: y <= len q by A9,Th1;
    then consider n be Nat such that
A13: y + n = len q by NAT_1:10;
    reconsider k,n as Element of NAT by ORDINAL1:def 12;
    reconsider q1 = q | (Seg k) as FinSequence by Th15;
    defpred P[Nat,object] means $2 = q.(y + $1);
A14: for j being Nat st j in Seg n ex x st P[j,x];
    consider q2 being FinSequence such that
A15: dom q2 = Seg n and
A16: for j being Nat st j in Seg n holds P[j,q2.j] from SeqEx(A14);
A17: k <= y by A11,NAT_1:12;
    then
A18: k <= len q by A12,XXREAL_0:2;
    then
A19: len q1 = k by Th17;
    len(q1 ^ <* x *>) + len q2 = len q1 + len<* x *> + len q2 by Th22
      .= k + 1 + len q2 by A19,Th39
      .= len q by A11,A13,A15,Def3;
    then
A20: dom q = Seg(len(q1 ^ <* x *>) + len q2) by Def3;
A21: rng(q1 ^ q2) = rng q \ {x}
    proof
      thus rng(q1 ^ q2) c= rng q \ {x}
      proof
        let z be object;
        assume z in rng(q1 ^ q2);
        then
A22:    z in rng q1 \/ rng q2 by Th31;
A23:    now
          assume
A24:      z in rng q1;
          A25:      rng
 q1 = q .: (Seg k) & q .: (Seg k) c= rng q by RELAT_1:111,115;
          consider y1 being object such that
A26:      y1 in dom q1 and
A27:      q1.y1 = z by A24,FUNCT_1:def 3;
A28:      q1.y1 = q.y1 by A26,FUNCT_1:47;
A29:      y1 in Seg(len q1) by A26,Def3;
          reconsider y1 as Element of NAT by A26;
A30:      y1 <= k by A19,A29,Th1;
A31:      k < y by A11,XREAL_1:29;
          Seg k c= Seg(len q) by A17,Th5,A12,XXREAL_0:2;
          then dom q1 c= Seg(len q) by A18,Th17;
          then dom q1 c= dom q by Def3;
          then x <> z by A5,A7,A8,A26,A27,A28,A30,A31;
          then not z in {x} by TARSKI:def 1;
          hence thesis by A24,A25,XBOOLE_0:def 5;
        end;
        now
          assume z in rng q2;
          then consider y1 being object such that
A32:      y1 in dom q2 and
A33:      q2.y1 = z by FUNCT_1:def 3;
          reconsider y1 as Element of NAT by A32;
A34:      q2.y1 = q.(y + y1) by A15,A16,A32;
A35:      1 <= y + y1 by A10,NAT_1:12;
          y1 <= n by A15,A32,Th1;
          then y + y1 <= len q by A13,XREAL_1:7;
          then y + y1 in Seg(len q) by A35;
          then
A36:      y + y1 in dom q by Def3;
          then
A37:      z in rng q by A33,A34,FUNCT_1:def 3;
          y1 <> 0 by A15,A32,Th1;
          then y <> y + y1;
          then x <> z by A5,A7,A8,A33,A34,A36;
          then not z in {x} by TARSKI:def 1;
          hence thesis by A37,XBOOLE_0:def 5;
        end;
        hence thesis by A22,A23,XBOOLE_0:def 3;
      end;
      let z be object;
      assume
A38:  z in rng q \ {x};
      then consider y1 being object such that
A39:  y1 in dom q and
A40:  z = q.y1 by FUNCT_1:def 3;
A41:  y1 in Seg(len q) by A39,Def3;
      reconsider y1 as Element of NAT by A39;
      not z in {x} by A38,XBOOLE_0:def 5;
      then
A42:  y <> y1 by A8,A40,TARSKI:def 1;
A43:  now
        assume
A44:    y < y1;
        then consider j being Nat such that
A45:    y1 = y + j by NAT_1:10;
A46:    1 <= j by A44,A45,NAT_1:19;
        j <= n by A13,A41,A45,Th1,XREAL_1:6;
        then
A47:    j in Seg n by A46;
        then z = q2.j by A16,A40,A45;
        hence z in rng q2 by A15,A47,FUNCT_1:def 3;
      end;
      now
        assume
A48:    y1 < y;
A49:    1 <= y1 by A41,Th1;
        y1 <= k by A11,A48,NAT_1:13;
        then y1 in Seg k by A49;
        then
A50:    y1 in dom q1 by A18,Th17;
        then q1.y1 = z by A40,FUNCT_1:47;
        hence z in rng q1 by A50,FUNCT_1:def 3;
      end;
      then z in rng q1 \/ rng q2 by A42,A43,XBOOLE_0:def 3,XXREAL_0:1;
      hence thesis by Th31;
    end;
A51: p = (p ^ <* x *>) | (dom p) by Th21;
A52: rng p = rng(p ^ <* x *>) \ {x}
    proof
      thus rng p c= rng(p ^ <* x *>) \ {x}
      proof
        let z be object;
        assume
A53:    z in rng p;
A54:    rng p c= rng(p ^ <* x *>) by A51,RELAT_1:70;
        consider y1 being object such that
A55:    y1 in dom p and
A56:    p.y1 = z by A53,FUNCT_1:def 3;
A57:    y1 in Seg(len p) by A55,Def3;
        reconsider y1 as Element of NAT by A55;
A58:    (p ^ <* x *>).(len p + 1) = x by Th42;
A59:    (p ^ <* x *>).y1 = p.y1 by A51,A55,FUNCT_1:47;
A60:    y1 <= len p by A57,Th1;
A61:    len p < len p +1 by XREAL_1:29;
A62:    1 <= y1 by A57,Th1;
        y1 <= len p + 1 by A60,A61,XXREAL_0:2;
        then
A63:    y1 in Seg(len p + 1) by A62;
A64:    len p + 1 in Seg(len p + 1) by Th3;
A65:    y1 in Seg(len p + len<* x *>) by A63,Th40;
A66:    len p + 1 in Seg(len p + len<* x *>) by A64,Th40;
A67:    y1 in dom(p ^ <* x *>) by A65,Def7;
        len p + 1 in dom(p ^ <* x *>) by A66,Def7;
        then x <> z by A3,A56,A58,A59,A60,A61,A67;
        then not z in {x} by TARSKI:def 1;
        hence thesis by A53,A54,XBOOLE_0:def 5;
      end;
      let z be object;
      assume
A68:  z in rng(p ^ <* x *>) \ {x};
      then
A69:  z in rng(p ^ <* x *>);
A70:  not z in {x} by A68,XBOOLE_0:def 5;
      z in rng p \/ rng<* x *> by A69,Th31;
      then z in rng p or z in rng<* x *> by XBOOLE_0:def 3;
      hence thesis by A70,Th38;
    end;
A71: q1 ^ q2 is one-to-one
    proof
      let y1,y2 be object;
      assume that
A72:  y1 in dom(q1 ^ q2) & y2 in dom(q1 ^ q2) and
A73:  (q1 ^ q2).y1 = (q1 ^ q2).y2;
      reconsider m1 = y1, m2 = y2 as Element of NAT by A72;
A74:  q1 is one-to-one by A5,FUNCT_1:52;
A75:  now
        assume
A76:    m1 in dom q1 & m2 in dom q1;
        then (q1 ^ q2).m1 = q1.m1 & (q1 ^ q2).m2 = q1.m2 by Def7;
        hence thesis by A73,A74,A76;
      end;
A77:  now
        assume
A78:    m1 in dom q1;
        given j being Nat such that
A79:    j in dom q2 and
A80:    m2 = len q1 + j;
A81:    (q1 ^ q2).m2 = q2.j by A79,A80,Def7;
        (q1 ^ q2).m1 = q1.m1 & q1.m1 = q.m1 by A78,Def7,FUNCT_1:47;
        then
A82:    q.m1 = q.(y + j) by A15,A16,A73,A79,A81;
        1 <= j by A15,A79,Th1;
        then
A83:    1 <= y + j by NAT_1:12;
        j <= n by A15,A79,Th1;
        then y + j <= len q by A13,XREAL_1:7;
        then y + j in Seg(len q) by A83;
        then
A84:    y + j in dom q by Def3;
        m1 in Seg k by A18,A78,Th17;
        then
A85:    m1 <= k by Th1;
        k < y by A11,XREAL_1:29;
        then
A86:    m1 < y by A85,XXREAL_0:2;
        dom q1 c= dom q & y <= y + j by NAT_1:12,RELAT_1:60;
        hence thesis by A5,A78,A82,A84,A86;
      end;
A87:  now
        assume
A88:    m2 in dom q1;
        given j be Nat such that
A89:    j in dom q2 and
A90:    m1 = len q1 + j;
A91:    (q1 ^ q2).m1 = q2.j by A89,A90,Def7;
        (q1 ^ q2).m2 = q1.m2 & q1.m2 = q.m2 by A88,Def7,FUNCT_1:47;
        then
A92:    q.m2 = q.(y + j) by A15,A16,A73,A89,A91;
        1 <= j by A15,A89,Th1;
        then
A93:    1 <= y + j by NAT_1:12;
        j <= n by A15,A89,Th1;
        then y + j <= len q by A13,XREAL_1:7;
        then y + j in Seg(len q) by A93;
        then
A94:    y + j in dom q by Def3;
        m2 in Seg k by A18,A88,Th17;
        then
A95:    m2 <= k by Th1;
        k < y by A11,XREAL_1:29;
        then
A96:    m2 < y by A95,XXREAL_0:2;
        dom q1 c= dom q & y <= y + j by NAT_1:12,RELAT_1:60;
        hence thesis by A5,A88,A92,A94,A96;
      end;
      now
        given j1 being Nat such that
A97:    j1 in dom q2 and
A98:    m1 = len q1 + j1;
        given j2 being Nat such that
A99:    j2 in dom q2 and
A100:    m2 = len q1 + j2;
A101:   (q1 ^ q2).m1 = q2.j1 by A97,A98,Def7;
A102:   (q1 ^ q2).m2 = q2.j2 by A99,A100,Def7;
A103:   (q1 ^ q2).m1 = q.(y + j1) by A15,A16,A97,A101;
A104:   (q1 ^ q2).m2 = q.(y + j2) by A15,A16,A99,A102;
A105:   1 <= j1 by A15,A97,Th1;
A106:   1 <= j2 by A15,A99,Th1;
A107:   1 <= y + j1 by A105,NAT_1:12;
A108:   1 <= y + j2 by A106,NAT_1:12;
A109:   j1 <= n by A15,A97,Th1;
A110:   j2 <= n by A15,A99,Th1;
A111:   y + j1 <= len q by A13,A109,XREAL_1:7;
A112:   y + j2 <= len q by A13,A110,XREAL_1:7;
A113:   y + j1 in Seg(len q) by A107,A111;
A114:   y + j2 in Seg(len q) by A108,A112;
A115:   y + j1 in dom q by A113,Def3;
        y + j2 in dom q by A114,Def3;
        then y + j1 = y + j2 by A5,A73,A103,A104,A115;
        hence thesis by A98,A100;
      end;
      hence thesis by A72,A75,A77,A87,Th25;
    end;
A116: now
      let j be Nat;
      assume
A117: j in dom(q1 ^ <* x *>);
A118: now
        assume
A119:   j in dom q1;
        then (q1 ^ <* x *>).j = q1.j by Def7;
        hence q.j = (q1 ^ <* x *>).j by A119,FUNCT_1:47;
      end;
      now
        given i be Nat such that
A120:   i in dom<* x *> and
A121:   j = len q1 + i;
        i in {1} by A120,Th2,Th38;
        then i = 1 by TARSKI:def 1;
        hence q.j = (q1 ^ <* x *>).j by A8,A11,A19,A121,Th42;
      end;
      hence q.j = (q1 ^ <* x *>).j by A117,A118,Th25;
    end;
    now
      let j be Nat;
      assume j in dom q2;
      hence q2.j = q.(len q1 + 1 + j) by A11,A15,A16,A19
        .= q.(len q1 + len<* x *> + j) by Th39
        .= q.(len(q1 ^ <* x *>) + j) by Th22;
    end;
    then q1 ^ <* x *> ^ q2 = q by A20,A116,Def7;
    then
A122: len q = len(q1 ^ <* x *>) + len q2 by Th22
      .= len <* x *> + len q1 + len q2 by Th22
      .= 1 + len q1 + len q2 by Th40
      .= 1 + (len q1 + len q2)
      .= len(q1 ^ q2) + 1 by Th22;
    len(p ^ <* x *>) = len p + len<* x *> by Th22
      .= len p + 1 by Th40;
    hence len(p ^ <* x *>) = len q by A2,A3,A4,A21,A51,A52,A71,A122,FUNCT_1:52;
  end;
  then
A123: for p,x st P[p] holds P[p^<*x*>];
  for p holds P[p] from IndSeq(A1,A123);
  hence thesis;
end;

theorem
  {} in D*
proof
  {} = <*>D;
  hence thesis by Def11;
end;

scheme SepSeq{D()->non empty set, P[FinSequence]}:
  ex X st for x holds x in X iff ex p st p in D()* & P[p] & x=p
proof
  defpred R[object] means ex p st P[p] & $1=p;
  consider Y such that
A1: for x being object holds x in Y iff x in D()* & R[x] from XBOOLE_0:sch 1;
  take Y;
  x in Y iff ex p st p in D()* & P[p] & x=p
  proof
    now
      assume x in Y;
      then x in D()* & ex p st P[p] & x=p by A1;
      hence ex p st p in D()* & P[p] & x=p;
    end;
    hence thesis by A1;
  end;
  hence thesis;
end;

::                           ::
::        Subsequences       ::
::                           ::

definition
  let IT be Function;
  attr IT is FinSubsequence-like means
  :Def12:
  ex k st dom IT c= Seg k;
end;

registration
  cluster FinSubsequence-like for Function;
  existence
  proof
    take {},len {};
    thus thesis;
  end;
end;

definition
  mode FinSubsequence is FinSubsequence-like Function;
end;

registration
 cluster FinSequence-like -> FinSubsequence-like for Function;
 coherence;
 let p be FinSubsequence, X be set;
 cluster p|X -> FinSubsequence-like;
 coherence
proof
  consider k such that
A1: dom p c= Seg k by Def12;
   dom(p|X) c= dom p by RELAT_1:60;
  hence thesis by A1,XBOOLE_1:1;
end;
 cluster X|`p -> FinSubsequence-like;
 coherence
proof
  consider k such that
A2: dom p c= Seg k by Def12;
   dom(X|`p) c= dom p by FUNCT_1:56;
  hence thesis by A2,XBOOLE_1:1;
end;
end;

registration
 cluster  -> NAT-defined for FinSubsequence;
 coherence
  proof let f be FinSubsequence;
    ex n st dom f c= Seg n by Def12;
   hence dom f c= NAT by XBOOLE_1:1;
  end;
end;

reserve p9 for FinSubsequence;

definition
  let X;
  given k being Nat such that
A1: X c= Seg k;
  func Sgm X -> FinSequence of NAT means
  :Def13:
  rng it = X & for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len it &
  k1=it.l & k2=it.m holds k1 < k2;
  existence
  proof
    defpred P[Nat] means for X st X c= Seg $1 ex p being FinSequence of NAT st
    rng p = X & for l,m,k1,k2 being Nat st ( 1 <= l & l < m & m <= len p &
    k1=p.l & k2=p.m) holds k1 < k2;
A2: P[0]
    proof
      let X;
      assume
A3:   X c= Seg 0;
      take <*>(NAT);
      thus rng <*>(NAT) = X by A3;
      thus thesis;
    end;
A4: for k being Nat st P[k] holds P[k+1]
    proof
      let k be Nat such that
A5:   for X st X c= Seg k holds ex p being FinSequence of NAT st
      rng p = X & for l,m,k1,k2 be Nat st 1 <= l & l < m & m <= len p &
      k1=p.l & k2=p.m holds k1 < k2;
      let X;
      assume
A6:   X c= Seg(k+1);
      now
        assume not X c= Seg k;
        then consider x being object such that
A7:     x in X and
A8:     not x in Seg k;
        x in Seg(k+1) by A6,A7;
        then reconsider n=x as Element of NAT;
A9:     n=k+1
        proof
          assume
A10:      n <> k+1;
A11:      n <= k+1 by A6,A7,Th1;
A12:      1 <= n by A6,A7,Th1;
          n <= k by A10,A11,NAT_1:8;
          hence contradiction by A8,A12;
        end;
        set Y=X\{k+1};
A13:    Y c= Seg k
        proof
          let x be object;
          assume
A14:      x in Y;
          then
A15:      x in X;
A16:      not x in {k+1} by A14,XBOOLE_0:def 5;
A17:      x in Seg(k+1) by A6,A15;
A18:      x<>k+1 by A16,TARSKI:def 1;
          reconsider m=x as Element of NAT by A17;
A19:      m <= k+1 by A6,A15,Th1;
A20:      1 <= m by A6,A15,Th1;
          m <= k by A18,A19,NAT_1:8;
          hence thesis by A20;
        end;
        then consider p being FinSequence of NAT such that
A21:    rng p = Y and
A22:    for l,m,k1,k2 be Nat st 1 <= l & l < m & m <= len p & k1=p.l & k2
        =p.m holds k1 < k2
        by A5;
        consider q such that
A23:    q=p^<*k+1*>;
        reconsider q as FinSequence of NAT by A23;
A24:    rng q = rng p \/ rng <*k+1*> by A23,Th31
          .= Y \/ {k+1} by A21,Th38
          .= X \/ {k+1} by XBOOLE_1:39
          .= X by A7,A9,XBOOLE_1:12,ZFMISC_1:31;
        for l,m,k1,k2 be Nat st 1 <= l & l < m & m <= len q &
        k1=q.l & k2=q.m holds k1 < k2
        proof
          let l,m,k1,k2 be Nat;
          assume that
A25:      1 <= l and
A26:      l < m and
A27:      m <= len q and
A28:      k1=q.l and
A29:      k2=q.m;
          l < len (p^<*k+1*>) by A23,A26,A27,XXREAL_0:2;
          then l < len p + len <*k+1*> by Th22;
          then l < len p + 1 by Th39;
          then l <= len p by NAT_1:13;
          then l in Seg len p by A25;
          then
A30:      l in dom p by Def3;
A31:      1 <= m by A25,A26,XXREAL_0:2;
A32:      now
            assume
A33:        m=len q;
            k1 = p.l by A23,A28,A30,Def7;
            then k1 in Y by A21,A30,FUNCT_1:def 3;
            then
A34:        k1 <= k by A13,Th1;
            q.m = (p^<*k+1*>).(len p + len <*k+1*>) by A23,A33,Th22
              .=(p^<*k+1*>).(len p + 1) by Th39
              .= k+1 by Th42;
            hence thesis by A29,A34,NAT_1:13;
          end;
          now
            assume m <> len q;
            then m < len (p^<*k+1*>) by A23,A27,XXREAL_0:1;
            then m < len p + len <*k+1*> by Th22;
            then m < len p + 1 by Th39;
            then
A35:        m <= len p by NAT_1:13;
            then m in Seg len p by A31;
            then m in dom p by Def3;
            then
A36:        k2 = p.m by A23,A29,Def7;
            k1 = p.l by A23,A28,A30,Def7;
            hence thesis by A22,A25,A26,A35,A36;
          end;
          hence thesis by A32;
        end;
        hence thesis by A24;
      end;
      hence thesis by A5;
    end;
    for k being Nat holds P[k] from NAT_1:sch 2(A2,A4);
    hence thesis by A1;
  end;
  uniqueness
  proof
    let p,q be FinSequence of NAT such that
    A37: (
 rng p = X & for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len p & k1=p.
l & k2=p.m holds k1 < k2 )&( rng q = X & for l,m,k1,k2 being Nat st 1 <= l &
    l < m & m <= len q & k1=q.l & k2=q.m holds k1 < k2 );
    defpred S[FinSequence] means for X st ex k being Nat st X c= Seg k holds
    ($1 is FinSequence of NAT & rng $1 = X &
    for l,m,k1,k2 being Nat st ( 1 <= l & l < m & m <= len $1 &
    k1=$1.l & k2=$1.m) holds k1 < k2) implies
    for q being FinSequence of NAT st rng q = X &
    for l,m,k1,k2 being Nat st ( 1 <= l & l < m & m <= len q &
    k1=q.l & k2=q.m) holds k1 < k2 holds q=$1;
A38: S[{}];
A39: for p,x st S[p] holds S[p^<*x*>]
    proof
      let p,x;
      assume
A40:  S[p];
      let X;
      given k being Nat such that
A41:  X c= Seg k;
      assume that
A42:  p^<*x*> is FinSequence of NAT and
A43:  rng (p^<*x*>) = X and
A44:  for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len(p^<*x*>) &
      k1=(p^<*x*>).l & k2=(p^<*x*>).m holds k1 < k2;
      let q be FinSequence of NAT;
      assume that
A45:  rng q = X and
A46:  for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len q & k1=q.l &
      k2=q.m holds k1 < k2;
      1 in Seg 1;
      then
A47:  1 in dom <*x*> by Def8;
A48:  ex m st m=x & for l st l in X & l <> x holds l < m
      proof
        <*x*> is FinSequence of NAT by A42,Th36;
        then rng <*x*> c= NAT by Def4;
        then {x} c= NAT by Th38;
        then reconsider m=x as Element of NAT by ZFMISC_1:31;
        take m;
        thus m=x;
        thus for l st l in X & l <> x holds l < m
        proof
          let l;
          assume that
A49:      l in X and
A50:      l <> x;
          consider y being object such that
A51:      y in dom (p^<*x*>) and
A52:      l=(p^<*x*>).y by A43,A49,FUNCT_1:def 3;
A53:      y in Seg len (p^<*x*>) by A51,Def3;
          reconsider k=y as Element of NAT by A51;
          k <= len (p^<*x*>) by A53,Th1;
          then k <= len p + len <*x*> by Th22;
          then
A54:      k <= len p + 1 by Th39;
A55:      k <> len p + 1
          proof
            assume k = len p + 1;
            then (p^<*x*>).k = <*x*>.1 by A47,Def7
              .= x by Def8;
            hence contradiction by A50,A52;
          end;
A56:      1 <= k by A53,Th1;
          k < len p + 1 by A54,A55,XXREAL_0:1;
          then k < len p + len <*x*> by Th39;
          then
A57:      k < len(p^<*x*>) by Th22;
          m=(p^<*x*>).(len p + 1) by Th42
            .= (p^<*x*>).(len p + len <*x*>) by Th39
            .= (p^<*x*>).(len(p^<*x*>)) by Th22;
          hence thesis by A44,A52,A56,A57;
        end;
      end;
      then reconsider m = x as Nat;
      len q <> 0
      proof
        assume len q = 0;
        then p^<*x*> = {} by A43,A45,Lm3,RELAT_1:38;
        then 0 = len (p^<*x*>) .= len p + len <*x*> by Th22
          .= 1 + len p by Th39;
        hence contradiction;
      end;
      then consider n be Nat such that
A58:  len q = n+1 by NAT_1:6;
      deffunc F(Nat) = q.$1;
      ex q9 being FinSequence st len q9 = n &
      for m st m in dom q9 holds q9.m = F(m) from SeqLambda;
      then consider q9 being FinSequence such that
A59:  len q9 = n and
A60:  for m st m in dom q9 holds q9.m = q.m;
      now
        let x be object;
        assume x in rng q9;
        then consider y being object such that
A61:    y in dom q9 and
A62:    x=q9.y by FUNCT_1:def 3;
A63:    y in Seg len q9 by A61,Def3;
        reconsider y as Element of NAT by A61;
A64:    y <= n by A59,A63,Th1;
A65:    n <= n + 1 by NAT_1:11;
A66:    1 <= y by A63,Th1;
        y <= n+1 by A64,A65,XXREAL_0:2;
        then y in Seg (n+1) by A66;
        then y in dom q by A58,Def3;
        then
A67:    q.y in rng q by FUNCT_1:def 3;
        rng q c= NAT by Def4;
        then q.y in NAT by A67;
        hence x in NAT by A60,A61,A62;
      end;
      then reconsider f=q9 as FinSequence of NAT by Def4,TARSKI:def 3;
A68:  dom q = Seg (n+1) by A58,Def3
        .= Seg (len q9 + len <*x*>) by A59,Th39;
A69:  for m st m in dom <*x*> holds q.(len q9 + m) = <*x*>.m
      proof
        let m;
        assume m in dom <*x*>;
        then
A70:    m in {1} by Def8,Th2;
        then
A71:    m=1 by TARSKI:def 1;
        q.(len q9 + m) = x
        proof
          assume q.(len q9 + m) <> x;
          then
A72:      q.len q <> x by A58,A59,A70,TARSKI:def 1;
          consider d being Nat such that
A73:      d=x and
A74:      for l st l in X & l<>x holds l<d by A48;
          x in {x} by TARSKI:def 1;
          then x in rng <*x*> by Th38;
          then x in rng p \/ rng <*x*> by XBOOLE_0:def 3;
          then x in rng q by A43,A45,Th31;
          then consider y being object such that
A75:      y in dom q and
A76:      x=q.y by FUNCT_1:def 3;
A77:      y in Seg len q by A75,Def3;
          reconsider y as Element of NAT by A75;
A78:      1 <= y by A77,Th1;
A79:      y <= len q by A77,Th1;
          then
A80:      y < len q by A72,A76,XXREAL_0:1;
          1 <= len q by A78,A79,XXREAL_0:2;
          then len q in Seg len q;
          then
A81:      len q in dom q by Def3;
A82:      q.len q in X by A45,A81,FUNCT_1:def 3;
          reconsider k = q.len q as Nat;
          k < d by A72,A74,A82;
          hence contradiction by A46,A73,A76,A78,A80;
        end;
        hence thesis by A71,Th40;
      end;
      then
A83:  q9^<*x*> = q by A60,A68,Def7;
A84:  not x in rng p
      proof
        assume x in rng p;
        then consider y being object such that
A85:    y in dom p and
A86:    x=p.y by FUNCT_1:def 3;
A87:    y in Seg len p by A85,Def3;
        reconsider y as Element of NAT by A85;
A88:    y <= len p by A87,Th1;
A89:    len p + 1 = len p + len <*x*> by Th39
          .= len (p^<*x*>) by Th22;
A90:    1 <= y by A87,Th1;
A91:    y < len p + 1 by A88,NAT_1:13;
A92:    m = (p^<*x*>).y by A85,A86,Def7;
        m = (p^<*x*>).(len p + 1 ) by Th42;
        hence contradiction by A44,A89,A90,A91,A92;
      end;
A93:  X = rng p \/ rng <*x*> by A43,Th31
        .= rng p \/ {x} by Th39;
A94:  for z being object holds z in rng p \/ {x} \ {x} iff z in rng p
      proof
        let z be object;
        thus z in rng p \/ {x} \ {x} implies z in rng p
        proof
          assume
A95:      z in rng p \/ {x} \ {x};
          then not z in {x} by XBOOLE_0:def 5;
          hence thesis by A95,XBOOLE_0:def 3;
        end;
        assume z in rng p;
        then
        ( not z in {x})& z in rng p \/ {x} by A84,TARSKI:def 1,XBOOLE_0:def 3;
        hence thesis by XBOOLE_0:def 5;
      end;
A96: for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len p &
      k1=p.l & k2=p.m holds k1 < k2
      proof
        let l,m,k1,k2 be Nat;
        assume that
A97:   1 <= l and
A98:   l < m and
A99:   m <= len p and
A100:   k1=p.l and
A101:   k2=p.m;
        l <= len p by A98,A99,XXREAL_0:2;
        then l in Seg len p by A97;
        then l in dom p by Def3;
        then
A102:   k1 = (p^<*x*>).l by A100,Def7;
        1 <= m by A97,A98,XXREAL_0:2;
        then m in Seg len p by A99;
        then m in dom p by Def3;
        then
A103:   k2 = (p^<*x*>).m by A101,Def7;
        len p <= len p + 1 by NAT_1:11;
        then m <= len p + 1 by A99,XXREAL_0:2;
        then m <= len p + len <*x*> by Th39;
        then m <= len (p^<*x*>) by Th22;
        hence thesis by A44,A97,A98,A102,A103;
      end;
A104: p is FinSequence of NAT by A42,Th36;
A105: rng p = X\{x} by A93,A94,TARSKI:2;
A106: not x in rng f
      proof
        assume x in rng f;
        then consider y being object such that
A107:   y in dom f and
A108:   x=f.y by FUNCT_1:def 3;
A109:   y in Seg len f by A107,Def3;
        reconsider y as Element of NAT by A107;
A110:   y <= len f by A109,Th1;
A111:   len f + 1 = len f + len <*x*> by Th39
          .= len (f^<*x*>) by Th22;
A112:   1 <= y by A109,Th1;
A113:   y < len f + 1 by A110,NAT_1:13;
A114:   m = q.y by A60,A107,A108;
        m = q.(len f + 1) by A83,Th42;
        hence contradiction by A46,A83,A111,A112,A113,A114;
      end;
A115: X = rng f \/ rng <*x*> by A45,A83,Th31
        .= rng f \/ {x} by Th39;
A116: for z being object holds z in rng f \/ {x} \ {x} iff z in rng f
      proof
        let z be object;
        thus z in rng f \/ {x} \ {x} implies z in rng f
        proof
          assume
A117:     z in rng f \/ {x} \ {x};
          then not z in {x} by XBOOLE_0:def 5;
          hence thesis by A117,XBOOLE_0:def 3;
        end;
        assume z in rng f;
        then
        ( not z in {x})& z in rng f \/ {x} by A106,TARSKI:def 1,XBOOLE_0:def 3;
        hence thesis by XBOOLE_0:def 5;
      end;
      A118: for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len f &
      k1=f.l & k2=f.m holds k1 < k2
      proof
        let l,m,k1,k2 be Nat;
        assume that
A119:   1 <= l and
A120:   l < m and
A121:   m <= len f and
A122:   k1=f.l and
A123:   k2=f.m;
A124:   m <= len q by A58,A59,A121,NAT_1:13;
        l <= n by A59,A120,A121,XXREAL_0:2;
        then
A125:   l in Seg n by A119;
        1 <= m by A119,A120,XXREAL_0:2;
        then
A126:   m in Seg n by A59,A121;
A127:   l in dom q9 by A59,A125,Def3;
A128:   m in dom q9 by A59,A126,Def3;
A129:   k1 = q.l by A60,A122,A127;
        k2 = q.m by A60,A123,A128;
        hence thesis by A46,A119,A120,A124,A129;
      end;
      rng f = X\{x} by A115,A116,TARSKI:2;
      then q9 = p by A40,A41,A96,A104,A105,A118,XBOOLE_1:1;
      hence thesis by A60,A68,A69,Def7;
    end;
    for p holds S[p] from IndSeq(A38,A39);
    hence thesis by A1,A37;
  end;
end;

theorem Th50:
  rng Sgm dom p9 = dom p9
proof
  ex k st dom p9 c= Seg k by Def12;
  hence thesis by Def13;
end;

definition
  let p9;
  func Seq p9 -> Function equals
  p9* Sgm(dom p9);
  coherence;
end;

registration
  let p9;
  cluster Seq p9 -> FinSequence-like;
  coherence
  proof
    rng Sgm dom p9 = dom p9 by Th50;
    then dom(p9*Sgm(dom p9)) = dom Sgm dom p9 by RELAT_1:27
      .=Seg len Sgm dom p9 by Def3;
    hence thesis;
  end;
end;

theorem
  for X st ex k st X c= Seg k holds Sgm X = {} iff X = {}
proof
  let X;
  given k such that
A1: X c= Seg k;
  thus Sgm X = {} implies X = {}
  proof
    assume Sgm X = {};
    hence X = rng {} by A1,Def13
      .= {};
  end;
  assume X={};
  then rng Sgm X = {} by A1,Def13;
  hence thesis;
end;

begin :: from FINSET_1, 1998

theorem :: FINSET_1:def 1
  D is finite iff ex p st D = rng p
proof
  thus D is finite implies ex p st D = rng p
  proof
    given g being Function such that
A1: rng g = D and
A2: dom g in omega;
    reconsider n = dom g as Element of NAT by A2;
    defpred R[object,object] means P[$2,$1];
A3: for x being object st x in Seg n ex y being object st R[x,y]
    proof
      let x be object;
      assume
A4:   x in Seg n;
      then reconsider x as Element of NAT;
      x >= 1 by A4,Th1;
      then ex k be Nat st x = 1+k by NAT_1:10;
      hence thesis;
    end;
    consider f such that
A5: dom f = Seg n and
A6: for x being object st x in Seg n holds R[x,f.x] from CLASSES1:sch 1(A3);
A7: rng f = dom g
    proof
A8:   n = { k where k is Nat: k < n } by AXIOMS:4;
      thus rng f c= dom g
      proof
        let x be object;
        assume x in rng f;
        then consider y being object such that
A9:     y in dom f and
A10:    x = f.y by FUNCT_1:def 3;
        consider k such that
A11:    x = k and
A12:    y = k+1 by A5,A6,A9,A10;
        k + 1 <= n by A5,A9,A12,Th1;
        then k < n by NAT_1:13;
        hence thesis by A8,A11;
      end;
      let x be object;
      assume x in dom g;
      then consider k being Nat such that
A13:  x = k and
A14:  k < n by A8;
      1 <= k+1 & k+1 <= n by A14,NAT_1:11,13;
      then
A15:  k+1 in Seg n;
      then ex k1 st f.(k+1) = k1 & k+1 = k1+1 by A6;
      hence thesis by A5,A13,A15,FUNCT_1:def 3;
    end;
    then dom(g*f) = Seg n by A5,RELAT_1:27;
    then reconsider p = g*f as FinSequence by Def2;
    take p;
    thus thesis by A1,A7,RELAT_1:28;
  end;
  given p such that
A16: D = rng p;
  consider n such that
A17: dom p = Seg n by Def2;
A18: n = { k where k is Nat: k < n } by AXIOMS:4;
A19: for x being object st x in n ex y being object st P[x,y]
  proof
    let x be object;
    assume x in n;
    then ex k being Nat st x = k & k < n by A18;
    then reconsider k = x as Nat;
    take k+1;
    thus thesis;
  end;
  consider f such that
A20: dom f = n and
A21: for x being object st x in n holds P[x,f.x] from CLASSES1:sch 1(A19);
  take p*f;
A22: rng f = dom p
  proof
    thus rng f c= dom p
    proof
      let x be object;
      assume x in rng f;
      then consider y being object such that
A23:  y in dom f and
A24:  x = f.y by FUNCT_1:def 3;
      consider k such that
A25:  y = k and
A26:  x = k+1 by A20,A21,A23,A24;
      ex m being Nat st k = m & m < n by A18,A20,A23,A25;
      then 1 <= k+1 & k+1 <= n by NAT_1:11,13;
      hence thesis by A17,A26;
    end;
    let x be object;
    assume
A27: x in dom p;
    then reconsider x as Element of NAT;
    1 <= x by A17,A27,Th1;
    then consider m be Nat such that
A28: x = 1+m by NAT_1:10;
    x <= n by A17,A27,Th1;
    then m < n by A28,NAT_1:13;
    then
A29: m in n by A18;
    then ex k st m = k & f.m = k+1 by A21;
    hence thesis by A20,A28,A29,FUNCT_1:def 3;
  end;
  hence rng(p*f) = D by A16,RELAT_1:28;
  dom(p*f) = dom f by A22,RELAT_1:27;
  hence thesis by A20,ORDINAL1:def 12;
end;

begin :: Moved from CARD_1, 1999

theorem
  Seg n,Seg m are_equipotent implies n = m
proof
  defpred P[Nat] means ex n st Seg n,Seg $1 are_equipotent & n <> $1;
  assume Seg n,Seg m are_equipotent & n <> m;
  then
A1: ex m being Nat st P[m];
  consider m being Nat such that
A2: P[m] and
A3: for k being Nat st P[k] holds m <= k from NAT_1:sch 5(A1);
  consider n such that
A4: Seg n,Seg m are_equipotent and
A5: n <> m by A2;
A6: ex f st
  f is one-to-one & dom f = Seg n & rng f = Seg m by A4;
A7: now
    assume m = 0;
    then Seg m = {};
    then Seg m = Seg n by A6,RELAT_1:42;
    hence contradiction by A5,Th6;
  end;
  then consider m1 being Nat such that
A8: m = m1+1 by NAT_1:6;
A9: now
    assume n = 0;
    then Seg n = {};
    then Seg m = Seg n by A6,RELAT_1:42;
    hence contradiction by A5,Th6;
  end;
  then consider n1 being Nat such that
A10: n = n1+1 by NAT_1:6;
A11: n in Seg n by A9,Th3;
A12: m in Seg m by A7,Th3;
A13: not n1+1 <= n1 by NAT_1:13;
A14: not m1+1 <= m1 by NAT_1:13;
A15: not n in Seg n1 by A10,A13,Th1;
A16: not m in Seg m1 by A8,A14,Th1;
A17: (Seg n1) /\ { n } c= {}
  proof
    let x be object;
    assume x in (Seg n1) /\ { n };
    then x in Seg n1 & x in { n } by XBOOLE_0:def 4;
    hence thesis by A15,TARSKI:def 1;
  end;
A18: (Seg m1) /\ { m } c= {}
  proof
    let x be object;
    assume x in (Seg m1) /\ { m };
    then x in Seg m1 & x in { m } by XBOOLE_0:def 4;
    hence thesis by A16,TARSKI:def 1;
  end;
A19: Seg n = (Seg n1) \/ { n } by A10,Th9;
A20: Seg m = (Seg m1) \/ { m } by A8,Th9;
A21: (Seg n1) /\ { n } = {} by A17;
A22: (Seg m1) /\ { m } = {} by A18;
  A23: (
Seg n1) \ { n } = ((Seg n1) \/ { n }) \ { n } & (Seg n1) misses { n } by A21,
XBOOLE_1:40;
  A24: (
Seg m1) \ { m } = ((Seg m1) \/ { m }) \ { m } & (Seg m1) misses { m } by A22,
XBOOLE_1:40;
A25: (Seg n) \ { n } = Seg n1 by A19,A23,XBOOLE_1:83;
  (Seg m) \ { m } = Seg m1 by A20,A24,XBOOLE_1:83;
  hence contradiction by A3,A4,A5,A8,A10,A11,A12,A14,A25,CARD_1:34;
end;

theorem
  Seg n,n are_equipotent by Lm1;

theorem
  card Seg n = card n by Lm1,CARD_1:5;

theorem Th56:
  X is finite implies ex n st X,Seg n are_equipotent
proof
  assume X is finite;
  then reconsider n = card X as Nat;
A1: X,n are_equipotent by CARD_1:def 2;
  take n;
  n,Seg n are_equipotent by Lm1;
  hence thesis by A1,WELLORD2:15;
end;

theorem
  for n being Nat holds card Seg n = n by Lm1,CARD_1:def 2;

begin :: Addenda
:: from FINSEQ_5

registration
  let x be object;
  cluster <*x*> -> non empty;
  coherence;
end;

:: From SPRECT_1

registration
  cluster non empty for FinSequence;
  existence
  proof
    take <* 0 *>;
    thus thesis;
  end;
end;

:: From FUNCT_7, actually from GOBOARD4

registration
  let f1 be FinSequence, f2 be non empty FinSequence;
  cluster f1^f2 -> non empty;
  coherence by Th35;
  cluster f2^f1 -> non empty;
  coherence by Th35;
end;

registration
  let x,y be object;
  cluster <*x,y*> -> non empty;
  coherence;
  let z be object;
  cluster <*x,y,z*> -> non empty;
  coherence;
end;

:: from MATRIX_2

scheme SeqDEx{D()->non empty set,A()->Nat,P[object,object]}:
  ex p being FinSequence of D() st dom p = Seg A() &
  for k st k in Seg A() holds P[k,p.k]
provided
A1: for k st k in Seg A() ex x being Element of D() st P[k,x]
proof
A2: for y be object st y in Seg A() ex x being object st x in D() & P[y,x]
  proof
    let y be object;
    assume
A3: y in Seg A();
    then reconsider k=y as Element of NAT;
    consider x being Element of D() such that
A4: P[k,x] by A1,A3;
    take x;
    thus thesis by A4;
  end;
  consider f being Function such that
A5: dom f = Seg A() and
A6: rng f c= D() and
A7: for y be object st y in Seg A() holds P[y,f.y] from FUNCT_1:sch 6(A2);
  reconsider f as FinSequence by A5,Def2;
  reconsider p=f as FinSequence of D() by A6,Def4;
  take p;
  thus thesis by A5,A7;
end;

:: from TOPREAL1

reserve D for set,
  p for FinSequence of D,
  m for Nat;

definition
  let m;
  let p be FinSequence;
  func p|m -> FinSequence equals
  p|Seg m;
  coherence by Th15;
end;

definition
  let D,m,p;
  redefine func p|m -> FinSequence of D;
  coherence by Th18;
end;

registration
  let f be FinSequence;
  cluster f|0 -> empty;
  coherence;
end;

theorem Th58:
  len q <= i implies q|i = q
proof
  assume len q <= i;
  then Seg len q c= Seg i by Th5;
  then dom q c= Seg i by Def3;
  hence thesis by RELAT_1:68;
end;

theorem Th59:
  i <= len q implies len(q|i) = i
proof
  assume i <= len q;
  then Seg i c= Seg(len q) by Th5;
  then Seg i c= dom q by Def3;
  then i in NAT & Seg i = dom(q|i) by ORDINAL1:def 12,RELAT_1:62;
  hence thesis by Def3;
end;

registration
  let f be non empty FinSequence;
  reduce len (f|1) to 1;
  reducibility
  proof
    1 <= len f by NAT_1:14;
    hence thesis by Th59;
  end;
  cluster f|1 -> 1-element;
  coherence;
end;

registration
  let p be non empty FinSequence, n be non zero Nat;
  cluster p|n -> non empty;
  coherence
  proof
    per cases;
    suppose n <= len p;
      then n+1-1 <= len p - 0;
      then len(p|n) = n by Th59;
      hence thesis;
    end;
    suppose len p <= n;
      hence thesis by Th58;
    end;
  end;
end;

:: from FSM_1

theorem
  i in Seg n implies i+m in Seg (n+m)
proof
  assume
A1: i in Seg n;
  then
A2: 1 <= i by Th1;
A3: i <= n by A1,Th1;
  i <= i+m by NAT_1:11;
  then 1 <= i+m by A2,XXREAL_0:2;
  hence thesis by A3,Th1,XREAL_1:7;
end;

theorem
  i>0 & i+m in Seg (n+m) implies i in Seg n & i in Seg (n+m)
proof
  assume that
A1: i > 0 and
A2: i+m in Seg (n+m);
  1 = 0+1;
  then
A3: 1 <= i by A1,NAT_1:13;
A4: i+m <= n+m by A2,Th1;
  i <= n by A2,Th1,XREAL_1:6;
  hence i in Seg n by A3;
  i <= i+m by NAT_1:11;
  then i <= n+m by A4,XXREAL_0:2;
  hence thesis by A3;
end;

:: from LANG1

definition
  let R be Relation;
  func R[*] -> Relation means
  for x,y being object holds [x,y] in it iff x in field R & y in field R &
  ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y &
  for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R;
  existence
  proof
    defpred X[object,object] means
    ex p being FinSequence st len p >= 1 & p.1 = $1 & p.(len p) = $2 &
    for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R;
    thus ex S being Relation st for x,y being object holds
    [x,y] in S iff x in field R & y in field R & X[x,y] from RELAT_1:sch 1;
  end;
  uniqueness
  proof
    let R1,R2 be Relation such that
A1: for x,y being object holds [x,y] in R1 iff x in field R & y in field R &
    ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y &
    for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R and
A2: for x,y being object holds [x,y] in R2 iff x in field R & y in field R &
    ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y &
    for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R;
    let x,y be object;
    thus [x,y] in R1 implies [x,y] in R2
    proof
      assume
A3:   [x,y] in R1;
      then
A4:   x in field R & y in field R by A1;
      ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y & for i
      being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R by A1,A3;
      hence thesis by A2,A4;
    end;
    assume
A5: [x,y] in R2;
    then
A6: x in field R & y in field R by A2;
    ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y & for i
    being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R by A2,A5;
    hence thesis by A1,A6;
  end;
end;

theorem
  for D1,D2 being set st D1 c= D2 holds D1* c= D2*
proof
  let D1,D2 be set such that
A1: D1 c= D2;
  let x be object;
  assume x in D1*;
  then reconsider p = x as FinSequence of D1 by Def11;
  rng p c= D1 by Def4;
  then x is FinSequence of D2 by Def4,A1,XBOOLE_1:1;
  hence thesis by Def11;
end;

:: 2005.05.13, A.T.

registration
  let D be set;
  cluster D* -> functional;
  coherence
  by Def11;
end;

:: from SCMFSA_7, 2005.11.21, A.T.

theorem
  for p,q being FinSequence st p c= q holds len p <= len q
  proof let p,q be FinSequence;
   assume p c= q;
    then Segm card p c= Segm card q by CARD_1:11;
   hence thesis by NAT_1:39;
  end;

theorem
  for p,q being FinSequence, i being Nat st
  1 <= i & i <= len p holds (p ^ q).i = p.i
proof
  let p,q be FinSequence, i be Nat;
  assume
A1: 1 <= i & i <= len p;
  i in NAT & Seg len p = dom p by Def3,ORDINAL1:def 12;
  then i in dom p by A1;
  hence thesis by Def7;
end;

theorem
  for p,q being FinSequence, i being Nat st
  1 <= i & i <= len q holds (p ^ q).(len p + i) = q.i
proof
  let p,q be FinSequence, i be Nat;
  assume 1 <= i & i <= len q;
  then
  len p + 1 <= len p + i & len p + i <= len p + len q by XREAL_1:6;
  hence (p ^ q).(len p + i) = q.(len p + i - len p) by Th23
    .= q.i;
end;

:: from GRAPH_2, 2006.01.09, A.T.

scheme FinSegRng{n() -> Nat, F(set)->set, P[set]}:
  {F(i) where i is Nat: i<=n() & P[i]} is finite
proof
  set F = {F(i) where i is Nat: i<=n() & P[i]};
  deffunc G(Nat) = F($1-1);
  consider f being FinSequence such that
A1: len f = n()+1 and
A2: for k st k in dom f holds f.k = G(k) from SeqLambda;
  F c= rng f
  proof
    let x be object;
    assume x in F;
    then consider j being Nat such that
A3: x=F(j) and
A4: j<=n() and P[j];
    1<=j+1 & j+1<=n()+1 by A4,NAT_1:11,XREAL_1:6;
    then j+1 in Seg (n()+1);
    then
A5: j+1 in dom f by A1,Def3;
    then f.(j+1) = F(j+1-1) by A2
      .= F(j);
    hence thesis by A3,A5,FUNCT_1:def 3;
  end;
  hence thesis;
end;

Lm5: x in Seg n implies x = 1 or ... or x = n
  proof assume
A1:  x in Seg n;
    then reconsider k = x as Nat;
    1 <= k & k <= n by A1,Th1;
   hence thesis;
  end;

theorem Th66:
  for x1, x2, x3, x4 being set, p being FinSequence
  st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>
  holds len p = 4 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4
proof
  let x1, x2, x3, x4 be set, p be FinSequence;
  assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>;
  set p13 = <*x1*>^<*x2*>^<*x3*>;
A2: p13 = <*x1, x2, x3*>;
  then
A3: len p13 = 3 by Th45;
A4: p13.1 = x1 & p13.2 = x2 by A2,Th45;
A5: p13.3 = x3 by A2,Th45;
  thus len p = len p13 + len <*x4*> by A1,Th22
    .= 3 + 1 by A3,Th40
    .= 4;
A6: dom p13 = Seg 3 by A3,Def3;
   1 in Seg 3 & ...& 3 in Seg 3;
  hence p.1 = x1 & p.2 = x2 & p.3 = x3 by A1,A4,A5,Def7,A6;
  thus p.4 = p.(len p13 + 1) by A3
    .= x4 by A1,Th42;
end;

theorem Th67:
  for x1, x2, x3, x4, x5 being set, p being FinSequence
  st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>
  holds len p = 5 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5
proof
  let x1, x2, x3, x4, x5 be set, p be FinSequence;
  assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>;
  set p14 = <*x1*>^<*x2*>^<*x3*>^<*x4*>;
A2: len p14 = 4 by Th66;
A3: p14.1 = x1 & p14.2 = x2 by Th66;
A4: p14.3 = x3 & p14.4 = x4 by Th66;
  thus len p = len p14 + len <*x5*> by A1,Th22
    .= 4 + 1 by A2,Th40
    .= 5;
A5:  dom p14 = Seg 4 by A2,Def3;
   1 in Seg 4 & ...& 4 in Seg 4;
  hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 by A1,A3,A4,Def7,A5;
  thus p.5 = p.(len p14 + 1) by A2
    .= x5 by A1,Th42;
end;

theorem Th68:
  for x1, x2, x3, x4, x5, x6 being set, p being FinSequence
  st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>
  holds len p = 6 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
  p.6 = x6
proof
  let x1, x2, x3, x4, x5, x6 be set, p be FinSequence;
  assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>;
  set p15 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>;
A2: len p15 = 5 by Th67;
A3: p15.1 = x1 & p15.2 = x2 by Th67;
A4: p15.3 = x3 & p15.4 = x4 by Th67;
A5: p15.5 = x5 by Th67;
  thus len p = len p15 + len <*x6*> by A1,Th22
    .= 5 + 1 by A2,Th40
    .= 6;
A6:  dom p15 = Seg 5 by A2,Def3;
   1 in Seg 5 & ...& 5 in Seg 5;
  hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5
  by A1,A3,A4,A5,Def7,A6;
  thus p.6 = p.(len p15 + 1) by A2
    .= x6 by A1,Th42;
end;

theorem Th69:
  for x1, x2, x3, x4, x5, x6, x7 being set, p being FinSequence
  st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>
  holds len p = 7 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
  p.6 = x6 & p.7 = x7
proof
  let x1, x2, x3, x4, x5, x6, x7 be set, p be FinSequence;
  assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>;
  set p16 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>;
A2: len p16 = 6 by Th68;
A3: p16.1 = x1 & p16.2 = x2 by Th68;
A4: p16.3 = x3 & p16.4 = x4 by Th68;
A5: p16.5 = x5 & p16.6 = x6 by Th68;
  thus len p = len p16 + len <*x7*> by A1,Th22
    .= 6 + 1 by A2,Th40
    .= 7;
A6: dom p16 = Seg 6 by A2,Def3;
   1 in Seg 6 & ...& 6 in Seg 6;
  hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6
  by A1,A3,A4,A5,Def7,A6;
  thus p.7 = p.(len p16 + 1) by A2
    .= x7 by A1,Th42;
end;

theorem Th70:
  for x1,x2,x3,x4, x5, x6, x7, x8 being set, p being FinSequence
  st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>
  holds len p = 8 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
  p.6 = x6 & p.7 = x7 & p.8 = x8
proof
  let x1, x2, x3, x4, x5, x6, x7, x8 be set, p be FinSequence;
  thus p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>
  implies len p = 8 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
  p.6 = x6 & p.7 = x7 & p.8 = x8
  proof
  assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>;
  set p17 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>;
A2: len p17 = 7 by Th69;
A3: p17.1 = x1 & p17.2 = x2 by Th69;
A4: p17.3 = x3 & p17.4 = x4 by Th69;
A5: p17.5 = x5 & p17.6 = x6 by Th69;
A6: p17.7 = x7 by Th69;
  thus len p = len p17 + len <*x8*> by A1,Th22
    .= 7 + 1 by A2,Th40
    .= 8;
A7:  dom p17 = Seg 7 by A2,Def3;
   1 in Seg 7 & ...& 7 in Seg 7;
  hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 &
  p.7 = x7 by A1,A3,A4,A5,A6,Def7,A7;
  thus p.8 = p.(len p17 + 1) by A2
    .= x8 by A1,Th42;
  end;
end;

theorem
  for x1,x2,x3,x4,x5,x6,x7, x8, x9 being set, p being FinSequence
  st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>
  holds len p = 9 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
  p.6 = x6 & p.7 = x7 & p.8 = x8 & p.9 = x9
proof
  let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set, p be FinSequence;
  thus p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>
  implies len p = 9 & p.1 = x1 & p.2 = x2 & p.3 = x3&p.4 = x4&p.5 = x5 &
  p.6 = x6 & p.7 = x7 & p.8 = x8 & p.9 = x9
proof
assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>;
  set p17 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>;
A2: len p17 = 8 by Th70;
A3: p17.1 = x1 & p17.2 = x2 by Th70;
A4: p17.3 = x3 & p17.4 = x4 by Th70;
A5: p17.5 = x5 & p17.6 = x6 by Th70;
A6: p17.7 = x7 & p17.8 = x8 by Th70;
  thus len p = len p17 + len <*x9*> by A1,Th22
    .= 8 + 1 by A2,Th40
    .= 9;
A7:  dom p17 = Seg 8 by A2,Def3;
   1 in Seg 8 & ...& 8 in Seg 8;
  hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 &
  p.7 = x7 & p.8 = x8 by A1,A3,A4,A5,A6,Def7,A7;
  thus p.9 = p.(len p17 + 1) by A2
    .= x9 by A1,Th42;
end;
end;

:: from SCMFSA_7, 2006.03.14, A.T.

theorem
  for p being FinSequence holds p | Seg 0 = {};

theorem
  for f,g being FinSequence holds f | Seg 0 = g | Seg 0;

theorem
  for D being non empty set, x being Element of D holds
  <* x *> is FinSequence of D;

theorem
  for D being set, p,q being FinSequence of D holds p ^ q is FinSequence of D;

:: from GROUP_7, 2007.02.10, AK

reserve a, b, c, d, e, f for object;

theorem
  <*a*> = <*b*> implies a = b
proof
  assume
A1: <*a*> = <*b*>;
  thus a = <*a*>.1 by Def8
    .= b by A1,Def8;
end;

theorem
  <*a,b*> = <*c,d*> implies a = c & b = d
proof
  assume
A1: <*a,b*> = <*c,d*>;
  thus a = <*a,b*>.1 by Th44
    .= c by A1,Th44;
  thus b = <*a,b*>.2 by Th44
    .= d by A1,Th44;
end;

theorem
  <*a,b,c*> = <*d,e,f*> implies a = d & b = e & c = f
proof
  assume
A1: <*a,b,c*> = <*d,e,f*>;
  thus a = <*a,b,c*>.1 by Th45
    .= d by A1,Th45;
  thus b = <*a,b,c*>.2 by Th45
    .= e by A1,Th45;
  thus c = <*a,b,c*>.3 by Th45
    .= f by A1,Th45;
end;

:: from PRVECT_1, 2007.03.09, A.T

registration
  cluster non empty non-empty for FinSequence;
  existence
  proof
    take <*{{}}*>;
    thus <*{{}}*> is non empty;
    assume {} in rng <*{{}}*>;
    then {} in {{{}}} by Th38;
    hence contradiction by TARSKI:def 1;
  end;
end;

theorem Th79:
  for p,q being FinSequence st q = p|Seg n holds len q <= len p
proof
  let p,q be FinSequence;
  assume q = p|Seg n;
  then
A1: dom q = dom p /\ Seg n by RELAT_1:61;
  Seg len q = dom q & Seg len p = dom p by Def3;
  hence thesis by Th5,A1,XBOOLE_1:17;
end;

theorem
  for p,r being FinSequence st r = p|Seg n ex q being FinSequence st p = r^q
proof
  let p,r be FinSequence;
  assume
A1: r = p|Seg n;
  then consider m be Nat such that
A2: len p = len r + m by Th79,NAT_1:10;
  deffunc U(Nat) = p.(len r + $1);
  consider q being FinSequence such that
A3: len q = m & for k st k in dom q holds q.k = U(k) from SeqLambda;
  take q;
A4: len p = len(r^q) by A2,A3,Th22;
  now
    let k such that
A5: 1 <= k and
A6: k <= len p;
A7: now
      assume k <= len r;
      then
A8:   k in Seg len r by A5;
A9:  dom r = Seg len r by Def3;
      then (r^q).k = r.k by A8,Def7;
      hence p.k = (r^q).k by A1,A8,A9,FUNCT_1:47;
    end;
    now
      assume
A10:  not k <= len r;
      then consider j being Nat such that
A11:  k = len r + j by NAT_1:10;
      k-len r = j by A11;
      then
A12:  (r^q).k = q.j by A4,A6,A10,Th24;
      j <> 0 by A10,A11;
      then
A13:  0+1 <= j by NAT_1:13;
      j <= len q by A2,A3,A6,A11,XREAL_1:6;
      then j in Seg m by A3,A13;
      then j in dom q by A3,Def3;
      hence p.k = (r^q).k by A3,A11,A12;
    end;
    hence p.k = (r^q).k by A7;
  end;
  hence thesis by A4,Th14;
end;

:: from GOBOARD1, PRALG_1, 2007.04.06, A.T

registration
  let D be non empty set;
  cluster non empty for FinSequence of D;
  existence
  proof set x = the Element of D;
    take <*x*>;
    thus thesis;
  end;
end;

:: Added by AK, 2007.11.07

definition
  let p,q be FinSequence;
  redefine pred p = q means
  len p = len q & for k st 1 <= k & k <= len p holds p.k = q.k;
  compatibility by Th14;
end;

:: from GROEB_2, 2008.10.08, A.T.

theorem
  for x,y,z being object holds
  1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*>
proof
  let x,y,z be object;
  len <*x,y,z*> = 3 by Th45; then
  dom <*x,y,z*> = Seg 3 by Def3;
  hence thesis;
end;

theorem
  for p being FinSequence, n,m being Nat st m <= n holds p|n|m = p|m
                       by Th5,RELAT_1:74;

:: from CARD_5, 2008.10.08, A.T.

reserve m for Nat;

theorem
  Seg n = (n+1) \ {0}
proof
A1: n+1 = {m: m < n+1} by AXIOMS:4;
  thus Seg n c= (n+1) \ {0}
  proof
    let x be object;
    assume x in Seg n;
    then consider k being Nat such that
A2: x = k and
A3: 1 <= k and
A4: k <= n;
    k < n+1 by A4,NAT_1:13;
    then
A5: x in n+1 by A1,A2;
    not x in {0} by A2,A3,TARSKI:def 1;
    hence thesis by A5,XBOOLE_0:def 5;
  end;
  let x be object;
  assume
A6: x in (n+1) \ {0};
  then
A7: x in n+1;
A8: not x in {0} by A6,XBOOLE_0:def 5;
  consider m such that
A9: x = m and
A10: m < n+1 by A1,A7;
A11: x <> 0 by A8,TARSKI:def 1;
  0+1 = 1;
  then
A12: 1 <= m by A9,A11,NAT_1:13;
  m <= n by A10,NAT_1:13;
  hence thesis by A9,A12;
end;

:: from CIRCCOMB, 2009.03.27, A.T.

registration
  let n be natural Number;
  cluster n-element for FinSequence;
  existence
  proof
A1: n is Nat by TARSKI:1;
    set p = Seg n --> {};
    dom p = Seg n by FUNCOP_1:13;
    then reconsider p as FinSequence by A1,Def2;
    take p;
    Seg len p = dom p by Def3;
    hence len p = n by Th6,FUNCOP_1:13;
  end;
end;

:: from FACIRC_1, 2009.02.16, A.T.

registration
  let x be object;
  cluster <*x*> -> 1-element;
  coherence;
  let y be object;
  cluster <*x,y*> -> 2-element;
  coherence by Th44;
  let z be object;
  cluster <*x,y,z*> -> 3-element;
  coherence by Th45;
end;

:: new, 2009.08.24, A.T.

definition let X be set;
 attr X is FinSequence-membered means
:Def18: x in X implies x is FinSequence;
end;

registration
 cluster empty -> FinSequence-membered for set;
 coherence;
end;

registration
 cluster non empty FinSequence-membered for set;
 existence
  proof
   take X = {the FinSequence};
   thus X is non empty;
   let x;
   thus thesis by TARSKI:def 1;
  end;
end;

registration let X be set;
 cluster X* -> FinSequence-membered;
 coherence by Def11;
end;

theorem
 for f being Function st f in D* & x in dom f holds f.x in D
proof let f be Function such that
A1: f in D* and
A2: x in dom f;
  f is FinSequence of D by A1,Def11;
  then
A3:   rng f c= D by Def4;
  f.x in rng f by A2,FUNCT_1:3;
 hence f.x in D by A3;
end;

registration
 cluster FinSequence-membered -> functional for set;
 coherence;
end;

theorem
 for X being FinSequence-membered set ex Y being non empty set st X c= Y*
proof
 let X be FinSequence-membered set;
  set Z = {rng f where f is Element of X: f in X};
 take Y = succ union Z;
 let x be object;
 assume
A1: x in X;
  then reconsider x as FinSequence by Def18;
  rng x in {rng f where f is Element of X: f in X} by A1;
  then rng x c= Y by ORDINAL3:1,SETFAM_1:41;
  then x is FinSequence of Y by Def4;
 hence thesis by Def11;
end;

registration
  let X be FinSequence-membered set;
  cluster -> FinSequence-like for Element of X;
  coherence
  proof
    let e be Element of X;
    X is empty or X is non empty;
    hence thesis by Def18,SUBSET_1:def 1;
  end;
end;

registration let X be FinSequence-membered set;
 cluster -> FinSequence-membered for Subset of X;
 coherence;
end;

:: from TREES_1, 2009.09.09, A.T.

theorem
  for p,q being FinSequence st q = p|Seg n holds len q <= n
proof
  let p,q be FinSequence;
  assume q = p|Seg n;
then A1: dom q = dom p /\ Seg n by RELAT_1:61;
 Seg len q = dom q by Def3;
  hence thesis by Th5,A1,XBOOLE_1:17;
end;

theorem
  for p,q being FinSequence st p = p^q or p = q^p holds q = {}
proof
  let p,q be FinSequence such that
A1: p = p^q or p = q^p;
   len(p^q) = len p + len q & len(q^p) = len q + len p by Th22;
  hence thesis by A1;
end;

theorem
  for p,q being FinSequence st p^q = <*x*> holds
  p = <*x*> & q = {} or p = {} & q = <*x*>
proof
  let p,q be FinSequence;
  assume
A1: p^q = <*x*>;
then A2: 1 = len(p^q) by Th40
    .= len p + len q by Th22;
A3: now
    assume len p = 0;
    thus
then  p = {};
    hence q = <*x*> by A1,Th34;
  end;
 now
    assume len p <> 0;
then A4: 0+1 <= len p by NAT_1:13;
 len p <= 1 by A2,NAT_1:11;
then  len p = 1 by A4,XXREAL_0:1;
    thus
then  q = {} by A2;
    hence p = <*x*> by A1,Th34;
  end;
  hence thesis by A3;
end;

:: missing, 2009.09.26, A.T.

theorem Th88:
 for f being n-element FinSequence holds dom f = Seg n
  proof let f be n-element FinSequence;
    len f = n by CARD_1:def 7;
   hence dom f = Seg n by Def3;
  end;

registration let n,m be natural Number;
 let f be n-element FinSequence, g be m-element FinSequence;
 cluster f^g -> (n+m)-element;
 coherence
  proof
   len f = n & len g = m by CARD_1:def 7;
   hence len(f^g) = n+m by Th22;
  end;
end;

:: from JORDAN7, 2010.02.26, A.T

registration
  cluster increasing -> one-to-one for real-valued FinSequence;
  coherence
  proof
    let f be real-valued FinSequence;
    assume
A1: f is increasing;
    let x,y be object;
    assume that
A2: x in dom f & y in dom f and
A3: f.x=f.y;
    reconsider nx=x,ny=y as Element of NAT by A2;
    nx<=ny & nx>=ny by A1,A2,A3,VALUED_0:def 13;
    hence thesis by XXREAL_0:1;
  end;
end;

:: from AMI_6, 2010.04.07, A.T.

theorem
 for x, y being object st x in dom <*y*> holds x = 1
proof
  let x, y be object;
  assume x in dom <*y*>;
  then x in Seg 1 by Th38;
  hence thesis by Th2,TARSKI:def 1;
end;

:: from FOMODEL0, 2011.06.12, A.T.

registration let X;
 cluster X-valued for FinSequence;
 existence
  proof
   take <*>X;
   thus thesis;
  end;
end;

:: new, 2011.10.03, A.K.

registration
  let D be FinSequence-membered set;
  let f be D-valued Function;
  let x be object;
  cluster f.x -> FinSequence-like;
  coherence
  proof
    per cases;
    suppose x in dom f;
      then
A1:   f.x in rng f by FUNCT_1:def 3;
      rng f c= D by RELAT_1:def 19;
      hence thesis by A1;
    end;
    suppose not x in dom f;
      hence thesis by FUNCT_1:def 2;
    end;
  end;
end;

theorem
 x in Seg n implies x = 1 or ... or x = n by Lm5;

theorem
 dom <*x,y*> = { 1,2 }
 proof
  thus dom <*x,y*> = Seg len <*x,y*> by Def3
          .= {1,2} by Th2,Th44;
 end;


begin :: Fixed ordering of a finite set into a finite sequence

registration
  let A be finite set;
  cluster onto one-to-one for FinSequence of A;
 existence
  proof
   consider n such that
A1:  A,Seg n are_equipotent by Th56;
   consider f being Function such that
A2: f is one-to-one and
A3: dom f = Seg n and
A4: rng f = A by A1,WELLORD2:def 4;
   f is FinSequence by A3,Def2;
   then reconsider f as FinSequence of A by A4,Def4;
   take f;
   thus thesis by A2,A4,FUNCT_2:def 3;
  end;
end;

definition
  let A be finite set;
  func canFS A -> FinSequence equals
  the one-to-one onto FinSequence of A;
  coherence;
end;

definition
  let A be finite set;
  redefine func canFS A -> FinSequence of A;
  coherence;
end;

registration
  let A be finite set;
  cluster canFS A -> one-to-one onto for FinSequence of A;
  coherence;
end;

theorem Th92:
  for A being finite set holds len canFS A = card A
proof
  let A be finite set;
  thus card canFS A = card dom canFS A by CARD_1:62
         .= card rng canFS A by CARD_1:70
         .= card A by FUNCT_2:def 3;
end;

registration
  let A be finite non empty set;
  cluster canFS A -> non empty;
  coherence
  proof
    len canFS A = card A by Th92;
    hence thesis;
  end;
end;

theorem
  for a being object holds canFS({a}) = <* a *>
proof
  let a be object;
A1: rng canFS({a}) = {a} by FUNCT_2:def 3;
  len canFS({a}) = card {a} by Th92
    .= 1 by CARD_1:30;
  hence thesis by A1,Th39;
end;

theorem
  for A being finite set holds (canFS A)" is Function of A, Seg card A
proof
  let A be finite set;
  len canFS A = card A by Th92;
  then dom canFS A = Seg card A by Def3;
  then
A1: rng ((canFS A)") = Seg card A by FUNCT_1:33;
  rng canFS A = A by FUNCT_2:def 3;
  then dom ((canFS A)") = A by FUNCT_1:33;
  hence thesis by A1,FUNCT_2:1;
end;

:: from PNPROC_1, 2012.02.20, A.T.

theorem
  i > 0 implies {[i,x]} is FinSubsequence
proof
  assume
A1: i > 0;
A2: dom {[i,x]} = {i} by RELAT_1:9;
  {i} c= Seg i
  proof
    let x be object;
    assume x in {i};
    then x = i by TARSKI:def 1;
    hence thesis by A1,Th3;
  end;
  hence thesis by A2,Def12;
end;

Lm6: for p being FinSubsequence st Seq p = {} holds p = {}
proof
  let p be FinSubsequence such that
A1: Seq p = {};
  rng Sgm dom p = dom p by Th50;
  then dom {} = dom Sgm dom p by A1,RELAT_1:27;
  then Sgm dom p = {};
  then dom p = rng {} by Th50;
  hence thesis;
end;

theorem
  for q being FinSubsequence holds q = {} iff Seq q = {} by Lm6;

registration
  cluster -> finite for FinSubsequence;
  coherence
  proof
    let q be FinSubsequence;
    ex n being Nat st dom q c= Seg n by Def12;
    hence thesis by FINSET_1:10;
  end;
end;

reserve x1,x2,y1,y2 for set;

theorem
  {[x1,y1], [x2,y2]} is FinSequence implies x1 = 1 & x2 = 1 & y1 = y2 or
  x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1
proof
  assume {[x1,y1], [x2,y2]} is FinSequence;
  then reconsider p = {[x1,y1], [x2,y2]} as FinSequence;
A1: dom p = {x1,x2} by RELAT_1:10;
  then
A2: x1 in dom p by TARSKI:def 2;
A3: x2 in dom p by A1,TARSKI:def 2;
A4: [x1,y1] in p by TARSKI:def 2;
A5: [x2,y2] in p by TARSKI:def 2;
A6: p.x1 = y1 by A4,FUNCT_1:1;
A7: p.x2 = y2 by A5,FUNCT_1:1;
A8: dom p = Seg len p by Def3;
A9: len p <= 1+1 by CARD_2:50;
A10: len p >= 0 qua Nat+1 by NAT_1:13;
A11: now
    assume len p = 1;
    hence x1 = 1 & x2 = 1 by A2,A3,A8,Th2,TARSKI:def 1;
    hence y1 = y2 by A5,A6,FUNCT_1:1;
  end;
  now
    assume
A12: len p = 2;
A13: x1 = x2 implies p = {[x1,y1]} by A6,A7,ENUMSET1:29;
    x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1 or x1 = 1 & x2 = 1 or x1 = 2 & x2 = 2
    by A2,A3,A8,A12,Th2,TARSKI:def 2;
    hence x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1 by A12,A13,CARD_1:30;
  end;
  hence thesis by A9,A10,A11,NAT_1:9;
end;

theorem
  <*x1,x2*> = {[1,x1], [2,x2]}
proof
  reconsider f={[1,x1], [2,x2]} as Function by GRFUNC_1:8;
A1: dom f = {1,2} by RELAT_1:10;
  then
A2: dom <*x1,x2*> = dom f by Th2,Th88;
  now
    let x be object;
    assume
A3: x in {1,2};
    per cases by A3,TARSKI:def 2;
    suppose
A4:   x = 1;
      then
A5:   <*x1,x2*>.x = x1 by Th44;
      [x,x1] in f by A4,TARSKI:def 2;
      hence f.x = <*x1,x2*>.x by A5,FUNCT_1:1;
    end;
    suppose
A6:   x = 2;
      then
A7:   <*x1,x2*>.x = x2 by Th44;
      [x,x2] in f by A6,TARSKI:def 2;
      hence f.x = <*x1,x2*>.x by A7,FUNCT_1:1;
    end;
  end;
  hence thesis by A1,A2,FUNCT_1:2;
end;

reserve j for Nat;

theorem
  for q being FinSubsequence holds dom Seq q = dom Sgm dom q
proof
  let q be FinSubsequence;
  rng Sgm dom q = dom q by Th50;
  hence thesis by RELAT_1:27;
end;

theorem
 for q being FinSubsequence holds rng q = rng Seq q
proof
  let q be FinSubsequence;
  dom q = rng Sgm dom q by Th50;
  hence thesis by RELAT_1:28;
end;

registration
  cluster one-to-one for FinSequence;
  existence
  proof
    take {};
    thus thesis;
  end;
end;

registration
  let D;
  cluster one-to-one for FinSequence of D;
  existence
  proof
    take <*>D;
    thus thesis;
  end;
end;

registration
  cluster non empty natural-valued for FinSequence;
  existence
  proof
    <*0*> is natural-valued & <*0*> is non empty;
    hence thesis;
  end;
end;