:: Zero Based Finite Sequences
::  by Tetsuya Tsunetou , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received September 28, 2001
:: Copyright (c) 2001 Association of Mizar Users

environ

 vocabularies FUNCT_1, BOOLE, ORDINAL1, FINSEQ_1, FINSET_1, RELAT_1, ORDINAL2,
      CARD_1, TARSKI, PARTFUN1, ALGSEQ_1, ARYTM_1, FUNCT_4, FINSEQ_7, CAT_1,
      AFINSQ_1, FUNCOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
      ORDINAL1, ORDINAL2, ORDINAL4, REAL_1, NAT_1, PARTFUN1, FINSET_1, CARD_1,
      FINSEQ_1, FUNCOP_1, FUNCT_4, CQC_LANG, FUNCT_7, XXREAL_0;
 constructors FUNCT_1, WELLORD2, FUNCT_4, XXREAL_0, XREAL_0, REAL_1, NAT_1,
      ORDINAL4, CQC_LANG, FUNCT_7;
 registrations FUNCT_1, RELAT_1, RELSET_1, CARD_1, SUBSET_1, ORDINAL1, ARYTM_3,
      FUNCT_7, XREAL_0, ORDINAL2, FUNCOP_1, XXREAL_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, FUNCT_1, WELLORD2, ORDINAL1, XBOOLE_0;
 theorems TARSKI, AXIOMS, FUNCT_1, REAL_1, NAT_1, ZFMISC_1, RELAT_1, RELSET_1,
      PARTFUN1, ORDINAL1, CARD_1, FINSEQ_1, EULER_1, CARD_4, CARD_5, FUNCT_7,
      GRFUNC_1, ORDINAL4, CARD_2, FUNCT_4, CQC_LANG, ORDINAL3,
      XBOOLE_0, XBOOLE_1, FINSET_1, FUNCOP_1, XREAL_1;
 schemes FUNCT_1, REAL_1, NAT_1, XBOOLE_0;

begin

 reserve k,m,n for Nat,
         x,y,z,y1,y2,X,Y for set,
         f,g for Function;

:::::::::::::::::::::::::::::::::::::::::::::::
::                                           ::
::   Extended Segments of Natural Numbers    ::
::                                           ::
:::::::::::::::::::::::::::::::::::::::::::::::

theorem
 Th1: n in n+1
  proof
       n < n+1 by NAT_1:38;
    then n in { k : k < n+1 };
   hence n in n+1 by AXIOMS:30;
  end;

theorem Th2:
   k <= n implies k = k /\ n
  proof
   assume k <= n;
      then k c= n by CARD_1:56;
   hence thesis by XBOOLE_1:28;
  end;

theorem
     k = k /\ n implies k <= n by Th2;

theorem Th4:  :: ORDINAL1:def 1, CARD_1:52
  n \/ { n } = n+1
proof
    n+1 = succ n by CARD_1:52;
 hence thesis by ORDINAL1:def 1;
end;

theorem Th5:
 Seg n c= n+1
  proof
   let x;
   assume A1:x in Seg n;
   then reconsider x as Nat;
      1<=x & x<=n by A1,FINSEQ_1:3;
   then x<n+1 by NAT_1:38;
   hence thesis by EULER_1:1;
  end;

theorem
    n+1 = {0} \/ Seg n
  proof
   thus n+1 c= {0} \/ Seg n
    proof
     let x;
     assume x in n+1;
     then x in {j where j is Nat: j<n+1} by AXIOMS:30;
     then consider j being Nat such that
A1: j=x & j<n+1;
        j=0 or 0<j & j<=n by A1,NAT_1:38;
     then j=0 or 1<j+1 & j<=n by XREAL_1:31;
     then j=0 or 1<=j & j<=n by NAT_1:38;
     then x in {0} or x in Seg n by A1,FINSEQ_1:3,TARSKI:def 1;
     hence thesis by XBOOLE_0:def 2;
    end;
          1 <= n+1 by NAT_1:29;
then A2:    {0} c= n+1 by CARD_1:56,CARD_5:1;
          Seg(n) c= n+1 by Th5;
   hence thesis by A2,XBOOLE_1:8;
  end;

::::::::::::::::::::::::::::::::
::                            ::
::  Finite ExFinSequences     ::
::                            ::
::::::::::::::::::::::::::::::::

theorem Th7:
 for r being Function holds
  r is finite T-Sequence-like iff ex n st dom r = n
  proof let r be Function;
   hereby assume r is finite T-Sequence-like;
      then dom r is finite & dom r is Ordinal by FINSET_1:29,ORDINAL1:def 7;
      then dom r in omega by CARD_4:7;
     hence ex n st dom r = n;
    end;
   assume ex n st dom r = n;
   hence thesis by FINSET_1:29,ORDINAL1:def 7;
  end;

 registration
  cluster finite T-Sequence-like Function;
   existence proof
     take f = {};
 A1: for x st x in {} holds f.x = 0;
      dom f = {};
     hence thesis by A1,Th7;
    end;
 end;

definition
  mode XFinSequence is finite T-Sequence;
end;

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

registration
 cluster natural -> finite set;
 coherence
  proof let a be set; assume a in omega;
    then a is Nat;
   hence thesis;
  end;
 let p;
 cluster dom p -> natural;
 coherence
  proof ex n st dom p = n by Th7;
   hence thesis;
  end;
end;

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

definition let p;
 redefine func len p -> Nat means
:Def1:  it = dom p;
 coherence
  proof Card p = card p;
   hence thesis;
  end;
 compatibility
  proof let k;
    consider n such that
A1:   dom p = n by Th7;
       dom p, p are_equipotent
     proof
        deffunc F(set) = [$1,p.$1];
      consider g being Function such that
A2:    dom g = dom p and
A3:    for x 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;
        assume
A4:        x in dom g & 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,A4;
        hence x = y by ZFMISC_1:33;
       end;
      thus dom g = dom p by A2;
      thus rng g c= p
       proof let i be set;
        assume i in rng g;
         then consider x such that
A5:       x in dom g and
A6:       g.x = i by FUNCT_1:def 5;
            g.x = [x,p.x] by A2,A3,A5;
        hence i in p by A2,A5,A6,FUNCT_1:8;
       end;
      let i be set;
      assume
A7:      i in p;
       then consider x,y such that
A8:      i = [x,y] by RELAT_1:def 1;
A9:     x in dom p & y = p.x by A7,A8,FUNCT_1:8;
       then g.x = i by A3,A8;
      hence i in rng g by A2,A9,FUNCT_1:def 5;
     end;
   then A10:  Card p = Card dom p by CARD_1:21;
   hence k = Card p implies k = dom p by A1,CARD_1:66;
   thus thesis by A10,CARD_1:66;
  end;
 end;

 definition let p;
  redefine func dom p -> Subset of NAT;
   coherence
  proof A1:dom p = len p by Def1 .={i where i is Nat:i<len p} by AXIOMS:30;
       {i where i is Nat:i<len p} c= NAT
     proof let x be set;assume x in {i where i is Nat:i<len p};
      then consider i being Nat such that A2:i=x & i<len p;
      thus x in NAT by A2;
     end;
   hence thesis by A1;
  end;
 end;

theorem
     (ex k st dom f c= k) implies ex p st f c= p
proof
  given k such that
A1: dom f c= k;
  deffunc F(set) = f.$1;
  consider g such that
A2: dom g = k & for x st x in k holds g.x = F(x) from FUNCT_1:sch 3;
  reconsider g as XFinSequence by A2,Th7;
  take g;
  let x; assume
A3: x in f;
  then consider y,z such that
A4: [y,z] = x by RELAT_1:def 1;
      y in dom f by A3,A4,RELAT_1:def 4;
   then y in dom g & f.y = z by A1,A2,A3,A4,FUNCT_1:def 4;
   then [y,g.y] in g & g.y = z by A2,FUNCT_1:8;
  hence thesis by A4;
end;

scheme XSeqEx{A()->Nat,P[set,set]}:
 ex p st dom p = A() & for k st k in A() holds P[k,p.k]
 provided
 A1: for k,y1,y2 st k in A() & P[k,y1] & P[k,y2] holds y1=y2
   and
 A2: for k st k in A() ex x st P[k,x]
proof
   A3: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1=y2
    proof let x,y1,y2;assume A4:x in A() & P[x,y1] & P[x,y2];
         A()={i where i is Nat: i<A()} by AXIOMS:30;
      then consider i being Nat such that A5:i=x & i<A() by A4;
     thus y1=y2 by A1,A4,A5;
    end;
   A6: for x st x in A() ex y st P[x,y]
    proof let x;assume A7:x in A();
         A()={i where i is Nat: i<A()} by AXIOMS:30;
      then consider i being Nat such that A8:i=x & i<A() by A7;
     thus thesis by A2,A7,A8;
    end;
    consider f being Function such that A9: dom f = A() &
        (for x st x in A() holds P[x,f.x]) from FUNCT_1:sch 2(A3,A6);
    reconsider p=f as XFinSequence by A9,Th7;
    take p;
    thus thesis by A9;
 end;

scheme XSeqLambda{A()->Nat,F(set) -> set}:
 ex p being XFinSequence st len p = A() & for k st k in A() holds p.k=F(k)
proof
   consider f being Function such that
    A1: dom f = A() & for x st x in A() holds f.x=F(x) from FUNCT_1:sch 3;
   reconsider p=f as XFinSequence by A1,Th7;
   take p;
  thus thesis by A1,Def1;
 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 such that A2: z=[x,y] by RELAT_1:def 1;
      x in dom p by A1,A2,FUNCT_1:8;
   then reconsider k = x as Nat;
   take k;
   thus thesis by A1,A2,FUNCT_1:8;
 end;

theorem Th10:
  dom p = dom q & (for k st k in dom p holds p.k = q.k) implies p=q
proof
  assume A1: dom p = dom q & (for k st k in dom p holds p.k = q.k);
  then for x st x in dom p holds p.x=q.x;
  hence thesis by A1,FUNCT_1:9;
end;

theorem
    ( len p = len q & for k st k < len p holds p.k=q.k ) implies p=q
proof
   assume
A1: len p = len q & for k st k<len p holds p.k = q.k;
A2:   dom p = len p & dom q = len q by Def1;
      now let x;
     assume
A3:    x in dom p;
     then reconsider k=x as Nat;
          k < len p by A2,A3,EULER_1:1;
     hence p.x = q.x by A1;
   end;
   hence thesis by A1,A2,FUNCT_1:9;
end;

theorem Th12:
   p|n is XFinSequence
proof
 A1: dom(p| n) = dom p /\ n by RELAT_1:90
                .= len p /\ n by Def1;
      len p <= n or n <= len p;
   then dom(p| n) = len p or dom(p| n) = n by A1,Th2;
  hence thesis by Th7;
end;

theorem
    rng p c= dom f implies f*p is XFinSequence
proof
  assume rng p c= dom f;
  then dom(f*p) = dom p by RELAT_1:46 .= len p by Def1;
  hence thesis by Th7;
end;

theorem
     k < len p & q = p|k implies len q = k & dom q = k
proof
   assume A1: k < len p & q = p|k;
    then k c= len p by CARD_1:56;
    then k c= dom p by Def1;
   then dom q = k by A1,RELAT_1:91;
  hence thesis by Def1;
end;

:::::::::::::::::::::::::::::::::
::                             ::
::    XFinSequences of D       ::
::                             ::
:::::::::::::::::::::::::::::::::

registration let D be set;
 cluster finite T-Sequence of D;
 existence
  proof
      {} is T-Sequence of D by ORDINAL1:45;
   hence thesis;
  end;
end;

definition let D be set;
 mode XFinSequence of D is finite T-Sequence of D;
end;

theorem Th15:
 for D being set, f being XFinSequence of D holds f is PartFunc of NAT,D
  proof let D be set, f be XFinSequence of D;
A1: dom f c= NAT;
       rng f c= D by ORDINAL1:def 8;
   hence thesis by A1,RELSET_1:11;
  end;

registration
 cluster {} -> T-Sequence-like;
 coherence by ORDINAL1:45;
end;

registration let D be set;
 cluster finite T-Sequence-like PartFunc of NAT,D;
  existence proof {} is PartFunc of NAT,D by PARTFUN1:56; hence thesis;end;
end;

reserve D for set;

theorem
    for p being XFinSequence of D holds p|k is XFinSequence of D
  proof let p be XFinSequence of D;
       rng(p|k) c= rng p & rng p c= D by ORDINAL1:def 8;
    then rng(p|k) c= D by XBOOLE_1:1;
   hence thesis by Th12,ORDINAL1:def 8;
  end;

theorem
    for D being non empty set
  ex p being XFinSequence of D st len p = k
proof let D be non empty set;
    consider y being Element of D;
    set p = k --> y;
A1: dom p = k & for n st n in k holds p.n= y by FUNCOP_1:13,19;
    then reconsider p = k --> y as XFinSequence by Th7;
A2:  rng p c= {y} by FUNCOP_1:19;
   {y} c= D by ZFMISC_1:37;
   then rng p c= D by A2,XBOOLE_1:1;
   then reconsider p as XFinSequence of D by ORDINAL1:def 8;
  take p;
  thus thesis by A1, Def1;
end;

::::::::::::::::::::::::::::::::::::
::                                ::
::    The Empty XFinSequence      ::
::                                ::
::::::::::::::::::::::::::::::::::::

registration
  cluster empty XFinSequence;
  existence by ORDINAL1:45;
end;

theorem Th18:
 len p = 0 iff p = {}
  proof
      len p = 0 iff p, {} are_equipotent by CARD_1:def 5;
   hence thesis by CARD_1:46;
  end;

theorem Th19:
  for D be set holds {} is XFinSequence of D
proof let D be set;
     rng {} c= D by XBOOLE_1:2;
 hence thesis by ORDINAL1:def 8;
end;

registration
  let D be set;
  cluster empty XFinSequence of D;
existence
 proof
      {} is XFinSequence of D by Th19;
   hence thesis;
 end;
end;

definition let x;
  func <%x%> -> set equals
    { [0,x] };
  coherence;
end;

definition let D be set;
  func <%>D -> XFinSequence of D equals
      {};
  coherence by Th19;
end;

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

 definition let p,q;
  redefine func p^q means
:Def4: dom it = 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);
  compatibility
   proof let pq be T-Sequence;
A1:  len p = dom p & len q = dom q by Def1;
A2:  len p +^ len q = len p + len q by CARD_2:49;
    hereby assume
A3:    pq = p^q;
      hence dom pq = len p + len q by A1,A2,ORDINAL4:def 1;
      thus for k st k in dom p holds pq.k=p.k by A3,ORDINAL4:def 1;
      let k; assume k in dom q;
       then pq.(len p +^ k) = q.k by A1,A3,ORDINAL4:def 1;
      hence pq.(len p + k) = q.k by CARD_2:49;
     end;
    assume that
A4:  dom pq = len p + len q and
A5:  (for k st k in dom p holds pq.k=p.k) and
A6:  (for k st k in dom q holds pq.(len p + k) = q.k);
A7:  for a be Ordinal st a in dom p holds pq.a = p.a by A5;
        now let a be Ordinal; assume
A8:    a in dom q;
      then reconsider k = a as Nat;
      thus pq.(dom p +^ a) = pq.(len p + k) by A1,CARD_2:49 .= q.a by A6,A8;
     end;
    hence thesis by A1,A2,A4,A7,ORDINAL4:def 1;
   end;
 end;
registration let p,q;
  cluster p^q -> finite;
  coherence
   proof
        dom (p^q) = (dom p)+^dom q by ORDINAL4:def 1;
     then dom (p^q) is Nat by ORDINAL1:def 13;
    hence thesis by Th7;
   end;
  end;

theorem
 Th20: len(p^q) = len p + len q
  proof
       dom(p^q) = len p + len q by Def4;
   hence thesis by Def1;
  end;

theorem Th21:
  (len p <= k & k < len p + len q) implies (p^q).k=q.(k-len p)
proof
    assume A1:len p <= k & k < len p + len q;
    then consider m such that A2: len p + m = k by NAT_1:28;
       k - len p < len p + len q - len p by A1,REAL_1:92;
    then m in len q by A2,EULER_1:1;
    then m in dom q by Def1;
   hence thesis by A2,Def4;
end;

theorem
     len p <= k & k < len(p^q) implies (p^q).k = q.(k - len p)
proof
  assume A1: len p <= k & k < len(p^q);
   then k < len p + len q by Th20;
  hence thesis by A1,Th21;
end;

theorem Th23:
  k in dom (p^q) implies
    (k in dom p or (ex n st n in dom q & k=len p + n))
proof assume k in dom(p^q);
    then k in len (p^q) by Def1;
    then k in (len p + len q) by Th20;
then A1:   k < len p + len q by EULER_1:1;
A2:  now assume not len p <= k;
            then k in len p by EULER_1:1;
        hence thesis by Def1;
    end;
       now assume len p <= k;
        then consider n such that A3: k=len p + n by NAT_1:28;
           n + len p - len p < len q + len p - len p by A1,A3,REAL_1:92;
        then n in len q by EULER_1:1;
      then n in dom q by Def1;
      hence thesis by A3;
    end;
  hence thesis by A2;
end;

theorem Th24:
 for p,q being T-Sequence holds dom p c= dom(p^q)
proof let p,q be T-Sequence;
     dom(p^q) = (dom p)+^(dom q) by ORDINAL4:def 1;
  hence thesis by ORDINAL3:27;
end;

theorem Th25:
  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 len q by Def1;
    reconsider k=x as Nat by A1;
    take k;
     k < len q by A2,EULER_1:1;
    then len p + k < len p + len q by XREAL_1:10;
    then len p + k in (len p + len q) by EULER_1:1;
  hence thesis by Def4;
end;

theorem Th26:
  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 Th25;
 hence thesis;
end;

theorem Th27:
   rng p c= rng(p^q)
proof
     now let x; assume x in rng p;
       then consider y such that A1: y in dom p & x=p.y by FUNCT_1:def 5;
       reconsider k=y as Nat by A1;
A2:    k in dom p & dom p c= dom(p^q) by A1,Th24;
          (p^q).k=p.k by A1,Def4;
     hence x in rng(p^q) by A1,A2,FUNCT_1:12;
  end;
 hence thesis by TARSKI:def 3;
end;

theorem Th28:
  rng q c= rng(p^q)
proof
       now let x; assume x in rng q;
         then consider y such that A1: y in dom q & x=q.y by FUNCT_1:def 5;
         reconsider k=y as Nat by A1;
   A2:    len p + k in dom(p^q) by A1,Th26;
            (p^q).(len p + k) = q.k by A1,Def4;
       hence x in rng(p^q) by A1,A2,FUNCT_1:12;
    end;
  hence thesis by TARSKI:def 3;
end;

theorem
 Th29: rng(p^q) = rng p \/ rng q
 proof
          now let x; assume x in rng(p^q);
         then consider y such that A1: y in dom(p^q) & x=(p^q).y by
FUNCT_1:def 5;
        A2:  y in (len p + len q) by A1,Def4;
             reconsider k=y as Nat by A1;
        A3:   k < len p + len q by A2,EULER_1:1;
     A4:    now assume A5: len p <= k;
               then A6: q.(k-len p) = x by A1,A3,Th21;
                  consider m such that A7: len p + m = k by A5,NAT_1:28;
                      m + len p - len p < len p + len q - len p
                   by A3,A7,REAL_1:92;
                   then m in len q by EULER_1:1;
                   then k-len p in dom q by A7,Def1;
               hence x in rng q by A6,FUNCT_1:12;
             end;

                now assume not len p <= k;
                    then k in len p by EULER_1:1;
                 then A8: k in dom p by Def1;
                    then p.k = x by A1,Def4;
                hence x in rng p by A8,FUNCT_1:12;
             end;
          hence x in rng p \/ rng q by A4,XBOOLE_0:def 2;
       end;
     then A9: rng(p^q) c= rng p \/ rng q by TARSKI:def 3;
        rng p c= rng(p^q) & rng q c= rng(p^q) by Th27,Th28;
        then (rng p \/ rng q) c= rng(p^q) by XBOOLE_1:8;
   hence thesis by A9,XBOOLE_0:def 10;
 end;

theorem
 Th30: p^q^r = p^(q^r)
  proof
 A1:     dom ((p^q)^r) = (len (p^q) + len r) by Def4
       .= (len p + len q + len r) by Th20
       .= (len p + (len q + len r))
       .= (len p + len(q^r)) by Th20;
 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 Th24;
           hence (p^q^r).k=(p^q).k by A3,Def4
              .=p.k by A3,Def4;
        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 Th26;
                  hence (p^q^r).(len p + k) = (p^q).(len p + k) by Def4
                        .=q.k by A6,Def4
                        .=(q^r).k by A6,Def4;
                end;
                   now assume not k in dom q;
                   then consider n such that
                      A7: n in dom r & k=len q + n by A4,Th23;
                    thus (p^q^r).(len p + k) =(p^q^r).(len p + len q + n)
                     by A7
                      .=(p^q^r).(len(p^q) + n) by Th20
                      .=r.n by A7,Def4
                      .=(q^r).k by A7,Def4;
                end;
            hence (p^q^r).(len p + k)=(q^r).k by A5;
        end;
     hence (p^q)^r=p^(q^r) by A1,A2,Def4;
  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 Th20;
       then len p + len r = len q + len r by Th20;
        then len p = len q;
then A4:    dom p = len q by Def1
         .= dom q by Def1;

          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,Def4
                 .=q.k by A4,A5,Def4;
          end;
       hence thesis by A4,Th10;
    end;
        now assume A6: r^p=r^q;
       then len r + len p = len(r^q) by Th20
       .=len r + len q by Th20;
        then len p = len q;
    then A7: dom p = len q by Def1
        .= dom q by Def1;
          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,Def4
                 .= q.k by A7,A8,Def4;
         end;
      hence thesis by A7,Th10;
    end;
   hence thesis by A1,A2;
  end;

theorem
 Th32: p^{} = p & {}^p = p
 proof
    A1: dom(p^{}) = len (p^{}) by Def1
       .= len p + len {} by Th20
       .= len p + 0 by Th18
       .= dom p by Def1;
     thus p^{} = p
       proof
             for k st k in dom p holds p.k=(p^{}).k by Def4;
         hence p^{}=p by A1,Th10;
       end;

   A2: dom({}^p) = len ({}^p) by Def1
      .= (len {} + len p) by Th20
      .= (0 + len p) by Th18
      .= dom p by Def1;
   thus
        {}^p=p
      proof
            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).(0 + k)
               .=({}^p).(len {} + k) by Th18
               .=p.k by A3,Def4;
           end;
         hence {}^p=p by A2,Th10;
      end;

 end;

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

 definition let D be set;let p,q be XFinSequence of D;
 redefine func p^q -> T-Sequence of D;
   coherence
    proof
A1:   rng(p^q) = rng p \/ rng q by Th29;
         rng p c= D & rng q c= D by ORDINAL1:def 8;
      then rng(p^q) c= D by A1,XBOOLE_1:8;
     hence thesis by ORDINAL1:def 8;
    end;
 end;

Lm1:
 for x1, y1 being set holds
 [x,y] in {[x1,y1]} implies x = x1 & y = y1
  proof
  let x1, y1 be set;
  assume [x,y] in {[x1,y1]};
   then [x,y] = [x1,y1] by TARSKI:def 1;
   hence x = x1 & y = y1 by ZFMISC_1:33;
  end;

 definition let x;
  redefine func <%x%> -> Function means
:Def5:  dom it = 1 & it.0 = x;
   coherence by GRFUNC_1:15;
   compatibility
   proof
     let f be Function;
     hereby assume f = <%x%>;
then A1:    f = { [0,x] };
       hence dom f = 1 by CARD_5:1,RELAT_1:23;
          [0,x] in f by A1,TARSKI:def 1;
       hence f.0 = x by FUNCT_1:8;
     end;
     assume A2: dom f = 1 & f.0 = x;
     reconsider g = { [0,f.0] } as Function by GRFUNC_1:15;
        f = { [0,f.0] }
     proof
         [y,z] in f iff [y,z] in g
      proof
        hereby assume [y,z] in f;
         then y in {0} & z in rng f & rng f = {f.0}
            by A2,CARD_5:1,FUNCT_1:14,RELAT_1:def 4,def 5;
         then y = 0 & z = f.0 by TARSKI:def 1;
         hence [y,z] in g by TARSKI:def 1;
        end;
        assume [y,z] in g;
        then y = 0 & z = f.0 & 0 in dom f by A2,Lm1,CARD_5:1,TARSKI:def 1;
        hence [y,z] in f by FUNCT_1:def 4;
      end;
      hence thesis by RELAT_1:def 2;
     end;
    hence thesis by A2;
  end;
 end;

 registration let x;
  cluster <%x%> -> Function-like Relation-like;
  coherence;
 end;

 registration let x;
  cluster <%x%> -> finite T-Sequence-like;
 coherence
    proof
         dom <%x%> = 1 by Def5;
     hence thesis by FINSET_1:29,ORDINAL1:def 7;
    end;
 end;

theorem
     p^q is XFinSequence of D implies
     p is XFinSequence of D & q is XFinSequence of D
proof
  assume p^q is XFinSequence of D;
  then rng(p^q) c= D by ORDINAL1:def 8;
 then A1: rng p \/ rng q c= D by Th29;
      rng p c= rng p \/ rng q by XBOOLE_1:7;
   then rng p c= D by A1,XBOOLE_1:1;
  hence p is XFinSequence of D by ORDINAL1:def 8;
      rng q c= rng p \/ rng q by XBOOLE_1:7;
   then rng q c= D by A1,XBOOLE_1:1;
  hence q is XFinSequence of D by ORDINAL1:def 8;
end;

definition let x,y;
  func <%x,y%> -> set equals
    <%x%>^<%y%>;
  correctness;

  let z;
  func <%x,y,z%> -> set equals
    <%x%>^<%y%>^<%z%>;
  correctness;
end;

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

registration let x,y;
  cluster <%x,y%> -> finite T-Sequence-like;
  coherence;
  let z;
  cluster <%x,y,z%> -> finite T-Sequence-like;
  coherence;
end;

theorem
     <%x%> = { [0,x] };

theorem Th36:
   p=<%x%> iff dom p = 1 & rng p = {x}
proof
      thus p = <%x%> implies dom p = 1 & rng p = {x}
            proof
               assume A1: p = <%x%>;
              hence dom p = 1 by Def5;
                   dom p = {0} by A1,Def5,CARD_5:1;
             then rng p = {p.0} by FUNCT_1:14;
              hence thesis by A1,Def5;
            end;
        assume A2: dom p = 1 & rng p = {x};
           1=0+1;
           then 0 in dom p by A2,Th1;
           then p.0 in {x} by A2,FUNCT_1:12;
           then p.0 = x by TARSKI:def 1;
       hence p=<%x%> by A2,Def5;
end;

theorem Th37:
  p=<%x%> iff len p = 1 & rng p = {x}
proof
     len p = 1 iff dom p = 1 by Def1;
 hence thesis by Th36;
end;

theorem
     p = <%x%> iff len p = 1 & p.0 = x
proof
     len p = 1 iff dom p = 1 by Def1;
 hence thesis by Def5;
end;

theorem
     (<%x%>^p).0 = x
  proof
      0 in 1 by CARD_5:1,TARSKI:def 1;
   then 0 in dom <%x%> by Def5;
   then (<%x%>^p).0 = <%x%>.0 by Def4;
   hence thesis by Def5;
  end;

theorem
     (p^<%x%>).(len p)=x
proof
       dom <%x%> = 1 & 1<>0 & 1 = (0+1) by Def5;
    then 0 in dom <%x%> & len p + 0 = len p by Th1;
  hence
      (p^<%x%>).(len p) = <%x%>.0 by Def4
   .=x by Def5;
end;

theorem Th41:
  <%x,y,z%>=<%x%>^<%y,z%> &
  <%x,y,z%>=<%x,y%>^<%z%> by Th30;

theorem Th42:
  p = <%x,y%> iff len p = 2 & p.0=x & p.1=y
proof
  thus
        p = <%x,y%> implies len p = 2 & p.0=x & p.1=y
      proof
         assume A1: p=<%x,y%>;
          hence
              len p = len(<%x%>^<%y%>)
           .= len <%x%> + len <%y%> by Th20
           .= 1 + len <%y%> by Th37
           .= 1 + 1 by Th37
           .=2;
A2:          0 in {0} by TARSKI:def 1;
          then A3: 0 in dom <%x%> by Def5,CARD_5:1;
         thus
                p.0 = (<%x%>^<%y%>).0 by A1
              .= <%x%>.0 by A3,Def4
              .= x by Def5;
         A4: 0 in dom <%y%> by A2,Def5,CARD_5:1;
         thus
              p.1 = (<%x%>^<%y%>).(1+0) by A1
           .= (<%x%>^<%y%>).(len <%x%> + 0) by Th37
           .= <%y%>.0 by A4,Def4
           .= y by Def5;
       end;
    assume A5: len p = 2 & p.0=x & p.1=y;
      then A6: dom p = (1+1) by Def1
          .= (len <%x%> + 1) by Th37
          .= (len <%x%> + len <%y%>) by Th37;

      A7: for k st k in dom <%x%> holds p.k=<%x%>.k
         proof let k; assume k in dom <%x%>;
            then k in {0} by Def5,CARD_5:1;
           then k=0 by TARSKI:def 1;
          hence p.k = <%x%>.k by A5,Def5;
         end;

          for k st k in dom <%y%> holds p.((len <%x%>)+k)=<%y%>.k
         proof let k; assume k in dom <%y%>;
then A8:              k in {0} by Def5,CARD_5:1;
            thus p.((len <%x%>) + k) = p.(1+k) by Th37
              .=p.(1+0) by A8,TARSKI:def 1
              .=<%y%>.0 by A5,Def5
              .= <%y%>.k by A8,TARSKI:def 1;
         end;
    hence p=<%x%>^<%y%> by A6,A7,Def4
          .= <%x,y%>;
end;

theorem
     p = <%x,y,z%> iff len p = 3 & p.0 = x & p.1 = y & p.2 = z
proof
   thus
        p = <%x,y,z%> implies len p = 3 & p.0 = x & p.1 = y & p.2 = z
      proof
         assume A1: p =<%x,y,z%>;
           hence
               len p = len (<%x,y%>^<%z%>)
            .=len <%x,y%> + len <%z%> by Th20
            .=2 + len <%z%> by Th42
            .=2+1 by Th37
            .=3;
A2:              0 in {0} by TARSKI:def 1;
              then A3:   0 in dom <%x%> by Def5,CARD_5:1;

         thus p.0 = (<%x%>^<%y,z%>).0 by A1,Th41
            .=<%x%>.0 by A3,Def4
            .=x by Def5;
          A4: 1 in (1+1) by Th1;
                len <%x,y%> = 2 by Th42;
          then A5: 1 in dom <%x,y%> by A4,Def1;
        thus p.1 = (<%x,y%>^<%z%>).1 by A1
           .=<%x,y%>.1 by A5,Def4
           .=y by Th42;

         A6: 0 in dom <%z%> by A2,Def5,CARD_5:1;
        thus p.2 = (<%x,y%>^<%z%>).(2+0) by A1
          .=(<%x,y%>^<%z%>).(len (<%x,y%>) + 0) by Th42
          .= <%z%>.0 by A6,Def4
          .= z by Def5;

      end;

    assume A7: len p = 3 & p.0 = x & p.1 = y & p.2 = z;
      then A8: dom p = (2+1) by Def1
          .= ((len <%x,y%>) + 1) by Th42
          .= ((len <%x,y%>) + len <%z%>) by Th37;
     A9: for k st k in dom <%x,y%> holds p.k=<%x,y%>.k
           proof let k such that A10: k in dom <%x,y%>;
                   len <%x,y%> = 2 by Th42;
then A11:             k in 2 by A10,Def1;
           A12:    k=0 implies p.k=<%x,y%>.k by A7,Th42;
                     k=1 implies p.k=<%x,y%>.k by A7,Th42;
              hence thesis by A11,A12,CARD_5:1,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 {0} by Def5,CARD_5:1;
       then A13:  k = 0 by TARSKI:def 1;
          hence
               p.( (len <%x,y%>) + k) = p.(2+0) by Th42
            .=<%z%>.k by A7,A13,Def5;
         end;
     hence p=<%x,y%>^<%z%> by A8,A9,Def4
           .=<%x,y,z%>;
end;

theorem Th44:
   p <> {} implies ex q,x st p=q^<%x%>
proof
 assume p <> {};
 then len p <> 0 by Th18;
 then consider n such that A1: len p = n+1 by NAT_1:22;
 reconsider q=p| n as XFinSequence by Th12;
 take q;
 take p.(len p - 1);
A2: dom q = n
      proof
       A3: dom q = dom p /\ n by RELAT_1:90
            .= len p /\ n by Def1;
            n <= len p by A1,NAT_1:29;
          then n c= len p by CARD_1:56;
        hence
            dom q = n by A3,XBOOLE_1:28;
      end;

thus q^<%p.(len p - 1)%>=p
   proof
     A4: dom(q^<%p.(len p - 1)%>) = len (q^<%p.(len p - 1)%>) by Def1
         .= (len q + len <%p.(len p - 1)%>) by Th20
         .= (len q + 1) by Th37
         .= len p by A1,A2,Def1
         .= dom p by Def1;

         for x st x in dom p holds p.x = (q^<%p.(len p - 1)%>).x
         proof let x; assume A5:  x in dom p;
            then reconsider k = x as Nat;
               k in (n+1) by A1,A5,Def1;
then A6:            k in n \/ {n} by Th4;
       A7:  now assume A8: k in n;
              hence
                    p.k=q.k by A2,FUNCT_1:70
                  .=(q^<%p.(len p - 1)%>).k by A2,A8,Def4;
            end;
               now assume A9: k in {n};
                     0 in (0+1) by Th1;
              then A10: 0 in dom <%p.(len p - 1)%> by Def5;
               thus
                   (q^<%p.(len p - 1)%>).k =(q^<%p.(len p - 1)%>).n
                by A9,TARSKI:def 1
                .=(q^<%p.(len p - 1)%>).(len q + 0) by A2,Def1
                .=<%p.(len p - 1)%>.0 by A10,Def4
                .=p.n by A1,Def5
                .=p.k by A9,TARSKI:def 1;
            end;
         hence thesis by A6,A7,XBOOLE_0:def 2;
       end;
     hence q^<%p.(len p - 1 )%>=p by A4,FUNCT_1:9;
   end;
end;

definition let D be non empty set; let x be Element of D;
 redefine func <%x%> -> XFinSequence of D;
   coherence
    proof
        rng <%x%> c= D
      proof let y; assume y in rng <%x%>;
        then y in {x} by Th37;
        then y = x by TARSKI:def 1;
       hence y in D;
      end;
     hence thesis by ORDINAL1:def 8;
    end;
 end;

:: scheme of induction for extended finite sequences ::

scheme IndXSeq{P[XFinSequence]}:
 for p holds P[p]
  provided
 A1: P[{}] and
 A2: for p,x st P[p] holds P[p^<%x%>]
proof let p;
  defpred P1[Real] means for p st len p = $1 holds P[p];
    consider X being Subset of REAL such that
      A3:  for x being Real holds x in X iff P1[x] from REAL_1:sch 1;
      for k holds k in X proof
         defpred R[Nat] means $1 in X;
      A4: R[0]
          proof
               for q st len q = 0 holds P[q] by A1,Th18;
           hence 0 in X by A3;
          end;

           now let n such that A5:n in X;
               now let q;
              assume A6: len q = n+1;
              then q <> {} by Th18;
              then consider r,x such that A7: q=r^<%x%> by Th44;
                 len q = len r + len <%x%> by A7,Th20
              .= len r + 1 by Th37;
              then len r = n + 1 - 1 by A6;
              then P[r] by A3,A5;
             hence P[q] by A2,A7;
            end;
           hence n+1 in X by A3;
          end;
    then A8:   for n st R[n] holds R[n+1];
         thus for k holds R[k] from NAT_1:sch 1(A4,A8);
       end;

      then len p in X;
      hence P[p] by A3;
 end;

theorem
     for p,q,r,s being XFinSequence st p^q = r^s & len p <= len r
  ex t being XFinSequence st p^t = r
 proof
    defpred P[XFinSequence] means
    for p,q,s st p^q=$1^s & len p <= len $1 holds
             ex t being XFinSequence st p^t=$1;
    A1: P[{}]
         proof
            let p,q,s; assume p^q={}^s & len p <= len {};
       then len p <= 0 by Th18;
then A2:            len p = 0;
            take {};
            thus
                 p^{} = p by Th32
              .= {} by A2,Th18;
         end;

     A3:  for r,x st P[r] holds P[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 A5: p^q=(r^<%x%>)^s & len p <= len (r^<%x%>);
             A6: now assume len p = len(r^<%x%>);
                    then A7: dom p = len(r^<%x%>) by Def1
                        .= dom(r^<%x%>) by Def1;
A8:                     for k st k in dom p holds p.k=(r^<%x%>).k
                        proof let k; assume A9: k in dom p;
                          hence
                               p.k = (r^<%x%>^s).k by A5,Def4
                            .=(r^<%x%>).k by A7,A9,Def4;
                        end;
                         p^{} = p by Th32
                         .=r^<%x%> by A7,A8,Th10;
                      hence thesis;
                end;

                   now assume len p <> len(r^<%x%>);
                        then len p <> len r + len <%x%> by Th20;
                    then A10: len p <> len r + 1 by Th37;
                           len p <= len r + len <%x%> by A5,Th20;
                        then len p <= len r + 1 by Th37;
                    then A11: len p <= len r by A10,NAT_1:26;
                           p^q=r^(<%x%>^s) by A5,Th30;
                        then consider t being XFinSequence such that
                           A12: p^t = r by A4,A11;
                           p^(t^<%x%>) = r^<%x%> by A12,Th30;
                   hence thesis;
                end;
              hence thesis by A6;
        end;
      for r holds P[r] from IndXSeq(A1,A3);
   hence thesis;
 end;

 definition let D be set;
  func D^omega -> set means
:Def8: x in it iff x is XFinSequence of D;
   existence
    proof
     defpred P[set] means  $1 is XFinSequence of D;
     consider X such that
A1:    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 XFinSequence of D by A1;
     assume x is XFinSequence of D;
     then reconsider p = x as XFinSequence of D;
     reconsider p as PartFunc of NAT,D by Th15;
         p c= [:NAT,D:];
     hence x in X by A1;
    end;
   uniqueness proof defpred P[set] means $1 is XFinSequence of D;
   thus for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
   end;
 end;

 registration let D be set;
  cluster D^omega -> non empty;
  coherence
  proof
    consider f being XFinSequence of D;
       f in D^omega by Def8;
    hence thesis;
   end;
  end;

theorem
     x in D^omega iff x is XFinSequence of D by Def8;

theorem
     {} in D^omega
proof
     {} = <%>D;
 hence {} in D^omega by Def8;
end;

scheme SepXSeq{D()->non empty set, P[XFinSequence]}:
 ex X st (for x holds x in X iff ex p st p in D()^omega & P[p] & x=p)
proof
  defpred P1[set] means ex p st P[p] & $1=p;
  consider Y such that A1: x in Y iff x in D()^omega & P1[x]
         from XBOOLE_0:sch 1;
  take Y;
  x in Y implies ex p st p in D()^omega & P[p] & x=p
  proof
   assume x in Y;
   then x in D()^omega & ex p st P[p] & x=p by A1;
   hence thesis;
  end;
hence thesis by A1;
end;

notation
 let p be XFinSequence;
 let i,x be set;
 synonym Replace(p,i,x) for p+*(i,x);
end;
registration
 let p be XFinSequence;
 let i,x be set;
 cluster p+*(i,x) -> finite T-Sequence-like;
 coherence
  proof dom (p+*(i,x)) = dom p by FUNCT_7:32;
   hence thesis by FINSET_1:29,ORDINAL1:def 7;
  end;
 end;

theorem
    for p being XFinSequence, i being Nat, x being set holds
   len Replace(p,i,x) = len p &
   (i < len p implies Replace(p,i,x).i = x) &
   for j being Nat st j <> i holds Replace(p,i,x).j = p.j
  proof let p be XFinSequence;
   let i be Nat, x be set;
A1: len p = dom p & len (p+*(i,x)) = dom (p+*(i,x)) by Def1;
   set f = Replace(p,i,x);
   thus len f = len p by A1,FUNCT_7:32;
       i < len p implies not dom p c= i by A1,CARD_1:56;
    then i < len p implies i in dom p by ORDINAL1:26;
   hence i < len p implies f.i = x by FUNCT_7:33;
   thus thesis by FUNCT_7:34;
  end;

definition
 let D be non empty set;
 let p be XFinSequence of D;
 let i be Nat, a be Element of D;
 redefine func Replace(p,i,a) -> XFinSequence of D;
 coherence
  proof
       now per cases;
      suppose i in dom p;
        then Replace(p,i,a) = p+*(i.-->a) by FUNCT_7:def 3;
then A1:     rng Replace(p,i,a) c= rng p \/ rng (i.-->a) by FUNCT_4:18;
           rng (i.-->a) = {a} by CQC_LANG:5;
        then rng (i.-->a) c= D & rng p c= D by ORDINAL1:def 8,ZFMISC_1:37;
        then rng p \/ rng (i.-->a) c= D by XBOOLE_1:8;
       hence rng Replace(p,i,a) c= D by A1,XBOOLE_1:1;
      end;
      suppose not i in dom p;
        then Replace(p,i,a) = p by FUNCT_7:def 3;
       hence rng Replace(p,i,a) c= D by ORDINAL1:def 8;
     end;
     end;
   hence thesis by ORDINAL1:def 8;
  end;
end;