:: Basic Properties and Concept of Selected Subsequence of Zero Based Finite
:: Sequences
::  by Yatsuka Nakamura and Hisashi Ito
::
:: Received June 27, 2008
:: Copyright (c) 2008-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, MEMBERED, ORDINAL1,
      FINSET_1, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0,
      CARD_1, XBOOLE_0, ORDINAL4, FINSEQ_5, RFINSEQ, JORDAN3, CARD_3, XCMPLX_0,
      AFINSQ_2, BINOP_1, SETWISEO, FINSOP_1, FUNCOP_1, BINOP_2, VALUED_0,
      FUNCT_2, INT_1, PRGCOR_2, XREAL_0, SEQ_1, SERIES_1, VALUED_1, RAT_1,
      SQUARE_1, COMPLEX1, PARTFUN3, PRE_POLY, AMISTD_1, AMISTD_2, REAL_1,
      ORDINAL2;
 notations TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, CARD_1, NUMBERS,
      RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, FINSET_1, XXREAL_0, NAT_D, AFINSQ_1,
      SEQ_1, MEMBERED, VALUED_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, INT_1,
      BINOP_1, BINOP_2, SETWISEO, FINSOP_1, FINSEQ_1, RECDEF_1, VALUED_0,
      SERIES_1, RAT_1, PARTFUN3, RFINSEQ, ORDINAL2;
 constructors SERIES_1, PARTFUN3, WELLORD2, SETWISEO, FINSOP_1, NAT_D,
      RECDEF_1, BINOP_2, RELSET_1, AFINSQ_1, FUNCOP_1, SQUARE_1, BINOP_1,
      XTUPLE_0, RFINSEQ, ORDINAL2;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1,
      NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, FINSEQ_1, AFINSQ_1,
      ORDINAL2, RELSET_1, ORDINAL3, VALUED_1, VALUED_0, MEMBERED, FINSEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1;
 equalities VALUED_1, BINOP_1, ORDINAL1, CARD_1, AFINSQ_1;
 expansions TARSKI, XBOOLE_0, FUNCT_1, BINOP_1, ORDINAL1, FINSEQ_1;
 theorems TARSKI, FUNCT_1, NAT_1, ZFMISC_1, RELAT_1, CARD_2, XBOOLE_0,
      XBOOLE_1, FINSET_1, ORDINAL1, CARD_1, XREAL_1, AFINSQ_1, XXREAL_0, NAT_2,
      FINSEQ_2, WELLORD2, MEMBERED, VALUED_0, VALUED_1, XREAL_0, NAT_D,
      SERIES_1, PARTFUN3, BINOP_1, BINOP_2, SETWISEO, FUNCOP_1, FINSOP_1,
      FINSEQ_1, FUNCT_2, XCMPLX_0, GRFUNC_1, RAT_1, INT_1, FINSEQ_3,
      RFINSEQ, ORDINAL2, FINSEQ_5;
 schemes NAT_1, AFINSQ_1, FUNCT_2, BINOP_1;

begin :: Preparation

reserve i,j,k,n,m for Nat,
  x,y,z,y1,y2 for object, X,Y,D for set,
  p,q for XFinSequence;

Lm1:
  for X,Y be finite set,F be Function of X,Y st card X=card Y
  holds F is onto iff F is one-to-one
proof
  let X,Y be finite set,F be Function of X,Y such that
A1: card X=card Y;
  thus F is onto implies F is one-to-one
  proof
    assume
A2: F is onto;
    assume F is not one-to-one;
    then consider x1,x2 be object such that
A3: x1 in dom F and
A4: x2 in dom F and
A5: F.x1=F.x2 and
A6: x1<>x2;
    reconsider Xx=X\{x1} as finite set;
    Y c= F.:Xx
    proof
      let Fy be object;
      assume Fy in Y;
      then Fy in rng F by A2,FUNCT_2:def 3;
      then consider y being object such that
A7:   y in dom F and
A8:   F.y=Fy by FUNCT_1:def 3;
      now
        per cases;
        suppose
A9:       y=x1;
          x2 in Xx by A4,A6,ZFMISC_1:56;
          hence thesis by A4,A5,A8,A9,FUNCT_1:def 6;
        end;
        suppose
          y<>x1;
          then y in Xx by A7,ZFMISC_1:56;
          hence thesis by A7,A8,FUNCT_1:def 6;
        end;
      end;
      hence thesis;
    end;
    then
A10: Segm card Y c= Segm card Xx by CARD_1:66;
{x1} meets X by A3,ZFMISC_1:48;
then A11:Xx <>X by XBOOLE_1:83;
    Xx c< X by A11;
    hence thesis by A1,A10,NAT_1:39,CARD_2:48;
  end;
  thus F is one-to-one implies F is onto
  proof
    assume F is one-to-one; then
A12: card dom F=card (F.:dom F) by CARD_1:5,CARD_1:33;
    assume F is not onto;
    then not rng F = Y by FUNCT_2:def 3;
    then not Y c= rng F;
    then consider y being object such that
A13: y in Y and
A14: not y in rng F;
A15: card rng F <=card (Y\{y}) by A14,NAT_1:43,ZFMISC_1:34;
A16: F.:dom F= rng F by RELAT_1:113;
{y} meets Y by A13,ZFMISC_1:48;
then A17:Y\{y} <>Y by XBOOLE_1:83;
Y\{y} c< Y by A17;
then    card (Y\{y})< card Y by CARD_2:48;
    hence thesis by A1,A13,A15,A12,A16,FUNCT_2:def 1;
  end;
end;

theorem Th1:
  x in i implies x is Element of NAT
proof
  i c= NAT;
  hence thesis;
end;

begin

theorem Th2:
  for X0 being finite natural-membered set holds ex n st X0 c= Segm n
proof
  let X0 be finite natural-membered set;
  consider p being Function such that
A1: rng p = X0 and
A2: dom p in NAT by FINSET_1:def 1;
  reconsider np=dom p as Element of NAT by A2;
  np=dom p;
  then reconsider p as XFinSequence by AFINSQ_1:5;
  X0 c= NAT by MEMBERED:6;
  then reconsider p as XFinSequence of NAT by A1,RELAT_1:def 19;
  defpred P[Nat] means ex n st for i st i in Segm $1 & $1-'1 in
  dom p holds p.i in n;
A3: for k st P[k] holds P[k+1]
  proof
    let k;
    assume P[k];
    then consider n such that
A4: for i st i in k & k-'1 in dom p holds p.i in n;
    per cases;
    suppose
A5:   k+1-1 <len p;
      set m=p.(k);
      set m2=max(n,m+1);
      k-'1<=k by NAT_D:35;
      then k-'1 < len p by A5,XXREAL_0:2;
      then
A6:   k-'1 in dom p by AFINSQ_1:86;
      for i st i in Segm(k+1) & k+1-'1 in dom p holds p.i in Segm m2
      proof
        let i;
        assume that
A7:     i in Segm(k+1) and
        k+1-'1 in dom p;
A8:     i<k+1 by A7,NAT_1:44;
        per cases;
        suppose
A9:       i<k;
          set k0=p.i;
          i in Segm k by A9,NAT_1:44;
          then p.i in Segm n by A4,A6;
          then k0<n by NAT_1:44;
          hence thesis by NAT_1:44,XXREAL_0:30;
        end;
        suppose
A10:      i>=k;
          m<m+1 by XREAL_1:29;
          then
A11:      m<m2 by XXREAL_0:30;
          i<=k by A8,NAT_1:13;
          then p.i=m by A10,XXREAL_0:1;
          hence thesis by A11,NAT_1:44;
        end;
      end;
      hence thesis;
    end;
    suppose
A12:  k+1-1>=len p;
      k+1-'1=k by NAT_D:34;
      then
      for i st i in (k+1) & (k+1)-'1 in dom p holds p.i in 2
               by A12,AFINSQ_1:86;
      hence thesis;
    end;
  end;
  for i st i in 0 & 0-'1 in dom p holds p.i in 0;
  then
A13: P[0];
  for k holds P[k] from NAT_1:sch 2(A13,A3);
  then consider n such that
A14: for i st i in Segm len p & len p -'1 in dom p holds p.i in n;
  rng p c= Segm n
  proof
    let y be object;
    assume y in rng p;
    then consider x being object such that
A15: x in dom p and
A16: y=p.x by FUNCT_1:def 3;
A17: len p -1<len p by XREAL_1:44;
    0 < len p by A15;
    then (0 qua Element of NAT )+1 <= len p by NAT_1:13;
    then len p-'1=len p-1 by XREAL_1:233;
    then len p -'1 in dom p by A17,AFINSQ_1:86;
    hence thesis by A14,A15,A16;
  end;
  hence thesis by A1;
end;

theorem Th3: :: from FINSEQ_2:11
x in rng p implies ex
  i being Element of NAT st i in dom p & p.i = x
proof
  assume x in rng p;
  then ex a being object st a in dom p & x = p.a by FUNCT_1:def 3;
  hence thesis;
end;

theorem Th4: ::from FINSEQ_2:14
  for p st for i st i in dom p holds p.i in D
   holds p is XFinSequence of D
proof
  let p;
  assume
A1: for i st i in dom p holds p.i in D;
  rng p c= D
  proof
    let x be object;
    assume x in rng p;
    then ex i being Element of NAT st i in dom p & p.i = x by Th3;
    hence thesis by A1;
  end;
  hence thesis by RELAT_1:def 19;
end;

scheme
  XSeqLambdaD{i()->Nat,D()->non empty set,F(set)->Element of D()}:
  ex p being XFinSequence of D() st len p = i() &
    for j st j in i() holds p.j = F(j)
proof
  consider z being XFinSequence such that
A1: len z = i() and
A2: for i st i in i() holds z.i = F(i) from
  AFINSQ_1:sch 2;
  for j be Nat st j in i() holds z.j in D()
  proof
    let j be Nat;
    reconsider j0=j as Element of NAT by ORDINAL1:def 12;
    assume j in i();
    then z.j0 = F(j0) by A2;
    hence thesis;
  end;
  then reconsider z as XFinSequence of D() by A1,Th4;
  take z;
  thus len z = i() by A1;
  let j be Nat;
  thus thesis by A2;
end;



registration
  cluster empty natural-valued for XFinSequence;
  existence
proof
  take the empty XFinSequence of NAT;
  thus thesis;
end;
  let p be complex-valued Sequence-like Function;
  cluster -p -> Sequence-like;
  coherence
proof
  dom p = dom -p & dom p is ordinal by VALUED_1:8;
  hence thesis;
end;
  cluster p" -> Sequence-like;
  coherence
proof
  dom p = dom (p") by VALUED_1:def 7;
  hence thesis;
end;
  cluster p^2 -> Sequence-like;
  coherence
proof
  dom p = dom (p^2) by VALUED_1:11;
  hence thesis;
end;
cluster abs p -> Sequence-like;
  coherence
proof
    dom p = dom abs p by VALUED_1:def 11;
  hence thesis;
end;
  let q be complex-valued Sequence-like Function;
  cluster p+q -> Sequence-like;
  coherence
proof
  dom (p+q)=dom p /\dom q & dom p is ordinal & dom q is ordinal
      by VALUED_1:def 1;
   hence thesis;
end;
  cluster p-q -> Sequence-like;
  coherence;
  cluster p(#)q -> Sequence-like;
  coherence
proof
  dom (p(#)q)=dom p /\dom q & dom p is ordinal & dom q is ordinal
      by VALUED_1:def 4;
   hence thesis;
end;
  cluster p/"q -> Sequence-like;
  coherence;
end;

registration
  let p be complex-valued finite Function;
  cluster -p -> finite;
  coherence
proof
  dom p = dom -p by VALUED_1:8;
  hence thesis by FINSET_1:10;
end;
  cluster p" -> finite;
  coherence
proof
  dom p = dom (p") by VALUED_1:def 7;
  hence thesis by FINSET_1:10;
end;
  cluster p^2 -> finite;
  coherence
proof
  dom p = dom (p^2) by VALUED_1:11;
  hence thesis by FINSET_1:10;
end;
  cluster abs p -> finite;
  coherence
proof
    dom p = dom abs p by VALUED_1:def 11;
  hence thesis by FINSET_1:10;
end;
  let q be complex-valued Function;
  cluster p+q -> finite;
  coherence
proof
  dom (p+q)=dom p /\dom q by VALUED_1:def 1;
   hence thesis by FINSET_1:10;
end;
  cluster p-q -> finite;
  coherence;
  cluster p(#)q -> finite;
  coherence
proof
  dom (p(#)q)=dom p /\dom q by VALUED_1:def 4;
   hence thesis by FINSET_1:10;
end;
  cluster p/"q -> finite;
  coherence;
  cluster q/"p -> finite;
  coherence;
end;

registration
  let p be complex-valued Sequence-like Function;
  let c be Complex;
  cluster c+p -> Sequence-like;
  coherence
proof
  dom p = dom (c+p) by VALUED_1:def 2;
  hence thesis;
end;
  cluster p-c -> Sequence-like;
  coherence;
  cluster c(#)p -> Sequence-like;
  coherence
proof
  dom p = dom (c(#)p) by VALUED_1:def 5;
  hence thesis;
end;
end;

registration
  let p be complex-valued finite Function;
  let c be Complex;
  cluster c+p -> finite;
  coherence
proof
  dom p = dom (c+p) by VALUED_1:def 2;
  hence thesis by FINSET_1:10;
end;
  cluster p-c -> finite;
  coherence;
  cluster c(#)p -> finite;
  coherence
proof
  dom p = dom (c(#)p) by VALUED_1:def 5;
  hence thesis by FINSET_1:10;
end;
end;



definition
  let p;
  func Rev p -> XFinSequence means
  :Def1:
  len it = len p & for i st i in dom it holds it.i = p.(len p - (i + 1));
  existence
  proof
    deffunc F(Nat) = p.(len p - ($1 + 1));
    ex q st len q = len p & for k
    st k in len p holds q.k = F(k) from AFINSQ_1:sch 2;
    hence thesis;
  end;
  uniqueness
  proof
    let f1,f2 be XFinSequence such that
A1: len f1 = len p and
A2: for i st i in dom f1 holds f1.i = p.(len p -(i + 1)) and
A3: len f2 = len p and
A4: for i st i in dom f2 holds f2.i = p.(len p -(i + 1));
    now
      let i;
      assume
A5:   i in dom p;
      then f1.i = p.(len p - (i + 1)) by A1,A2;
      hence f1.i = f2.i by A3,A4,A5;
    end;
    hence thesis by A1,A3;
  end;
end;

theorem Th5: ::from FINSEQ_5:60
  dom p = dom Rev p & rng p = rng Rev p
proof
  thus
A1: dom p = len p
    .= len (Rev p) by Def1
    .= dom(Rev p);
A2: len p = len(Rev p) by Def1;
  hereby
    let x be object;
    assume x in rng p;
    then consider z being object such that
A3: z in dom p and
A4: p.z = x by FUNCT_1:def 3;
    reconsider i=z as Element of NAT by A3;
    i+1<=len p by NAT_1:13,A3,AFINSQ_1:86;
    then len p -'(i+1)=len p -(i+1) by XREAL_1:233;
    then reconsider j = len p - (i + 1) as Element of NAT;
A5: j in len (Rev p) by A2,AFINSQ_1:86,XREAL_1:44;
    then (Rev p).j = p.(len p - (j + 1)) by Def1;
    hence x in rng(Rev p) by A4,A5,FUNCT_1:def 3;
  end;
  let x be object;
  assume x in rng(Rev p);
  then consider z being object such that
A6: z in dom(Rev p) and
A7: (Rev p).z = x by FUNCT_1:def 3;
  reconsider i=z as Element of NAT by A6;
  i < len p by A2,A6,AFINSQ_1:86;
  then i+1<=len p by NAT_1:13;
  then len p -'(i+1)=len p -(i+1) by XREAL_1:233;
  then reconsider j = len p - (i + 1) as Element of NAT;
  len p -(i+1)<len p by XREAL_1:44;
  then
A8: j in len (Rev p) by A2,AFINSQ_1:86;
  (Rev p).i = p.(len p - (i + 1)) by A6,Def1;
  hence thesis by A1,A7,A8,FUNCT_1:def 3;
end;

registration
  let D be set, f be XFinSequence of D;
  cluster Rev f -> D -valued;
  coherence
  proof
    rng f=rng (Rev f) by Th5;
    hence thesis by RELAT_1:def 19;
  end;
end;

definition
  let p,n;
  func p /^ n -> XFinSequence means  :Def2:
  len it = len p -' n & for m st m in dom it holds it.m = p.(m+n);
  existence
  proof
    thus ex p1 be XFinSequence st len p1 = len p -' n & for m st m in
    dom p1 holds p1.m = p.(m+n)
    proof
      deffunc F(Nat)=p.($1+n);
      set k = len p -' n;
      consider q  such that
A1:   len q = k & for m2 be Nat st m2 in k holds q.m2 = F(
      m2) from AFINSQ_1:sch 2;
      take q;
      thus thesis by A1;
    end;
  end;
  uniqueness
  proof
    let p1,p2 be XFinSequence;
    thus (len p1 = len p -' n & for m be Nat st m in dom p1 holds p1.m = p.(m+
n)) & (len p2 = len p -' n & for m be Nat st m in dom p2 holds p2.m = p.(m+n))
    implies p1 = p2
    proof
      assume that
A2:   len p1 = len p -' n and
A3:   for m st m in dom p1 holds p1.m = p.(m+n) and
A4:   len p2 = len p -' n and
A5:   for m st m in dom p2 holds p2.m = p.(m+n);
      now
        let m;
        assume
A6:     m in dom p1;
        then p1.m = p.(m+n) by A3;
        hence p1.m = p2.m by A2,A4,A5,A6;
      end;
      hence thesis by A2,A4;
    end;
  end;
end;

theorem Th6:
  n >= len p implies p/^n={}
proof
  assume n>=len p;
  then len p-'n=0 by NAT_2:8;
  then len (p/^n)=0 by Def2;
  hence thesis;
end;

theorem Th7:
  n < len p implies len (p/^n) = len p -n
proof
  assume n < len p;
  then len p-'n=len p-n by XREAL_0:def 2,XREAL_1:48;
  hence thesis by Def2;
end;

theorem Th8:
  m+n<len p implies (p/^n).m = p.(m+n)
proof
  assume
A1: m+n<len p;
  then
A2: m<len p-n by XREAL_1:20;
  len (p/^n)=len p-n by A1,Th7,NAT_1:12;
  hence thesis by Def2,A2,AFINSQ_1:86;
end;

registration
  let f be one-to-one XFinSequence, n;
  cluster f/^n -> one-to-one;
  coherence
  proof
    let x,y be object;
    assume that
A1: x in dom (f/^n) and
A2: y in dom (f/^n) and
A3: (f/^n).x=(f/^n).y;
    reconsider nx=x,ny=y as Nat by A1,A2;
A4: nx<len (f/^n) by A1,AFINSQ_1:86;
A5: len (f/^n)=len f-'n by Def2;
A6: ny<len (f/^n) by A2,AFINSQ_1:86;
    per cases;
    suppose
      n<=len f;
      then
A7:   len f-'n=len f-n by XREAL_1:233;
      then
A8:   nx+n<len f by A4,A5,XREAL_1:20;
      then
A9:   nx+n in dom f by AFINSQ_1:86;
A10:  ny+n<len f by A6,A5,A7,XREAL_1:20;
      then
A11:  ny+n in dom f by AFINSQ_1:86;
A12:  (f/^n).ny=f.(ny+n) by A10,Th8;
      (f/^n).nx=f.(nx+n) by A8,Th8;
      then nx+n=ny+n by A3,A9,A12,A11,FUNCT_1:def 4;
      hence thesis;
    end;
    suppose
      n>len f;
      then f/^n={} by Th6;
      hence thesis by A1;
    end;
  end;
end;

theorem Th9:
  rng (p/^n) c= rng p
proof
  thus rng (p/^n) c= rng p
  proof
    let z be object;
    assume z in rng (p/^n);
    then consider x being object such that
A1: x in dom (p/^n) and
A2: z=(p/^n).x by FUNCT_1:def 3;
    reconsider nx=x as Element of NAT by A1;
    nx<len (p/^n) by A1,AFINSQ_1:86;
    then
A3: nx < len p -' n by Def2;
    per cases;
    suppose
      n<len p;
      then len p-'n=len p-n by XREAL_1:233; then
A4:   nx+n in dom p by AFINSQ_1:86,A3,XREAL_1:20;
      (p/^n).nx=p.(nx+n) by A1,Def2;
      hence thesis by A2,A4,FUNCT_1:def 3;
    end;
    suppose
      n>=len p;
      then (p/^n)={} by Th6;
      hence thesis by A1;
    end;
  end;
end;

theorem Th10: ::FINSEQ_5:31
 p/^0 = p
proof
  per cases;
  suppose
A1: 0 <len p;
A2: now
      let i;
      assume i < len(p/^0);
      hence (p/^0).i = p.(i+(0 qua Element of NAT)) by Def2,AFINSQ_1:86
        .= p.i;
    end;
    len(p/^0) = len p - 0 by A1,Th7
      .= len p;
    hence thesis by A2,AFINSQ_1:9;
  end;
  suppose
A3: 0>=len p;
    then p/^0 ={} by Th6;
    hence thesis by A3;
  end;
end;

theorem Th11: ::FINSEQ_5:39
  (p^q)/^(len p + i) = q/^i
proof
A1: len(p^q) = len p + len q by AFINSQ_1:17;
  per cases;
  suppose
A2: i < len q;
    then len p + i < len p + len q by XREAL_1:6;
    then len p +i<len (p^q) by AFINSQ_1:17;
    then
A3: len((p^q)/^(len p + i)) = len (p^q)-(len p +i) by Th7
      .=len q + len p - (len p + i) by AFINSQ_1:17
      .= len q - i
      .= len(q/^i) by A2,Th7;
    now
      let k;
      assume
A4:   k < len(q/^i);
      then
A5:   k in dom(q/^i) by AFINSQ_1:86;
      k < len q -i by A2,A4,Th7;
      then
A6:   i+k in dom q by AFINSQ_1:86,XREAL_1:20;
      k in dom((p^q)/^(len p + i)) by A3,A4,AFINSQ_1:86;
      hence ((p^q)/^(len p + i)).k = (p^q).(len p + i + k) by Def2
        .= (p^q).(len p + (i+k))
        .= q.(i+k) by A6,AFINSQ_1:def 3
        .= (q/^i).k by A5,Def2;
    end;
    hence thesis by A3,AFINSQ_1:9;
  end;
  suppose
A7: i >= len q;
    hence (p^q)/^(len p+i) = {} by Th6,A1,XREAL_1:6
      .= q/^i by A7,Th6;
  end;
end;

theorem Th12: ::FINSEQ_5:40
  (p^q)/^(len p) = q
proof
  thus (p^q)/^(len p) = (p^q)/^(len p + (0 qua Element of NAT))
    .= q/^0 by Th11
    .= q by Th10;
end;

theorem Th13: ::RFINSEQ:21
  (p|n)^(p/^n) = p
proof
  set pn = p/^n;
  now
    per cases;
    case
A1:   len p<=n;
      p/^n = {} by A1,Th6;
      hence thesis by A1,AFINSQ_1:52;
    end;
    case
A2:   n<len p;
      set g=p|n;
A3:   len (g) = n by A2,AFINSQ_1:54;
A4:   len pn = len p - n by A2,Th7;
A5:   now
        let m;
        assume
A6:     m < len p;
        now
          per cases;
          case
            m<n;
            then
A7:         m in Segm n by NAT_1:44;
            hence ((p|n)^(p/^n)).m = (p|n).m by A3,AFINSQ_1:def 3
              .= p.m by A2,A7,AFINSQ_1:53;
          end;
          case
            n<=m;
            then max(0,m-n) = m-n by FINSEQ_2:4;
            then reconsider k = m-n as Element of NAT by FINSEQ_2:5;
            k< len pn by A4,A6,XREAL_1:9;
            then
A8:         k in dom pn by AFINSQ_1:86;
            m=len (p|n) +k by A3;
            hence ((p|n) ^ (p/^n)).m = pn.k by A8,AFINSQ_1:def 3
              .= p.(k+n) by A8,Def2
              .= p.m;
          end;
        end;
        hence ((p|n) ^ (p/^n)).m = p.m;
      end;
      len (g^(p/^n)) = n+(len p - n) by A4,A3,AFINSQ_1:17
        .= len p;
      hence thesis by A5,AFINSQ_1:9;
    end;
  end;
  hence thesis;
end;

registration
  let f be XFinSequence;
  cluster f|0 -> empty;
  coherence;
  let n be Nat;
  cluster f/^(dom f + n) -> empty;
  coherence
  proof
    len f <= len f + n + 0 by NAT_1:11; then
    (len f) - (len f + n) <= 0 by XREAL_1:20; then
    (len f) -' (len f + n) = 0 by XREAL_0:def 2; then
    len (f/^(dom f + n)) = 0 by Def2;
    hence thesis;
  end;
  reduce f|(len f + n) to f;
  reducibility
  proof
    len f + n >= len f + 0 by XREAL_1:6;
    hence thesis by AFINSQ_1:52;
  end;
  reduce (f|n)^(f/^n) to f;
  reducibility by Th13;
end;

registration
  let D be set, f be XFinSequence of D, n;
  cluster f /^ n -> D -valued;
  coherence
  proof
    deffunc F(Element of NAT)=f.($1+n);
    set p = f /^ n;
    per cases;
    suppose
A1:   n<len f;
      then reconsider k = len f - n as Nat by NAT_1:21;
A2:   len p = k by A1,Th7;
A3:   rng p c= rng f
      proof
        let x be object;
        assume x in rng p;
        then consider m being Element of NAT such that
A4:     m in dom p and
A5:     p.m = x by Th3;
        m+n<k+n by A2,XREAL_1:6,A4,AFINSQ_1:86;
        then
A6:     m+n in dom f by AFINSQ_1:86;
        p.m = f.(m+n) by A4,Def2;
        hence thesis by A5,A6,FUNCT_1:def 3;
      end;
      for f2 being XFinSequence st rng f2 c= D holds f2 is XFinSequence
      of D by RELAT_1:def 19;
      hence thesis by A3,XBOOLE_1:1;
    end;
    suppose
      len f <= n;
      then f /^ n = <%>D by Th6;
      hence thesis;
    end;
  end;
end;

reserve k1,k2 for Nat;

definition
  let p,k1,k2;
  func mid(p,k1,k2) -> XFinSequence equals
  (p|k2)/^(k1-'1);
  coherence;
end;

theorem Th14:
  k1>k2 implies mid(p,k1,k2) = {}
proof
  set k21=k2;
A1: len (p|k21)<=k21 by AFINSQ_1:55;
  assume
A2: k1>k2;
  then k1>= (0 qua Nat) +1 by NAT_1:13;
  then
A3: k1-'1=k1-1 by XREAL_1:233;
  k1>=k2+1 by A2,NAT_1:13;
  then k1-1>=k2+1-1 by XREAL_1:9;
  hence thesis by A3,A1,Th6,XXREAL_0:2;
end;

theorem
  1<=k1 & k2<=len p implies mid(p,k1,k2) = (p/^(k1-'1))|(k2+1-'k1)
proof
  assume that
A1: 1<=k1 and
A2: k2<=len p;
  set k11=k1,k21=k2;
A3: len (p|k21)=k21 by A2,AFINSQ_1:54;
  k1<k1+1 by NAT_1:13;
  then k1-1<k1+1-1 by XREAL_1:9;
  then
A4: k1-'1<k1 by A1,XREAL_1:233;
  per cases;
  suppose
A5: k1<=k2;
A6: k2<k2+1 by XREAL_1:29;
    then
A7: k2+1-'k1 =k2+1-k1 by A5,XREAL_1:233,XXREAL_0:2
      .=k2-(k1-1);
A8: k11-'1=k11-1 by A1,XREAL_1:233;
    k11-1<k11 by XREAL_1:44;
    then k11-1<k21 by A5,XXREAL_0:2;
    then
A9: len (mid(p,k1,k2))=k21-(k11-1) by A3,A8,Th7;
    then
A10: len (mid(p,k1,k2))=k21+1-k11;
    k1-'1<k2 by A4,A5,XXREAL_0:2;
    then k1-'1<len p by A2,XXREAL_0:2;
    then len (p/^(k1-'1))=len p -(k1-'1) by Th7;
    then
A11: k2+1-'k1<= len (p/^(k1-'1)) by A2,A8,A7,XREAL_1:9;
A12:  i<len (mid(p,k1,k2)) implies (mid(p,k1,k2
    )).i=((p/^(k1-'1))|(k2+1-'k1)).i
    proof
      assume
A13:  i<len (mid(p,k1,k2));
      then
A14:  (i+(k11-'1)) in Segm k21 by NAT_1:44,A8,A9,XREAL_1:20;
      i+(k1-'1)<k21-(k11-1)+(k1-'1) by A9,A13,XREAL_1:6;
      then
A15:  i+(k1-'1)<len p by A2,A8,XXREAL_0:2;
      i+(k11-1)<k21 by A9,A13,XREAL_1:20;
      then
A16:  ((p|k21)/^(k11-'1)).i=(p|k21).(i+(k11-'1)) by A3,A8,Th8;
      i in k2+1-'k1 by A7,A9,A13,AFINSQ_1:86;
      then ((p/^(k1-'1))|(k2+1-'k1)).i=(p/^(k1-'1)).i by A11,AFINSQ_1:53
        .=p.(i+(k1-'1)) by A15,Th8;
      hence thesis by A2,A16,A14,AFINSQ_1:53;
    end;
    len ((p/^(k1-'1))|(k2+1-'k1))=k2+1-'k1 by A11,AFINSQ_1:54;
    then len (mid(p,k1,k2))= len ((p/^(k1-'1))|(k2+1-'k1)) by A5,A6,A10,
XREAL_1:233,XXREAL_0:2;
    hence thesis by A12,AFINSQ_1:9;
  end;
  suppose
A17: k1>k2;
    then k2+1<=k1 by NAT_1:13;
    then
A18: k2+1-'k1=0 by NAT_2:8;
    mid(p,k1,k2)={} by A17,Th14;
    hence thesis by A18;
  end;
end;

theorem Th16: :: FINSEQ_8:5
  mid(p,1,k)=p|k
proof
  1-'1=0 by XREAL_1:232;
  hence thesis by Th10;
end;

theorem :: FINSEQ_8:6
  len p<=k implies mid(p,1,k)=p
proof
  assume
A1: len p<=k;
  thus mid(p,1,k)=p|k by Th16
    .=p by A1,AFINSQ_1:52;
end;

theorem :: FINSEQ_8:8
  mid(p,0,k)=mid(p,1,k)
proof
A1: 0-'1=0 by NAT_2:8;
  mid(p,1,k) = (p|k) by Th16;
  hence thesis by A1,Th10;
end;

theorem :: FINSEQ_8:9
  mid(p^q,len p+1,len p+len q)=q
proof
A1: (len p +1)-'1=len p by NAT_D:34;
  len (p^q)=len p + len q by AFINSQ_1:17;
  hence thesis by A1,Th12;
end;

registration
  let D be set, f be XFinSequence of D, k1,k2;
  cluster mid(f,k1,k2) -> D-valued;
  coherence;
end;

begin :: Selected Subsequences

definition
  let X be finite natural-membered set;
  func Sgm0 X -> XFinSequence of NAT means  :Def4:
  rng it = X & for l,m,k1,k2 being Nat st
    l < m & m < len it & k1=it.l & k2=it.m holds k1 < k2;
  existence
  proof
    defpred P[Nat] means for X being set st X c= Segm $1
  ex p being XFinSequence of
NAT st rng p = X & for l,m,k1,k2 being Nat st ( l < m & m < len p & k1=p.l & k2
    =p.m) holds k1 < k2;
A1: ex k being Nat st X c= Segm k by Th2;
A2: for k being Nat st P[k] holds P[k+1]
    proof
      let k be Nat such that
A3:   for X being set st X c= Segm k
     ex p being XFinSequence of NAT
st rng p = X & for l,m,k1,k2 be Nat st l < m & m < len p & k1=p.l & k2=p.m
      holds k1 < k2;
      let X be set;
      assume
A4:   X c= Segm(k+1);
      now
        set Y=X\{k};
        assume not X c= k;
        then consider x being object such that
A5:     x in X and
A6:     not x in Segm k;
        reconsider n=x as Element of NAT by A4,A5,Th1;
        n<k+1 by A4,A5,NAT_1:44;
        then
A7:     n<=k by NAT_1:13;
        not n<k by A6,NAT_1:44;
        then
A8:     n=k by A7,XXREAL_0:1;
A9:     Y c= Segm k
        proof
          let x be object;
          assume
A10:      x in Y; then
          reconsider m=x as Element of NAT by A4,Th1;
          not x in {k} by A10,XBOOLE_0:def 5;
          then
A12:      m<>k by TARSKI:def 1;
          m<k+1 by A4,A10,NAT_1:44;
          then m<=k by NAT_1:13;
          then m <k by A12,XXREAL_0:1;
          hence thesis by NAT_1:44;
        end;
        then consider p being XFinSequence of NAT such that
A13:    rng p = Y and
A14:    for l,m,k1,k2 be Nat st l < m & m < len p & k1=p.l & k2=p.m
        holds k1 < k2 by A3;
        reconsider k as Element of NAT by ORDINAL1:def 12;
        consider q being XFinSequence of NAT such that
A15:    q=p^<% k %>;
A16:    for l,m,k1,k2 be Nat st l < m & m < len q & k1=q.l & k2=q.m holds
        k1 < k2
        proof
          let l,m,k1,k2 be Nat;
          assume that
A17:      l < m and
A18:      m < len q and
A19:      k1=q.l and
A20:      k2=q.m;
          m+1<=len q by A18,NAT_1:13;
          then
A21:      m<=len q -1 by XREAL_1:19;
          then l < len (p^<% k %>) -1 by A15,A17,XXREAL_0:2;
          then l < len p + len <% k %> -1 by AFINSQ_1:17;
          then l < len p + 1 -1 by AFINSQ_1:34;
          then
A22:      l in dom p by AFINSQ_1:86;
A23:      m<=len q-'1 by A21,XREAL_0:def 2;
A24:      now
A25:        k1 = p.l by A15,A19,A22,AFINSQ_1:def 3;
            assume m <> len q -'1;
            then m < len (p^<% k %>) -'1 by A15,A23,XXREAL_0:1;
            then m < len p + len <% k %> -'1 by AFINSQ_1:17;
            then m < len p + 1 -'1 by AFINSQ_1:34;
            then
A26:        m < len p by NAT_D:34;
            then m in dom p by AFINSQ_1:86;
            then k2 = p.m by A15,A20,AFINSQ_1:def 3;
            hence thesis by A14,A17,A26,A25;
          end;
          now
            assume m=len q -'1;
            then
A27:        q.m = (p^<% k %>).((len p + len <% k %>)-'1) by A15,AFINSQ_1:17
              .= (p^<% k %>).((len p + 1)-'1) by AFINSQ_1:34
              .=(p^<% k %>).(len p) by NAT_D:34
              .= k by AFINSQ_1:36;
            k1 = p.l by A15,A19,A22,AFINSQ_1:def 3;
            then k1 in Y by A13,A22,FUNCT_1:def 3;
            hence thesis by A9,A20,A27,NAT_1:44;
          end;
          hence thesis by A24;
        end;
A28:    {k} c= X by A5,A8,ZFMISC_1:31;
        rng q = rng p \/ rng <% k %> by A15,AFINSQ_1:26
          .= Y \/ {k} by A13,AFINSQ_1:33
          .= X \/ {k} by XBOOLE_1:39
          .= X by A28,XBOOLE_1:12;
        hence thesis by A16;
      end;
      hence thesis by A3;
    end;
A29: P[0]
    proof
      let X be set;
      assume
A30:  X c= Segm 0;
      take <%>(NAT);
      thus rng <%>(NAT) = X by A30;
      thus thesis;
    end;
    for k2 being Nat holds P[k2] from NAT_1:sch 2(A29,A2);
    hence thesis by A1;
  end;
  uniqueness
  proof
    defpred S[XFinSequence] means for X st ex k being Nat st X c= k holds ($1
is XFinSequence of NAT & rng $1 = X & for l,m,k1,k2 being Nat st ( l < m & m <
len $1 & k1=$1.l & k2=$1.m) holds k1 < k2) implies for q being XFinSequence of
NAT st rng q = X & for l,m,k1,k2 being Nat st ( l < m & m < len q & k1=q.l & k2
    =q.m) holds k1 < k2 holds q=$1;
    let p,q be XFinSequence of NAT such that
A31: rng p = X and
A32: for l,m,k1,k2 being Nat st l < m & m < len p & k1=p.l & k2=p.m
    holds k1 < k2 and
A33: rng q = X and
A34: for l,m,k1,k2 being Nat st l < m & m < len q & k1=q.l & k2=q.m
    holds k1 < k2;
A35: for p being XFinSequence,x be object st S[p] holds S[p^<% x %>]
    proof
      let p be XFinSequence,x be object;
      assume
A36:  S[p];
      let X be set;
      given k being Nat such that
A37:  X c= k;
      assume that
A38:  p^<% x %> is XFinSequence of NAT and
A39:  rng (p^<% x %>) = X and
A40:  for l,m,k1,k2 being Nat st l < m & m < len(p^<%x%>) & k1=(p^<%
      x %>).l & k2=(p^<% x %>).m holds k1 < k2;
      let q be XFinSequence of NAT;
      assume that
A41:  rng q = X and
A42:  for l,m,k1,k2 being Nat st l < m & m < len q & k1=q.l & k2=q.m
      holds k1 < k2;
      deffunc F(Nat) = q.$1;
      len q <> 0
      proof
        assume len q = 0;
        then p^<%x%> = {} by A39,A41,AFINSQ_1:15,RELAT_1:38;
        then 0 = len (p^<%x%>)
          .= len p + len <%x%> by AFINSQ_1:17
          .= 1 + len p by AFINSQ_1:34;
        hence contradiction;
      end;
      then consider n be Nat such that
A43:  len q = n+1 by NAT_1:6;
A44:  ex m being Nat st m=x & for l being Nat st l in X & l <> x holds l
      < m
      proof
        <%x%> is XFinSequence of NAT by A38,AFINSQ_1:31;
        then rng <%x%> c= NAT by RELAT_1:def 19;
        then {x} c= NAT by AFINSQ_1:33;
        then reconsider m=x as Element of NAT by ZFMISC_1:31;
        take m;
        thus m=x;
        thus for l being Nat st l in X & l <> x holds l < m
        proof
          len <%x%>=1 by AFINSQ_1:34;
          then
A45:      m= (p^<%x%>).(len p + len <%x%> -1) by AFINSQ_1:36
            .= (p^<%x%>).(len(p^<%x%>) -1) by AFINSQ_1:17;
          len(p^<%x %>)<len(p^<%x %>) +1 by XREAL_1:29;
          then
A46:      len(p^<%x%>)-1 < len(p^<%x %>) by XREAL_1:19;
          let l be Nat;
          assume that
A47:      l in X and
A48:      l <> x;
          consider y being object such that
A49:      y in dom (p^<%x%>) and
A50:      l=(p^<%x%>).y by A39,A47,FUNCT_1:def 3;
          reconsider k=y as Element of NAT by A49;
          k < len (p^<%x%>) by A49,AFINSQ_1:86;
          then k < len p + len <%x%> by AFINSQ_1:17;
          then k < len p + 1 by AFINSQ_1:34;
          then
A51:      k<=len p by NAT_1:13;
          k <> len p by A48,A50,AFINSQ_1:36;
          then k< len p +1-1 by A51,XXREAL_0:1;
          then k < len p + len <%x%>-1 by AFINSQ_1:34;
          then
A52:      k < len(p^<%x%>)-1 by AFINSQ_1:17;
          then len(p^<%x %>) -'1=len(p^<%x %>)-1 by XREAL_0:def 2;
          hence thesis by A40,A50,A52,A46,A45;
        end;
      end;
      then reconsider m = x as Nat;
A53:  not x in rng p
      proof
        len p + 1 = len p + len <%x%> by AFINSQ_1:34
          .= len (p^<%x%>) by AFINSQ_1:17;
        then
A54:    len p < len (p^<%x%>) by XREAL_1:29;
A55:    m = (p^<%x%>).(len p ) by AFINSQ_1:36;
        assume x in rng p;
        then consider y being object such that
A56:    y in dom p and
A57:    x=p.y by FUNCT_1:def 3;
        reconsider y as Element of NAT by A56;
A58:    y < len p by A56,AFINSQ_1:86;
        m = (p^<%x%>).y by A56,A57,AFINSQ_1:def 3;
        hence contradiction by A40,A58,A54,A55;
      end;
A59:  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
A60:      z in rng p \/ {x} \ {x};
          then not z in {x} by XBOOLE_0:def 5;
          hence thesis by A60,XBOOLE_0:def 3;
        end;
        assume
A61:    z in rng p;
        then
A62:    z in rng p \/ {x} by XBOOLE_0:def 3;
        not z in {x} by A53,A61,TARSKI:def 1;
        hence thesis by A62,XBOOLE_0:def 5;
      end;
      deffunc Q(set) =q.$1;
      consider q9 being XFinSequence such that
A63:  len q9 = n and
A64:  for m be Nat st m in n holds q9.m = Q(m)
       from AFINSQ_1:sch 2;
      now
        let x be object;
        assume x in rng q9;
        then consider y being object such that
A65:    y in dom q9 and
A66:    x=q9.y by FUNCT_1:def 3;
        reconsider y as Element of NAT by A65;
        q.y in NAT;
        hence x in NAT by A63,A64,A65,A66;
      end;
      then rng q9 c= NAT;
      then reconsider f=q9 as XFinSequence of NAT by RELAT_1:def 19;
A67:  p is XFinSequence of NAT by A38,AFINSQ_1:31;
A68:  for m be Nat st m in dom <%x%> holds q.(len q9 + m)
      = <%x%>.m
      proof
        let m be Nat;
        assume m in dom <%x%>;
        then m in len <%x%>;
        then
A69:    m in 1 by AFINSQ_1:34;
        Segm(0+1)= Segm 0 \/ {0} by AFINSQ_1:2;
        then
A70:    m=0 by A69,TARSKI:def 1;
        q.(len q9 + m) = x
        proof
          x in {x} by TARSKI:def 1;
          then x in rng <%x%> by AFINSQ_1:33;
          then x in rng p \/ rng <%x%> by XBOOLE_0:def 3;
          then x in rng q by A39,A41,AFINSQ_1:26;
          then consider y being object such that
A71:      y in dom q and
A72:      x=q.y by FUNCT_1:def 3;
          reconsider y as Element of NAT by A71;
          y+1<=len q by NAT_1:13,A71,AFINSQ_1:86;
          then
A73:      y <= len q -1 by XREAL_1:19;
          len q<len q+1 by XREAL_1:29;
          then len q -1 in dom q by A43,AFINSQ_1:86,XREAL_1:19;
          then
A74:      q.(len q -1) in X by A41,FUNCT_1:def 3;
          len q<len q+1 by XREAL_1:29;
          then
A75:      y <len q -1 & len q -1 < len q or y=len q-1 by A73,XREAL_1:19
,XXREAL_0:1;
          set k = q.(len q-1);
          consider d being Nat such that
A76:      d=x and
A77:      for l being Nat st l in X & l<>x holds l<d by A44;
          assume q.(len q9 + m) <> x;
          then k < d by A43,A63,A70,A77,A74;
          hence contradiction by A42,A43,A76,A72,A75;
        end;
        hence thesis by A70;
      end;
A78:  dom q = (len q9 + len <%x%>) by A43,A63,AFINSQ_1:34;
      then
A79:  q9^<%x%> = q by A63,A64,A68,AFINSQ_1:def 3;
A80:  not x in rng f
      proof
        len f + 1 = len f + len <%x%> by AFINSQ_1:34
          .= len (f^<%x%>) by AFINSQ_1:17;
        then
A81:    len f < len (f^<%x%>) by XREAL_1:29;
A82:    m = q.(len f) by A79,AFINSQ_1:36;
        assume x in rng f;
        then consider y being object such that
A83:    y in dom f and
A84:    x=f.y by FUNCT_1:def 3;
        reconsider y as Element of NAT by A83;
A85:    y < len f by A83,AFINSQ_1:86;
        m = q.y by A63,A64,A83,A84;
        hence contradiction by A42,A79,A85,A81,A82;
      end;
A86:  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
A87:      z in rng f \/ {x} \ {x};
          then not z in {x} by XBOOLE_0:def 5;
          hence thesis by A87,XBOOLE_0:def 3;
        end;
        assume
A88:    z in rng f;
        then
A89:    z in rng f \/ {x} by XBOOLE_0:def 3;
        not z in {x} by A80,A88,TARSKI:def 1;
        hence thesis by A89,XBOOLE_0:def 5;
      end;
      X = rng p \/ rng <%x%> by A39,AFINSQ_1:26
        .= rng p \/ {x} by AFINSQ_1:33;
      then
A90:  rng p = X\{x} by A59,TARSKI:2;
A91:  for l,m,k1,k2 being Nat st l < m & m < len p & k1=p.l & k2=p.m
      holds k1 < k2
      proof
        let l,m,k1,k2 be Nat;
        assume that
A92:    l < m and
A93:    m < len p and
A94:    k1=p.l and
A95:    k2=p.m;
        l < len p by A92,A93,XXREAL_0:2;
        then l in dom p by AFINSQ_1:86;
        then
A96:    k1 = (p^<%x%>).l by A94,AFINSQ_1:def 3;
        len p < len p + 1 by XREAL_1:29;
        then m < len p + 1 by A93,XXREAL_0:2;
        then m < len p + len <%x%> by AFINSQ_1:34;
        then
A97:    m < len (p^<%x%>) by AFINSQ_1:17;
        m in dom p by A93,AFINSQ_1:86;
        then k2 = (p^<%x%>).m by A95,AFINSQ_1:def 3;
        hence thesis by A40,A92,A96,A97;
      end;
A98:  for l,m,k1,k2 being Nat st l < m & m < len f & k1=f.l & k2=f.m
      holds k1 < k2
      proof
        let l,m,k1,k2 be Nat;
        assume that
A99:   l < m and
A100:   m < len f and
A101:   k1=f.l and
A102:   k2=f.m;
A103:   k2 = q.m by A64,A102,A63,A100,AFINSQ_1:86;
        l < n by A63,A99,A100,XXREAL_0:2;
        then l in Segm n by NAT_1:44;
        then
A104:   k1 = q.l by A64,A101;
        m < len q by A43,A63,A100,NAT_1:13;
        hence thesis by A42,A99,A104,A103;
      end;
      X = rng f \/ rng <%x%> by A41,A79,AFINSQ_1:26
        .= rng f \/ {x} by AFINSQ_1:33;
      then
A105: rng f = X\{x} by A86,TARSKI:2;
      ex m being Nat st X\{x} c= m by A37,XBOOLE_1:1;
      then q9 = p by A36,A91,A67,A90,A98,A105;
      hence thesis by A63,A64,A78,A68,AFINSQ_1:def 3;
    end;
A106: S[{}];
A107: for p being XFinSequence holds S[p] from AFINSQ_1:sch 3(A106,A35);
    ex k being Nat st X c= Segm k by Th2;
    hence thesis by A31,A32,A33,A34,A107;
  end;
end;

registration
  let A be finite natural-membered set;
  cluster Sgm0 A -> one-to-one;
  coherence
  proof
    for x,y being object st x in dom(Sgm0 A) & y in dom(Sgm0 A) & (Sgm0(A)).x
    = (Sgm0(A)).y & x<>y holds contradiction
    proof
      let x,y be object;
      assume that
A1:   x in dom(Sgm0 A) and
A2:   y in dom(Sgm0 A) and
A3:   (Sgm0(A)).x = (Sgm0(A)).y and
A4:   x <> y;
      reconsider i = x, j = y as Element of NAT by A1,A2;
      per cases by A4,XXREAL_0:1;
      suppose
A5:     i < j;
        j < len(Sgm0 A) by A2,AFINSQ_1:86;
        hence contradiction by A3,A5,Def4;
      end;
      suppose
A6:     j < i;
        i < len(Sgm0 A) by A1,AFINSQ_1:86;
        hence contradiction by A3,A6,Def4;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th20: :: FINSEQ_3:44
  for A being finite natural-membered set holds len(Sgm0 A) = card A
proof
  let A be finite natural-membered set;
  rng(Sgm0 A) = A by Def4;
  then (len(Sgm0 A)),A are_equipotent by WELLORD2:def 4;
  then card A = card((len(Sgm0 A))) by CARD_1:5;
  hence thesis;
end;

theorem Th21:
  for X,Y being finite natural-membered set st X c= Y & X <> {}
  holds (Sgm0 Y).0 <= (Sgm0 X).0
proof
  let X,Y be finite natural-membered set;
  assume that
A1: X c= Y and
A2: X <> {};
  reconsider X0=X as finite set;
  0 <> card X0 by A2;
  then 0 < len (Sgm0 X) by Th20;
  then
A3: 0 in dom (Sgm0 X) by AFINSQ_1:86;
A4: rng (Sgm0 Y)=Y by Def4;
  rng (Sgm0 X)=X by Def4;
  then (Sgm0 X).0 in X by A3,FUNCT_1:def 3;
  then consider x being object such that
A5: x in dom (Sgm0 Y) and
A6: (Sgm0 Y).x=(Sgm0 X).0 by A1,A4,FUNCT_1:def 3;
  reconsider nx=x as Nat by A5;
A7: nx <len (Sgm0 Y) by A5,AFINSQ_1:86;
  now
    per cases;
    case
      0<>nx;
      hence thesis by A6,A7,Def4;
    end;
    case
      0=nx;
      hence thesis by A6;
    end;
  end;
  hence thesis;
end;

theorem Th22:
  (Sgm0 {n}).0=n
proof
  len (Sgm0 {n})=card {n} by Th20;
  then 0 in dom (Sgm0 {n}) by AFINSQ_1:86;
  then
A1: (Sgm0 {n}).0 in rng (Sgm0 {n}) by FUNCT_1:def 3;
  rng (Sgm0 {n})={n} by Def4;
  hence thesis by A1,TARSKI:def 1;
end;

definition
  let B1,B2 be set;
  pred B1 <N< B2 means

  for n,m being Nat st n in B1 & m in B2 holds n<m;
end;

definition
  let B1,B2 be set;
  pred B1 <N= B2 means

  for n,m st n in B1 & m in B2 holds n <= m;
end;

theorem Th23:
  for B1,B2 being set st B1 <N< B2 holds B1/\B2/\NAT={}
proof
  let B1,B2 be set;
  assume
A1: B1 <N< B2;
  now
    set x =the  Element of B1/\B2/\NAT;
    reconsider nx=x as Nat;
    assume B1/\ B2/\NAT <> {};
    then
A2: x in B1/\B2 by XBOOLE_0:def 4;
    then
A3: nx in B2 by XBOOLE_0:def 4;
    nx in B1 by A2,XBOOLE_0:def 4;
    hence contradiction by A1,A3;
  end;
  hence thesis;
end;

theorem
  for B1,B2 being finite natural-membered set st B1 <N< B2 holds
  B1 misses B2
proof
  let B1,B2 be finite natural-membered set;
  assume
A1: B1 <N< B2;
  now
    set x = the Element of B1 /\ B2;
    assume a2: B1 meets B2; then
A3: x in B2 by XBOOLE_0:def 4;
    x in B1 by a2,XBOOLE_0:def 4;
    hence contradiction by A1,A3;
  end;
  hence thesis;
end;

theorem Th25:
  for A,B1,B2 being set st B1 <N< B2 holds A/\ B1 <N< A/\B2
proof
  let A,B1,B2 be set;
  assume
A1: B1 <N< B2;
  for n,m st n in A/\B1 & m in A/\B2 holds n<m
  proof
    let n,m;
    assume that
A2: n in A/\B1 and
A3: m in A/\B2;
A4: m in B2 by A3,XBOOLE_0:def 4;
    n in B1 by A2,XBOOLE_0:def 4;
    hence thesis by A1,A4;
  end;
  hence thesis;
end;

theorem
  for X,Y being finite natural-membered set st Y <> {} & (ex x being set
  st x in X & {x} <N= Y) holds (Sgm0 X).0 <= (Sgm0 Y).0
proof
  let X,Y be finite natural-membered set;
  assume that
A1: Y <> {} and
A2: ex x being set st x in X & {x} <N= Y;
  consider x being set such that
A3: x in X and
A4: {x} <N= Y by A2;
  0 <> card Y by A1;
  then 0 < len (Sgm0 Y) by Th20;
  then
A5: 0 in dom (Sgm0 Y) by AFINSQ_1:86;
  rng (Sgm0 Y)=Y by Def4;
  then
A6: (Sgm0 Y).0 in Y by A5,FUNCT_1:def 3;
  reconsider x0=x as Element of NAT by A3,ORDINAL1:def 12;
  set nx=x0;
  nx in {x0} by TARSKI:def 1;
  then
A7: nx<=(Sgm0 Y).0 by A4,A6;
  {x0} c= X
  by A3,TARSKI:def 1;
  then
A8: (Sgm0 X).0 <= (Sgm0 {x0}).0 by Th21;
  (Sgm0 {x0}).0=nx by Th22;
  hence thesis by A8,A7,XXREAL_0:2;
end;

theorem Th27:
  for X0,Y0 being finite natural-membered set st
    X0 <N< Y0 & i < (card X0) holds
  rng((Sgm0 (X0\/Y0))|(card X0))=X0 &
  ((Sgm0 (X0\/Y0))|(card X0)).i = (Sgm0 (X0 \/ Y0)).i
proof
  let X0,Y0 be finite natural-membered set;
  assume that
A1: X0 <N< Y0 and
A2: i < card X0;
A3: i in Segm card X0 by A2,NAT_1:44;
  set f=(Sgm0 (X0\/Y0))|(card X0);
  set f0=(Sgm0 (X0\/Y0));
  set Z={ v where v is Element of X0 \/Y0: ex k2 being Nat st v=f.k2 & k2 in
  card X0};
A4: X0 c= X0 \/ Y0 by XBOOLE_1:7;
A5: len (Sgm0 (X0\/Y0))=card (X0\/Y0) by Th20;
  then
A6: len f=card X0 by A4,AFINSQ_1:54,NAT_1:43;
A7: Z c= rng f
  proof
    let y being object;
   assume y in Z;
    then
    ex v0 being Element of X0 \/Y0 st y=v0 & ex k2 being Nat st v0=f.k2
    & k2 in card X0;
    hence thesis by A6,FUNCT_1:def 3;
  end;
  then reconsider Z0=Z as finite set;
  f is one-to-one by FUNCT_1:52;
  then
A8: dom f,(f.:(dom f)) are_equipotent by CARD_1:33;
A9: f.:(dom f)=rng f by RELAT_1:113;
A10: len f0=card (X0 \/Y0) by Th20;
A11: rng f0=X0 \/Y0 by Def4;
A12: rng f c= Z
  proof
    let y being object;
    assume
A13: y in rng f;
    then consider x being object such that
A14: x in dom f and
A15: y=f.x by FUNCT_1:def 3;
    reconsider y0=y as Element of (X0 \/Y0) by Def4,A13;
    ex k2 being Nat st y0=f.k2 & k2 in card X0 by A14,A15;
   hence thesis;
  end;
  then rng f=Z by A7;
  then card Z=card (len f) by A8,A9,CARD_1:5;
  then
A16: card Z= card X0 by A5,A4,AFINSQ_1:54,NAT_1:43;
A17: X0 \/ Y0 <> {} by A2,CARD_1:27,XBOOLE_1:15;
A18: now
    assume that
A19: not Z c= X0 and
A20: not X0 c= Z;
    consider v1 being object such that
A21: v1 in Z and
A22: not v1 in X0 by A19;
    consider v10 being Element of X0 \/Y0 such that
A23: v1=v10 and
A24: ex k2 being Nat st v10=f.k2 & k2 in card X0 by A21;
A25: v10 in Y0 by A17,A22,A23,XBOOLE_0:def 3;
    reconsider nv10 =v10 as Nat;
    consider v2 being object such that
A26: v2 in X0 and
A27: not v2 in Z by A20;
    X0 c= X0\/Y0 by XBOOLE_1:7;
    then consider x2 being object such that
A28: x2 in dom f0 and
A29: v2=f0.x2 by A11,A26,FUNCT_1:def 3;
    reconsider x20=x2 as Nat by A28;
    reconsider nv2 =v2 as Nat by A29;
A30: x20<len f0 by A28,AFINSQ_1:86;
A31: now
      assume x20 < card X0;
      then
A32:  x20 in Segm card X0 by NAT_1:44;
      card X0 <= card (X0 \/Y0) by NAT_1:43,XBOOLE_1:7;
      then card X0 <= len f0 by Th20;
      then f.x20=f0.x20 by A32,AFINSQ_1:53;
      hence contradiction by A4,A26,A27,A29,A32;
    end;
    consider k20 being Nat such that
A33: v10=f.k20 and
A34: k20 in card X0 by A24;
    card X0 <= len f0 by A10,NAT_1:43,XBOOLE_1:7;
    then
A35: f.k20=f0.k20 by A34,AFINSQ_1:53;
    k20<len f by A6,A34,AFINSQ_1:86;
    then k20<x20 by A6,A31,XXREAL_0:2;
    then nv10<nv2 by A33,A29,A35,A30,Def4;
    hence contradiction by A1,A26,A25;
  end;
A36: now
    per cases by A18;
    case
      Z0 c= X0;
      hence Z0=X0 by A16,CARD_2:102;
    end;
    case
      X0 c=Z0;
      hence Z0=X0 by A16,CARD_2:102;
    end;
  end;
  card X0 <= len f0 by A5,NAT_1:43,XBOOLE_1:7;
  hence thesis by A12,A7,A36,A3,AFINSQ_1:53;
end;

theorem
  for X,Y being finite natural-membered set st
     X <N< Y & i in card (X) holds (Sgm0 (X\/Y)).i in X
proof
  let X,Y be finite natural-membered set;
  assume that
A1: X <N< Y and
A2: i in card (X);
  set f=(Sgm0 (X\/Y))|(card X);
  set f0=(Sgm0 (X\/Y));
  set Z={ v where v is Element of X \/Y: ex k2 being Nat st v=f.k2 & k2 in
  card X};
A3: rng f0=X \/Y by Def4;
  len (Sgm0 (X\/Y))=card (X\/Y) by Th20;
  then
A4: card X <= len (Sgm0 (X\/Y)) by NAT_1:43,XBOOLE_1:7;
  then
A5: len f=card X by AFINSQ_1:54;
A6: Z c= rng f
  proof
    let y being object;
    assume y in Z;
    then
    ex v0 being Element of X \/Y st y=v0 & ex k2 being Nat st v0=f.k2 &
    k2 in card X;
    hence thesis by A5,FUNCT_1:def 3;
  end;
  then reconsider Z0=Z as finite set;
  rng f c= Z
  proof
    let y being object;
    assume
A7: y in rng f;
    then consider x being object such that
A8: x in dom f and
A9: y=f.x by FUNCT_1:def 3;
    reconsider y0=y as Element of X\/Y by A7,Def4;
    ex k2 being Nat st y0=f.k2 & k2 in card X by A8,A9;
    hence thesis;
  end;
  then
A10: rng f=Z by A6;
A11: X \/ Y <> {} by A2,CARD_1:27,XBOOLE_1:15;
A12: now
    assume that
A13: not Z c= X and
A14: not X c= Z;
    consider v1 being object such that
A15: v1 in Z and
A16: not v1 in X by A13;
    consider v10 being Element of X \/Y such that
A17: v1=v10 and
A18: ex k2 being Nat st v10=f.k2 & k2 in card X by A15;
A19: v10 in Y by A11,A16,A17,XBOOLE_0:def 3;
    reconsider nv10 =v10 as Nat;
    consider v2 being object such that
A20: v2 in X and
A21: not v2 in Z by A14;
    X c= X\/Y by XBOOLE_1:7;
    then consider x2 being object such that
A22: x2 in dom f0 and
A23: v2=f0.x2 by A3,A20,FUNCT_1:def 3;
    reconsider x20=x2 as Nat by A22;
    now
      assume x20 < card X;
      then
A24:  x20 in Segm card X by NAT_1:44;
      card X <= card (X \/Y) by NAT_1:43,XBOOLE_1:7;
      then card X <= len f0 by Th20;
      then f.x20=f0.x20 by A24,AFINSQ_1:53;
      hence contradiction by A5,A10,A21,A23,A24,FUNCT_1:def 3;
    end;
    then
A25: len f <=x20 by A4,AFINSQ_1:54;
    consider k20 being Nat such that
A26: v10=f.k20 and
A27: k20 in card X by A18;
A28: f.k20=f0.k20 by A4,A27,AFINSQ_1:53;
    reconsider nv2 =v2 as Nat by A23;
    k20<len f by A5,A27,AFINSQ_1:86;
    then
A29: k20<x20 by A25,XXREAL_0:2;
    x20<len f0 by A22,AFINSQ_1:86;
    then nv10<nv2 by A26,A23,A29,A28,Def4;
    hence contradiction by A1,A20,A19;
  end;
  f is one-to-one by FUNCT_1:52;
  then
A30: dom f,(f.:(dom f)) are_equipotent by CARD_1:33;
  f.:(dom f)=rng f by RELAT_1:113;
  then
A31: card Z=card (len f)by A10,A30,CARD_1:5;
  then
A32: card Z=card X by A4,AFINSQ_1:54;
A33: now
    per cases by A12;
    case
      Z0 c= X;
      hence Z0=X by A4,A31,CARD_2:102,AFINSQ_1:54;
    end;
    case
      X c=Z0;
      hence Z0=X by A32,CARD_2:102;
    end;
  end;
  f.i=f0.i by A2,A4,AFINSQ_1:53;
  hence thesis by A2,A5,A10,A33,FUNCT_1:def 3;
end;

theorem Th29:
  for X,Y being finite natural-membered set st X <N<
  Y & i< len (Sgm0 X) holds (Sgm0 X).i = (Sgm0 (X \/ Y)).i
proof
  let X,Y be finite natural-membered set;
  assume that
A1: X <N< Y and
A2: i< len (Sgm0 X);
  reconsider h=(Sgm0 (X \/ Y))|(len (Sgm0 X)) as XFinSequence of NAT;
A3: len (Sgm0 X)=card X by Th20;
  then
A4: h.i=(Sgm0 (X \/ Y)).i by A1,A2,Th27;
  Segm card X c= Segm card (X \/ Y) by CARD_1:11,XBOOLE_1:7;
  then
A5: card X <= card (X \/ Y) by NAT_1:39;
  then card X <= len (Sgm0 (X \/ Y)) by Th20;
  then
A6: len (Sgm0 X) <= len (Sgm0 (X \/ Y)) by Th20;
A7: len (Sgm0 (X \/ Y))=card (X \/Y) by Th20;
  then
A8: len h=len (Sgm0 X) by A5,A3,AFINSQ_1:54;
A9: len h=card X by A5,A3,A7,AFINSQ_1:54;
A10: for l,m,k1,k2 being Nat st l < m & m < len h & k1=h.l & k2=h.m holds k1
  < k2
  proof
    let l,m,k1,k2 be Nat;
    assume that
A11: l < m and
A12: m < len h and
A13: k1=h.l and
A14: k2=h.m;
A15: m<len (Sgm0 (X \/ Y)) by A8,A6,A12,XXREAL_0:2;
    l < card X by A9,A11,A12,XXREAL_0:2;
    then
A16: h.l= (Sgm0 (X \/ Y)).l by A1,A3,Th27;
    h.m=(Sgm0 (X \/ Y)).m by A1,A3,A8,A12,Th27;
    hence thesis by A11,A13,A14,A16,A15,Def4;
  end;
  rng h=X by A1,A2,A3,Th27;
  hence thesis by A10,A4,Def4;
end;

theorem Th30:
  for X0,Y0 being finite natural-membered set st X0
<N< Y0 & i < (card Y0) holds rng((Sgm0 (X0\/Y0))/^(card X0))=Y0 & ((Sgm0 (X0\/
  Y0))/^(card X0)).i = (Sgm0 (X0 \/ Y0)).(i+(card X0))
proof
  let X0,Y0 be finite natural-membered set;
  assume that
A1: X0 <N< Y0 and
A2: i < card Y0;
  consider n being Nat such that
A3: Y0 c= Segm n by Th2;
  X0/\Y0=(X0/\(Y0/\NAT)) by A3,XBOOLE_1:1,28
    .= (X0/\Y0/\NAT) by XBOOLE_1:16
    .={} by A1,Th23;
  then
A4: X0 misses Y0;
  set f=(Sgm0 (X0\/Y0))/^(card X0);
  set f0=(Sgm0 (X0\/Y0));
  set Z={ v where v is Element of X0 \/Y0: ex k2 being Nat st v=f.k2 & k2 in
  card Y0};
A5: dom f,(f.:(dom f)) are_equipotent by CARD_1:33;
A6: rng f0=X0 \/Y0 by Def4;
A7: len (Sgm0 (X0\/Y0))=card (X0\/Y0) by Th20;
  then
A8: card X0 <= len (Sgm0 (X0\/Y0)) by NAT_1:43,XBOOLE_1:7;
A9: len f=len f0 -' (card X0) by Def2
    .=len f0 - (card X0) by A8,XREAL_1:233;
A10: (X0\/Y0)\X0=(X0\X0)\/(Y0\X0) by XBOOLE_1:42
    .={} \/ (Y0\X0) by XBOOLE_1:37
    .=Y0 by A4,XBOOLE_1:83;
  then
A11: len f=card Y0 by A7,A9,CARD_2:44,XBOOLE_1:7;
A12: Z c= rng f
  proof
    let y being object;
    assume y in Z;
    then
    ex v0 being Element of X0 \/Y0 st y=v0 & ex k2 being Nat st v0=f.k2
    & k2 in card Y0;
    hence thesis by A11,FUNCT_1:def 3;
  end;
  then reconsider Z0=Z as finite set;
A13: f.:(dom f)=rng f by RELAT_1:113;
A14: rng f c= rng (Sgm0 (X0\/Y0)) by Th9;
A15: rng f c= Z
  proof
    let y be object;
    assume
A16: y in rng f;
    then consider x being object such that
A17: x in dom f and
A18: y=f.x by FUNCT_1:def 3;
    reconsider y0=y as Element of X0\/Y0 by A14,A16,Def4;
    ex k2 being Nat st y0=f.(k2) & k2 in card Y0 by A11,A17,A18;
    hence thesis;
  end;
  then rng f=Z by A12;
  then card Z=card (len f) by A5,A13,CARD_1:5;
  then
A19: card Z=card Y0 by A7,A9,A10,CARD_2:44,XBOOLE_1:7;
  len f0=card (X0 \/Y0) by Th20;
  then
A20: len f0=(card X0)+(card Y0) by A4,CARD_2:40;
A21: X0 \/ Y0 <> {} by A2,CARD_1:27,XBOOLE_1:15;
A22: now
    assume that
A23: not Z c= Y0 and
A24: not Y0 c= Z;
    consider v2 being object such that
A25: v2 in Y0 and
A26: not v2 in Z by A24;
    Y0 c= X0\/Y0 by XBOOLE_1:7;
    then consider x2 being object such that
A27: x2 in dom f0 and
A28: v2=f0.x2 by A6,A25,FUNCT_1:def 3;
    consider v1 being object such that
A29: v1 in Z and
A30: not v1 in Y0 by A23;
    consider v10 being Element of X0 \/Y0 such that
A31: v1=v10 and
A32: ex k2 being Nat st v10=f.k2 & k2 in Segm card Y0 by A29;
A33: v10 in X0 by A21,A30,A31,XBOOLE_0:def 3;
    reconsider nv10 =v10 as Nat;
    reconsider nv2 =v2 as Nat by A28;
    consider k20 being Nat such that
A34: v10=f.k20 and
A35: k20 in Segm card Y0 by A32;
A36: k20+card X0<len f0 by A20,XREAL_1:6,A35,NAT_1:44;
    then
A37: f.k20=f0.(k20+card X0) by Th8;
    reconsider x20=x2 as Nat by A27;
    set nx20=x20 -' (card X0);
A38: v2 in X0 \/Y0 by A6,A27,A28,FUNCT_1:def 3;
A39: now
      assume
A40:  x20 >= card X0;
      then
A41:  x20-'card X0=x20-card X0 by XREAL_1:233;
      x20<card X0 +card Y0 by A20,A27,AFINSQ_1:86;
      then x20-card X0 < card X0 +card Y0 -card X0 by XREAL_1:9;
      then
A42:  nx20<card Y0 by A40,XREAL_1:233;
      then
A43:  nx20 in Segm card Y0 by NAT_1:44;
      nx20+(card X0)<len f0 by A20,A42,XREAL_1:6;
      then f.nx20=f0.x20 by A41,Th8;
      hence contradiction by A26,A28,A38,A43;
    end;
    card X0 <=(card X0)+k20 by NAT_1:12;
    then k20+card X0 >x20 by A39,XXREAL_0:2;
    then nv10>nv2 by A34,A28,A36,A37,Def4;
    hence contradiction by A1,A25,A33;
  end;
A44: now
    per cases by A22;
    case
      Z0 c= Y0;
      hence Z0=Y0 by A19,CARD_2:102;
    end;
    case
      Y0 c=Z0;
      hence Z0=Y0 by A19,CARD_2:102;
    end;
  end;
  i+card X0 < len f0 by A2,A9,A11,XREAL_1:20;
  hence thesis by A15,A12,A44,Th8;
end;

theorem Th31:
  for X,Y being finite natural-membered set st X <N< Y
  & i< len (Sgm0 Y) holds (Sgm0 Y).i = (Sgm0 (X \/ Y)).(i+len (Sgm0 X))
proof
  let X,Y be finite natural-membered set;
  assume that
A1: X <N< Y and
A2: i< len (Sgm0 Y);
  consider m being Nat such that
A3: Y c= Segm m by Th2;
  reconsider h=(Sgm0 (X \/ Y))/^(len (Sgm0 X)) as XFinSequence of NAT;
A4: len (Sgm0 X)=card X by Th20;
A5: len (Sgm0 Y)=card Y by Th20;
  then
A6: h.i=(Sgm0 (X \/ Y)).(i+card X) by A1,A2,A4,Th30;
A7: len (Sgm0 (X \/ Y))=card (X \/Y) by Th20;
  X/\Y=(X/\(Y/\NAT)) by A3,XBOOLE_1:1,28
    .= (X/\Y/\NAT) by XBOOLE_1:16
    .={} by A1,Th23;
  then X misses Y;
  then
A8: card Y +card X=card (X\/Y) by CARD_2:40;
  len h=len ((Sgm0 (X \/ Y))) -' len (Sgm0 X) by Def2
    .= card (X) + card Y -' card X by A8,A7,Th20
    .= card Y by NAT_D:34
    .= len (Sgm0 Y) by Th20;
  then
A9: len h=card Y by Th20;
A10: for l,m,k1,k2 being Nat st l < m & m < len h & k1=h.l & k2=h.m holds k1
  < k2
  proof
    let l,m,k1,k2 be Nat;
    assume that
A11: l < m and
A12: m < len h and
A13: k1=h.l and
A14: k2=h.m;
A15: m+card X <len (Sgm0 (X \/ Y)) by A8,A7,A9,A12,XREAL_1:6;
    set m3=m+card X;
    set l3=l+card X;
A16: l3<m3 by A11,XREAL_1:6;
    l < card Y by A9,A11,A12,XXREAL_0:2;
    then
A17: h.l= (Sgm0 (X \/ Y)).(l+card X) by A1,A4,Th30;
    h.m=(Sgm0 (X \/ Y)).(m+card X) by A1,A4,A9,A12,Th30;
    hence thesis by A13,A14,A17,A15,A16,Def4;
  end;
  rng h=Y by A1,A2,A4,A5,Th30;
  hence thesis by A4,A10,A6,Def4;
end;

theorem Th32:
  for X,Y being finite natural-membered set st Y <> {} & X <N< Y
  holds (Sgm0 Y).0 = (Sgm0 (X \/ Y)).(len (Sgm0 X))
proof
  let X,Y be finite natural-membered set;
  assume that
A1: Y <> {} and
A2: X <N< Y;
  card Y <> 0 by A1;
  then 0<len (Sgm0 Y) by Th20;
  then
  (Sgm0 Y).0 = (Sgm0 (X \/ Y)).((0 qua Element of NAT)+len (Sgm0 X)) by A2,Th31
;
  hence thesis;
end;

theorem Th33: ::from FINSEQ_3:46
  for l,m,n,k being Nat,X being finite natural-membered set st k <
  l & m < len(Sgm0 X) & (Sgm0(X)).m = k & (Sgm0(X)).n = l holds m < n
proof
  let l,m,n,k be Nat,X being finite natural-membered set;
  assume that
A1: k < l and
A2: m < len(Sgm0 X) and
A3: (Sgm0(X)).m = k and
A4: (Sgm0(X)).n = l and
A5: not m < n;
  n < m by A1,A3,A4,A5,XXREAL_0:1;
  hence thesis by A1,A2,A3,A4,Def4;
end;

theorem Th34:
  for X,Y being finite natural-membered set st X <> {} & X <N< Y
  holds (Sgm0 X).0 = (Sgm0 (X \/ Y)).0
proof
  let X,Y be finite natural-membered set;
  assume that
A1: X <> {} and
A2: X <N< Y;
  card X <> 0 by A1;
  then 0<len (Sgm0 X) by Th20;
  hence thesis by A2,Th29;
end;

theorem Th35: ::from FINSEQ_3
  for X,Y being finite natural-membered set holds
X <N< Y iff Sgm0(X \/Y) = Sgm0(X) ^ Sgm0(Y)
proof
  let X,Y be finite natural-membered set;
  set p = Sgm0 X;
  set q = Sgm0 Y;
  set r = Sgm0(X \/ Y);
  thus X <N< Y implies Sgm0(X \/ Y) = Sgm0(X) ^ Sgm0(Y)
  proof
    defpred P[Nat] means $1 in dom p implies r.$1 = p.$1;
    reconsider X1 = X, Y1 = Y as finite set;
    assume
A1: X <N< Y;
    X /\ Y = {}
    proof
      set x =the  Element of X /\ Y;
A2:   X = rng p by Def4;
      assume
A3:   not thesis;
      then x in X by XBOOLE_0:def 4;
      then reconsider m = x as Element of NAT by A2;
A4:   m in Y by A3,XBOOLE_0:def 4;
      m in X by A3,XBOOLE_0:def 4;
      hence thesis by A1,A4;
    end;
    then
A5: X misses Y;
A6: len r = card(X1 \/ Y1) by Th20
      .= card X1 + card Y1 by A5,CARD_2:40
      .= len p + card Y1 by Th20
      .= len p + len q by Th20;
A7: now
      let k;
      assume
A8:   P[k];
      thus P[k+1]
      proof
        set m = r.(k + 1);
        set n = p.(k + 1);
        assume
A9:     k + 1 in dom p;
        then n in rng p by FUNCT_1:def 3;
        then
A10:    n in X by Def4;
        len p <= len r by A6,NAT_1:12;
        then
A11:    Segm(len p) c= Segm(len r) by NAT_1:39;
        then m in rng r by A9,FUNCT_1:def 3;
        then
A12:    m in X \/ Y by Def4;
        assume
A13:    m <> n;
        now
          per cases;
          suppose
A14:        k in dom p;
            set m1 = r.k;
            set n1 = p.k;
            now
              per cases by A13,XXREAL_0:1;
              suppose
A15:            m < n;
                then not m in Y by A1,A10;
                then m in X by A12,XBOOLE_0:def 3;
                then m in rng p by Def4;
                then consider x being object such that
A16:            x in dom p and
A17:            p.x = m by FUNCT_1:def 3;
                reconsider x as Element of NAT by A16;
                x < len p by A16,AFINSQ_1:86;
                then
A18:            x < k + 1 by A15,A17,Th33;
A19:            k < k + 1 by XREAL_1:29;
                k + 1 < len r by A9,A11,AFINSQ_1:86;
                then
A20:            n1 < m by A8,A14,A19,Def4;
                k < len p by A14,AFINSQ_1:86;
                then k < x by A17,A20,Th33;
                hence contradiction by A18,NAT_1:13;
              end;
              suppose
A21:            n < m;
                n in X \/ Y by A10,XBOOLE_0:def 3;
                then n in rng r by Def4;
                then consider x being object such that
A22:            x in dom r and
A23:            r.x = n by FUNCT_1:def 3;
                reconsider x as Element of NAT by A22;
                x < len r by A22,AFINSQ_1:86;
                then
A24:            x < k + 1 by A21,A23,Th33;
A25:            k < k + 1 by XREAL_1:29;
                k + 1 < len p by A9,AFINSQ_1:86;
                then
A26:            m1 < n by A8,A14,A25,Def4;
                k < len r by A11,A14,AFINSQ_1:86;
                then k < x by A23,A26,Th33;
                hence contradiction by A24,NAT_1:13;
              end;
            end;
            hence contradiction;
          end;
          suppose
A27:        not k in dom p;
A28:        k < k + 1 by XREAL_1:29;
            len p <= k by A27,AFINSQ_1:86;
            then len p < k + 1 by A28,XXREAL_0:2;
            hence contradiction by A9,AFINSQ_1:86;
          end;
        end;
        hence contradiction;
      end;
    end;
    0<len p implies X1<>{} by Th20,CARD_1:27;
    then
A29: P[0] by A1,Th34;
A30: for k holds P[k] from NAT_1:sch 2(A29,A7);
    defpred P[Nat] means $1 in dom q implies r.(len p + $1) = q.$1;
A31: now
      let k;
      assume
A32:  P[k];
      thus P[k+1]
      proof
        set n = q.(k + 1);
        set a = len p + (k + 1);
        set m = r.a;
        assume
A33:    k + 1 in dom q;
        then q.(k + 1) in rng q by FUNCT_1:def 3;
        then
A34:    n in Y by Def4;
        k + 1 <len q by A33,AFINSQ_1:86;
        then
A35:    a < len r by A6,XREAL_1:6;
        then
A36:    a in dom r by AFINSQ_1:86;
        then r.a in rng r by FUNCT_1:def 3;
        then
A37:    m in X \/ Y by Def4;
A38:    now
A39:      len p <= len r by A6,NAT_1:12;
          assume m in X;
          then m in rng p by Def4;
          then consider x being object such that
A40:      x in dom p and
A41:      p.x = m by FUNCT_1:def 3;
          reconsider x as Element of NAT by A40;
          x < len p by A40,AFINSQ_1:86;
          then x < len r by A39,XXREAL_0:2;
          then
A42:      x in dom r by AFINSQ_1:86;
          r.x = r.a by A30,A40,A41;
          then x = a by A36,A42,FUNCT_1:def 4;
          then len p + (k + 1) <= len p + (0 qua Element of NAT) by A40,
AFINSQ_1:86;
          hence contradiction by XREAL_1:29;
        end;
        assume
A43:    r.(len p + (k + 1)) <> q.(k + 1);
        now
          per cases;
          suppose
A44:        k in dom q;
            set m1 = r.(len p + k);
            set n1 = q.k;
A45:        k < len q by A44,AFINSQ_1:86;
            now
              per cases by A43,XXREAL_0:1;
              suppose
A46:            m < n;
                m in Y by A37,A38,XBOOLE_0:def 3;
                then m in rng q by Def4;
                then consider x being object such that
A47:            x in dom q and
A48:            q.x = m by FUNCT_1:def 3;
                reconsider x as Element of NAT by A47;
                x < len q by A47,AFINSQ_1:86;
                then
A49:            x < k + 1 by A46,A48,Th33;
                len p + k < len p + k + 1 by XREAL_1:29;
                then
A50:            n1 < m by A32,A35,A44,Def4;
                k < len q by A44,AFINSQ_1:86;
                then k < x by A48,A50,Th33;
                hence contradiction by A49,NAT_1:13;
              end;
              suppose
A51:            n < m;
                n in X \/ Y by A34,XBOOLE_0:def 3;
                then n in rng r by Def4;
                then consider x being object such that
A52:            x in dom r and
A53:            r.x = n by FUNCT_1:def 3;
                reconsider x as Element of NAT by A52;
                x < len r by A52,AFINSQ_1:86;
                then
A54:            x < len p + k + 1 by A51,A53,Th33;
A55:            k < k + 1 by XREAL_1:29;
                k + 1 < len q by A33,AFINSQ_1:86;
                then
A56:            m1 < n by A32,A44,A55,Def4;
                len p + k < len r by A6,A45,XREAL_1:6;
                then len p + k < x by A53,A56,Th33;
                hence contradiction by A54,NAT_1:13;
              end;
            end;
            hence contradiction;
          end;
          suppose
A57:        not k in dom q;
A58:        k < k + 1 by XREAL_1:29;
            len q <= k by A57,AFINSQ_1:86;
            hence contradiction by A33,AFINSQ_1:86,A58,XXREAL_0:2;
          end;
        end;
        hence contradiction;
      end;
    end;
    len q>0 implies Y <>{} by Th20,CARD_1:27;
    then
A59: P[0] by A1,Th32;
    for k holds P[k] from NAT_1:sch 2(A59,A31);
    hence thesis by A6,A30,AFINSQ_1:def 3;
  end;
  assume
A60: Sgm0(X \/ Y) = Sgm0(X) ^ Sgm0(Y);
  let m,n be Nat;
  assume that
A61: m in X and
A62: n in Y;
  n in rng q by A62,Def4;
  then consider y being object such that
A63: y in dom q and
A64: q.y = n by FUNCT_1:def 3;
  reconsider y as Element of NAT by A63;
A65: n = r.(len p + y) by A60,A63,A64,AFINSQ_1:def 3;
  y < len q by A63,AFINSQ_1:86;
  then len p + y < len p + len q by XREAL_1:6;
  then
A66: len p + y < len r by A60,AFINSQ_1:17;
A67: len p<=len p+y by NAT_1:12;
  m in rng(Sgm0 X) by A61,Def4;
  then consider x being object such that
A68: x in dom p and
A69: p.x = m by FUNCT_1:def 3;
  reconsider x as Element of NAT by A68;
  x < len p by A68,AFINSQ_1:86;
  then
A70: x < len p + y by A67,XXREAL_0:2;
  m = r.x by A60,A68,A69,AFINSQ_1:def 3;
  hence thesis by A65,A70,A66,Def4;
end;

definition
  let f be XFinSequence;
  let B be set;
  ::Following is a subsequence selected from f by B.
  func SubXFinS (f,B) -> XFinSequence equals
  f*Sgm0(B /\ Segm len f);
  coherence
  proof
    B/\ Segm len f c= dom f by XBOOLE_1:17;
    then rng Sgm0(B/\ Segm len f) c= dom f by Def4;
    hence thesis by AFINSQ_1:10;
  end;
end;

theorem Th36:
  for B being set holds len SubXFinS (p,B)=
   card (B/\ Segm(len p)) &
  for i st i < len SubXFinS (p,B) holds SubXFinS
  (p,B).i=p.((Sgm0 (B/\ Segm(len p))).i)
proof
  let  B be set;
  B/\ Segm len p c= dom p by XBOOLE_1:17;
  then rng Sgm0(B/\ Segm len p) c= dom p by Def4;
  then dom SubXFinS (p,B) = len Sgm0(B/\ Segm len p) by RELAT_1:27
    .= card(B/\ Segm len p) by Th20;
  hence len SubXFinS (p,B)=card (B/\ Segm len p);
  let i;
  assume i < len SubXFinS (p,B);
  hence thesis by FUNCT_1:12,AFINSQ_1:86;
end;

registration
  let D be set;
  let f be XFinSequence of D, B be set;
  cluster SubXFinS(f,B) -> D-valued;
  coherence;
end;

registration
  let p;
  cluster SubXFinS (p,{}) -> empty;
  coherence
  proof
    len (SubXFinS (p,{})) =card {} by Th36;
    hence thesis;
  end;
end;

registration
  let B be set;
  cluster SubXFinS ({},B) -> empty;
  coherence;
end;

 :: AFINSQ_2:48 => AFINSQ_2:83

reserve D for non empty set,
  F,G for XFinSequence of D,
  b for BinOp of D,
  d,d1,d2 for Element of D;

scheme
  Sch5{D()->set, P[set]}: for F be XFinSequence of D() holds P[F]
provided
A1: P[<%>D()] and
A2: for F be XFinSequence of D(),d be Element of D() st P[F] holds P[F^<%d%>]
proof
  defpred R[set] means for F be XFinSequence of D() st len F = $1 holds P[F];
A3: for n st R[n] holds R[n+1]
  proof
    let n such that
A4: for F be XFinSequence of D() st len F=n holds P[F];
    let F be XFinSequence of D();
    assume
A5: len F = n + 1;
    then F <>{};
    then consider G be XFinSequence, d be object such that
A6: F = G^<%d%> by AFINSQ_1:40;
    reconsider G,dd=<%d%> as XFinSequence of D() by A6,AFINSQ_1:31;
    A7:rng dd c= D() & rng dd = {d} & d in {d}
      by AFINSQ_1:33,TARSKI:def 1;
     len dd = 1 by AFINSQ_1:34;
    then len F = len G + 1 by A6,AFINSQ_1:17;
    hence thesis by A2,A4,A5,A6,A7;
  end;
  let F be XFinSequence of D();
A8: len F=len F;
  card X = {} implies X = {};
  then
A9: R[0] by A1;
  for n holds R[n] from NAT_1:sch 2(A9,A3);
  hence thesis by A8;
end;

definition
  let D;
  let F be XFinSequence;
  assume A1:F is D-valued;
  let b;
  assume A2: b is having_a_unity or len F >= 1;
  func b "**" F -> Element of D means :Def8: :: STIRL2_1:def 3
  it = the_unity_wrt b if b is having_a_unity & len F = 0
    otherwise ex f be sequence of D st f.0 = F.0 &
   (for n st n+1 < len F holds f.(n + 1) = b.(f.n,F.(n + 1))) &
it = f.(len F-1);
  existence
  proof
    now
      per cases;
      suppose
        len F = 0;
        hence thesis by A2;
      end;
      suppose
A3:     len F <> 0;
        defpred P[Nat] means for F st len F = $1 & len F <> 0 ex d
be Element of D,f be sequence of D st f.0 = F.0 & (for n st n+1 < len F
        holds f.(n + 1) = b.(f.n,F.(n + 1))) & d = f.(len F-1);
A4:     for k st P[k] holds P[k + 1]
        proof
          let k such that
A5:       P[k];
          let F such that
A6:       len F = k + 1 and
          len F <> 0;
          set G = F|k;
A7:       k < k+1 by NAT_1:13;
          then
A8:       len G = k by A6,AFINSQ_1:11;
          now
            per cases;
            suppose
A9:           len G = 0;
              then 0 in dom F by A6,A8,CARD_1:49,TARSKI:def 1;
              then
A10:           F.0 in rng F by FUNCT_1:def 3;
              reconsider f = NAT --> F.0 as sequence of D by A10,
FUNCOP_1:45;
              take d = f.0,f;
              thus f.0 = F.0 by FUNCOP_1:7;
              thus for n st n+1 < len F holds f.(n + 1) = b.(f.n,F.(n + 1)) by
A6,A8,A9,NAT_1:14;
              k<k+1 by NAT_1:13;
              hence d = f.(len F-1) by A6,A9,AFINSQ_1:11;
            end;
            suppose
A11:          len G <> 0;
              k < len F by A6,NAT_1:13;
              then k in dom F by AFINSQ_1:86;
              then
A12:          F.k in rng F by FUNCT_1:def 3;
              reconsider d1 = F.k as Element of D by A12;
A13:          0 in len G by A11,AFINSQ_1:86;
              consider d be Element of D,f be sequence of D such that
A14:          f.0 = G.0 and
A15:          for n st n+1<len G holds f.(n + 1)=b.(f.n,G.(n + 1)) and
A16:          d = f.(len G-1) by A5,A6,A7,A11,AFINSQ_1:11;
              deffunc F(Element of NAT) = f.$1;
              reconsider K=k as Element of NAT by ORDINAL1:def 12;
              consider h be sequence of D such that
A17:          h.K = b.(d,d1) and
A18:          for n be Element of NAT st n <> K holds h.n = F(n) from
              FUNCT_2:sch 6;
              take a = h.k, h;
              h.0=f.0 by A8,A11,A18;
              hence h.0 =F.0 by A14,A13,FUNCT_1:47;
              thus for n st n+1 < len F holds h.(n + 1) = b.(h.n,F.(n + 1))
              proof
                let n;
                assume n+1 < len F;
                then
A19:            n+1 <= len G by A6,A8,NAT_1:13;
                now
                  per cases by A19,XXREAL_0:1;
                  suppose
A20:                n+1 = len G;
                    then
A21:                n<k by A8,NAT_1:13;
                    n+1=k & n in NAT by A6,A7,A20,AFINSQ_1:11,ORDINAL1:def 12;
                    hence thesis by A16,A17,A18,A20,A21;
                  end;
                  suppose
A22:                n+1 < len G; then
A23:                G.(n+1)=F.(n+1) by FUNCT_1:47,AFINSQ_1:86;
                    n<=n+1 & n in NAT by NAT_1:11,ORDINAL1:def 12;
                    then
A24:                f.n=h.n  by A8,A18,A22;

                    f.(n+1)=h.(n+1) by A8,A18,A22;
                    hence thesis by A15,A22,A23,A24;
                  end;
                end;
                hence thesis;
              end;
              thus a = h.(len F-1) by A6;
            end;
          end;
          hence thesis;
        end;
A25:    P[0];
        for k holds P[k] from NAT_1:sch 2(A25,A4);
        hence thesis by A1,A3;
      end;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let d1,d2 be Element of D;
    thus b is having_a_unity & len F=0 & d1 = the_unity_wrt b & d2 =
    the_unity_wrt b implies d1 = d2;
A26: (len F-1) +1 =len F;
    assume not b is having_a_unity or len F <> 0;
    then 0< len F by A2;
    then
A27: len F-1 is Element of NAT by NAT_1:20;
    given f1 be sequence of D such that
A28: f1.0 = F.0 and
A29: for n st n+1<len F holds f1.(n + 1) = b.(f1.n,F.(n + 1)) and
A30: d1 = f1.(len F-1);
    given f2 be sequence of D such that
A31: f2.0 = F.0 and
A32: for n st n+1<len F holds f2.(n + 1) = b.(f2.n,F.(n + 1)) and
A33: d2 = f2.(len F-1);
    defpred P[Nat] means $1+1 <= len F implies f1.$1 = f2.$1;
A34: P[n] implies P[n + 1]
    proof
      assume A35:  P[n];
      assume (n+1)+1 <= len F;
      then
A36:  n+1<len F by NAT_1:13;
      then f2.(n+1)=b.(f2.n,F.(n+1)) by A32;
      hence thesis by A29,A35,A36;
    end;
A37: P[0] by A28,A31;
    for n holds P[n] from NAT_1:sch 2(A37,A34);
    hence thesis by A30,A33,A26,A27;
  end;
  consistency;
end;

theorem Th37:
  b "**" <%d%> = d
proof
  len<%d%> = 1 by AFINSQ_1:33;
  then ex f be sequence of D st f.0=<%d%>.0& (for n st n+1 < len <%d%>
  holds f.(n+1) = b.(f.n,<%d%>.(n+1)))& b "**" <%d%>=f.(1-1) by Def8;
  hence thesis;
end;

reconsider zz=0 as Nat;

theorem  Th38:
  b "**" <%d1,d2%> = b.(d1,d2)
proof
  len <%d1,d2%>=2 by AFINSQ_1:38;
  then consider f be sequence of D such that
A1: f.0 = <%d1,d2%>.0 and
A2: for n st n+1 < 2 holds f.(n + 1) = b.(f.n,<%d1,d2%>.(n + 1)) and
A3: b "**" <%d1,d2%> = f.(2-1) by Def8;
  f.(zz+1)=b.(f.zz,<%d1,d2%>.(zz+1)) by A2;
  hence thesis by A1,A3;
end;

theorem  Th39:
  b "**" <%d,d1,d2%> = b.(b.(d,d1),d2)
proof
  set F=<%d,d1,d2%>;
  len F=3 by AFINSQ_1:39;
  then consider f be sequence of D such that
A1: f.0 = F.0 and
A2: for n st n+1 < 3 holds f.(n + 1) = b.(f.n,F.(n + 1)) and
A3: b "**" F = f.(3-1) by Def8;
A4: f.(1+1)=b.(f.1,F.(1+1)) by A2;
  f.(zz+1)=b.(f.zz,F.(zz+1)) by A2;
  hence thesis by A1,A3,A4;
end;

theorem Th40:  :: STIRL2_1:45
  b is having_a_unity or len F > 0 implies b "**" (F ^ <% d %>) =
  b.(b "**" F,d)
proof
  assume
A1: b is having_a_unity or len F > 0;
  now
    per cases;
    suppose
A2:   len F<zz+1;
      then
A3:     F={} by NAT_1:13;
A4:   b "**" (F ^<% d %>)=d by Th37,A3;
      len F=0 by A2,NAT_1:13;
      then b "**" F = the_unity_wrt b by A1,Def8;
      hence thesis by A1,A2,A4,NAT_1:13,SETWISEO:15;
    end;
    suppose
A5:   len F>=1;
      set G = F ^ <% d %>;
      reconsider lenF1=len F-1 as Element of NAT by A5,NAT_1:21;
A6:   G.(len F)=d by AFINSQ_1:36;
A7:   len G=len F+len <%d%> by AFINSQ_1:17
        .=len F+1 by AFINSQ_1:33;
      then 1 <= len G by NAT_1:12;
      then consider f1 be sequence of D such that
A8:   f1.0 = G.0 and
A9:   for n st n+1 < len G holds f1.(n+1)=b.(f1.n,G.(n+1)) and
A10:   b "**" G = f1.(len G-1) by Def8;
      consider f be sequence of D such that
A11:  f.0 = F.0 and
A12:  for n st n+1 < len F holds f.(n+1)=b.(f.n,F.(n+1)) and
A13:  b "**" F = f.(len F-1) by A5,Def8;
      defpred P[Nat] means $1+1 < len G implies f.$1 = f1.$1;
A14:   P[n] implies P[n + 1]
      proof
       assume
A15:    P[n];
        set n1=n+1;
        assume
A16:    n1+1<len G; then
A17:    f1.n1=b.(f1.n,G.(n+1)) by A9,NAT_1:13;
A18:    (n1+1)+(-1)<(len F+1)+(-1) by A7,A16,XREAL_1:8;
        then
A19:    n1 in len F by AFINSQ_1:86;
        f.n1=b.(f.n,F.n1) by A12,A18;
        hence thesis by A15,A16,A17,A19,AFINSQ_1:def 3,NAT_1:13;
      end;
      0 in len F by A5,AFINSQ_1:86;
      then
A20:  P[0] by A11,A8,AFINSQ_1:def 3;
A21:  for n holds P[n] from NAT_1:sch 2(A20,A14);
A22:  lenF1+1<len G by A7,NAT_1:13;
      then b "**" G = b.(f1.(lenF1),G.(lenF1+1)) by A7,A9,A10;
      hence thesis by A13,A21,A22,A6;
    end;
  end;
  hence thesis;
end;

::$CT

theorem Th41: :: STIRL2_1:47
  b is associative & (b is having_a_unity or len F >= 1 & len G >= 1)
  implies b "**" (F ^ G) = b.(b "**" F,b "**" G)
proof
  defpred P[XFinSequence of D] means for F,b st b is associative & (b is
  having_a_unity or len F >= 1 & len $1 >= 1) holds b "**" (F^$1)=b.(b "**" F,b
  "**" $1);
A1: for G,d st P[G] holds P[G ^ <%d%>]
  proof
    let G,d such that
A2: P[G];
    let F,b such that
A3: b is associative and
A4: b is having_a_unity or len F >= 1 & len(G ^ <% d %>) >= 1;
    now
      per cases;
      suppose
A5:     len G<>0;
        then
        b is having_a_unity or len F>=1&len (F^G)=len F+len G & len F+len
        G >len F+zz by A4,AFINSQ_1:17,XREAL_1:8;
        then b.(b "**" (F ^ G),d)=b "**" ((F ^ G)^<%d%>) by Th40;
        then
A6:     b "**" (F ^ (G ^ <% d %>)) = b.(b "**" (F ^ G),d) by AFINSQ_1:27;
        len G>=1 by A5,NAT_1:14;
        then b "**" (F ^ (G ^ <% d %>))=b.(b.(b "**" F,b "**" G),d) by A2,A3,A4
,A6
          .= b.(b "**" F,b.(b "**" G,d)) by A3
          .= b.(b "**" F,b "**" (G ^ <% d %>)) by A5,Th40;
        hence thesis;
      end;
      suppose
        len G=0;
        then
A7:     G = {};
        hence b "**" (F ^(G ^ <% d %>))
           = b "**"(F^({}^<% d %>))
          .= b "**"(F^<% d %>)
          .= b.(b "**" F,d) by A4,Th40
          .= b.(b "**" F,b "**" ({}^<%d%>)) by Th37
          .= b.(b "**" F,b "**" (G ^ <% d %>)) by A7;
      end;
    end;
    hence thesis;
  end;
A8: P[<%>D]
  proof
    let F,b;
    assume that
    b is associative and
A9: b is having_a_unity or len F >= 1 & len <%>D >= 1;
    thus b "**" (F ^ <%>D) = b "**" (F^{})
      .= b.(b "**" F,the_unity_wrt b) by A9,SETWISEO:15
      .= b.(b "**" F,b "**" <%>D) by A9,Def8,CARD_1:27;
  end;
  for G holds P[G] from Sch5(A8,A1);
  hence thesis;
end;

theorem Th42: :: CARD_FIN:42
  n in dom F & (b is having_a_unity or n <> 0 ) implies
   b.(b "**" F|n, F.n) = b "**" F|(n+1)
proof
assume that
A1: n in dom F and
A2: b is having_a_unity or n <> 0;
  len F>n by A1,AFINSQ_1:86;
  then
A3: len (F|n)=n by AFINSQ_1:54;
  defpred P[Nat] means $1 in dom F & (b is having_a_unity or len (F
  |$1) >= 1) implies b.(b "**" F|$1, F.$1) = b "**" F|($1+1);
A4: for k st P[k] holds P[k+1]
  proof
    let k such that P[k];
    set k1=k+1;
    set Fk1=F|k1;
    set Fk2=F|(k1+1);
    assume that
A5: k1 in dom F and
A6: b is having_a_unity or len Fk1 >= 1;
    0 < len F by A5;
    then
A7: 0 in dom F by AFINSQ_1:86;
    0 in Segm k1 by NAT_1:44;
    then 0 in dom F/\k1 by A7,XBOOLE_0:def 4;
    then 0 in dom Fk1 by RELAT_1:61;
    then
A8: Fk1.0=F.0 by FUNCT_1:47;
A9: k<k1 by NAT_1:13;
    k1<k1+1 by NAT_1:13;
    then k1 in Segm(k1+1) by NAT_1:44;
    then
A10: k1 in dom F/\(k1+1) by A5,XBOOLE_0:def 4;
A12: k1 < len F by A5,AFINSQ_1:86;
    then
A13: len Fk1=k1 by AFINSQ_1:54;
    then consider f1 be sequence of D such that
A14: f1.0 = Fk1.0 and
A15: for n st n+1 < len Fk1 holds f1.(n+1) = b.(f1.n,Fk1.(n + 1)) and
A16: b "**" Fk1= f1.(k1-1) by A6,Def8;
    k1+1 <=dom F by A12,NAT_1:13;
    then
A17: len Fk2=k1+1 by AFINSQ_1:54;
    then b is having_a_unity or len Fk2 >= 1 by A6,A13,NAT_1:13;
    then consider f2 be sequence of D such that
A18: f2.0 = Fk2.0 and
A19: for n st n+1 < len Fk2 holds f2.(n+1) = b.(f2.n,Fk2.(n+1)) and
A20: b "**" Fk2= f2.((k1+1)-1) by A17,Def8;
    defpred R[Nat] means $1 < k1 implies f1.$1=f2.$1;
A21: for m  st R[m] holds R[m+1]
    proof
      let m such that
A22:  R[m];
      set m1=m+1;
      assume
A23:  m1 < k1;
      k1< len F by A5,AFINSQ_1:86;
      then m1 < len F by A23,XXREAL_0:2;
      then
A24:  m1 in dom F by AFINSQ_1:86;
      m1 <k1+1 by A23,NAT_1:13;
      then m1 in Segm(k1+1) by NAT_1:44;
      then m1 in dom F/\Segm(k1+1) by A24,XBOOLE_0:def 4;
      then m1 in dom Fk2 by RELAT_1:61;
      then
A25:  Fk2.m1 = F.m1 by FUNCT_1:47;
      m1 in Segm k1 by A23,NAT_1:44;
      then m1 in dom F/\Segm k1 by A24,XBOOLE_0:def 4;
      then m1 in dom Fk1 by RELAT_1:61;
      then
A26:  Fk1.m1 = F.m1 by FUNCT_1:47;
      m1 < len Fk2 by A17,A23,NAT_1:13;
      then f2.m1 = b.(f1.m,Fk1.m1) by A19,A22,A23,A26,A25,NAT_1:13;
      hence thesis by A13,A15,A23;
    end;
    0 in Segm(k1+1) by NAT_1:44;
    then 0 in dom F/\(k1+1) by A7,XBOOLE_0:def 4;
    then 0 in dom Fk2 by RELAT_1:61;
    then
A27: R[0] by A14,A18,A8,FUNCT_1:47;
    for m holds R[m] from NAT_1:sch 2(A27,A21);
    then
A28: dom F/\(k1+1)=dom Fk2 & f1.k=f2.k by A9,RELAT_1:61;
    k1<k1+1 by NAT_1:13;
    then f2.k1 = b.(f2.k,Fk2.k1) by A17,A19;
    hence thesis by A16,A20,A10,A28,FUNCT_1:47;
  end;
A29: P[0]
  proof
    assume that
A30: 0 in dom F and
A31: b is having_a_unity or len (F|(0 qua Ordinal)) >= 1;
A32: F.0 in rng F by A30,FUNCT_1:def 3;
    len F>0 by A30;
    then
A33: len (F|1)=1 by AFINSQ_1:54,NAT_1:14;
    then
A34: (F|1)=<%(F|1).0%> by AFINSQ_1:34;
    0 in Segm 1 by NAT_1:44;
    then
A35: F.0=(F|1).0 by A33,FUNCT_1:47;
    len (F|(0 qua Ordinal))=0;
    then b "**" F|(0 qua Ordinal)=the_unity_wrt b by A31,Def8;
    then b.(b "**" F|(0 qua Ordinal), F.0)=F.0 by A31,A32,SETWISEO:15;
    hence thesis by A32,A34,A35,Th37;
  end;
  for k holds P[k] from NAT_1:sch 2(A29,A4);
  hence thesis by A1,A2,A3,NAT_1:14;
end;

theorem Th43: :: CARD_FIN:47
b is having_a_unity or len F >= 1 implies b "**" F = b "**" (XFS2FS F)
proof
assume
A1: b is having_a_unity or len F >= 1;
  per cases by A1;
  suppose
A2: len F >=1;
    set FS=XFS2FS F;
    len F=len FS by AFINSQ_1:def 9;
    then consider f be sequence of D such that
A3: f.1 = FS.1 and
A4: for n be Nat st 0<>n & n<len F holds
f.(n+1) = b.(f.n,FS.(n+1)) and
A5: b "**" FS = f.(len F) by A2,FINSOP_1:def 1;
    consider xf be sequence of D such that
A6: xf.0 = F.0 and
A7: for n
st n+1 < len F holds xf.(n + 1) = b.(xf.n,F.(n + 1)) and
A8: b "**" F = xf.(len F-1) by A2,Def8;
    defpred P[Nat] means $1 < len F implies xf.$1=f.($1+1);
A9: for n st P[n] holds P[n+1]
    proof
      let n such that
A10:  P[n];
      set n1=n+1;
      set n2=n1+1;
      assume
A11:  n1 < len F;
      then zz+1<=n2 & n2 <=len F by NAT_1:13;
      then
A12:  F.(n2-'1)=FS.n2 by AFINSQ_1:def 9;
      xf.n1 = b.(xf.n,F.n1) & f.(n1+1) = b.(f.n1,FS.(n1+1)) by A7,A4,A11;
      hence thesis by A10,A11,A12,NAT_1:13,NAT_D:34;
    end;
    reconsider L1=len F-1 as Element of NAT by A2,NAT_1:21;
A13: L1<L1+1 by NAT_1:13;
A14: P[0]
    proof
      assume 0 <len F;
      then zz+1<=len F by NAT_1:13;
      then F.(1-'1)=FS.1 by AFINSQ_1:def 9;
      hence thesis by A6,A3,XREAL_1:232;
    end;
    for n holds P[n] from NAT_1:sch 2(A14,A9);
    hence thesis by A8,A5,A13;
  end;
  suppose
A15: b is having_a_unity & len F<1;
    then len F<=zz+1;
    then
A16: len F=0 by A15,NAT_1:8;
    then len F=len (XFS2FS F) & b "**" F=the_unity_wrt b
by A15,Def8,AFINSQ_1:def 9;
    hence thesis by A15,A16,FINSOP_1:def 1;
  end;
end;

theorem Th44: ::CARD_FIN:43
  for P be Permutation of dom F st b is commutative associative &
    (b is having_a_unity or len F >= 1) &
    G = F * P holds b "**" F = b "**" G
proof
  let P be Permutation of dom F such that
A1: b is commutative associative and
A2: b is having_a_unity or len F >= 1 and
A3: G = F * P;
  set xF=XFS2FS F;
A4: b is having_a_unity or len xF >= 1 by A2,AFINSQ_1:def 9;
  set xG=XFS2FS G;
  defpred p[object,object] means for n st $1=n holds $2=P.(n-1)+1;
  dom F=len F;
  then reconsider d=dom F as Element of NAT;
A6: for x being object st x in Seg d ex y being object st y in Seg d & p[x,y]
  proof
    let x be object such that
A7: x in Seg d;
    reconsider x9=x as Element of NAT by A7;
    1+zz<=x9 by A7,FINSEQ_1:1;
    then reconsider x91=x9-1 as Element of NAT by NAT_1:21;
A8: x91+1<= d by A7,FINSEQ_1:1;
    then x91 <d by NAT_1:13;
    then
A9: x91 in Segm d by NAT_1:44;
    take (P.x91)+1;
  dom F=dom P by A8,FUNCT_2:def 1;
    then P.x91 in rng P by A9,FUNCT_1:def 3;
    then P.x91 < d by AFINSQ_1:86;
    then zz+1<=(P.x91)+1 & (P.x91)+1 <=d by NAT_1:13;
    hence thesis by FINSEQ_1:1;
  end;
  consider P9 be Function of Seg d,Seg d such that
A10: for x being object st x in Seg d holds p[x,P9.x] from FUNCT_2:sch 1(A6);
  now
    let x1,x2 be object such that
A11: x1 in dom P9 and
A12: x2 in dom P9 and
A13: P9.x1=P9.x2;
    dom P9=Seg d by FUNCT_2:52;
    then reconsider X1=x1,X2=x2 as Element of NAT by A11,A12;
    1+zz<=X1 & 1+zz<=X2 by A11,A12,FINSEQ_1:1;
    then reconsider X19=X1-1,X29=X2-1 as Element of NAT by NAT_1:21;
A14: X19<X19+1 & X1 <=d by A11,FINSEQ_1:1,NAT_1:13;
    then
A15: dom P=dom F by FUNCT_2:def 1;
    X29<X29+1 & X2<=d by A12,FINSEQ_1:1,NAT_1:13;
    then X29<d by XXREAL_0:2;
    then
A16: X29 in dom P by A15,AFINSQ_1:86;
    X19<d by A14,XXREAL_0:2;
    then
A17: X19 in dom P by A15,AFINSQ_1:86;
    P9.X1=P.X19+1 by A10,A11;
    then (P.X19+1)-1=(P.X29+1)-1 by A10,A12,A13;
    then X1-1+1=X2-1+1 by A17,A16,FUNCT_1:def 4;
    hence x1=x2;
  end;
  then
A18: P9 is one-to-one;
  card Seg d=card Seg d;
  then
A19: P9 is one-to-one onto by A18,Lm1;
  len xF =len F by AFINSQ_1:def 9;
  then dom xF= Seg len F by FINSEQ_1:def 3;
  then reconsider P9 as Permutation of dom xF by A19;
A20: dom P9= Seg d & dom xG=Seg len xG by FINSEQ_1:def 3,FUNCT_2:52;
  rng P9 c= dom xF;
  then
A21: dom (xF* P9)=dom P9 by RELAT_1:27;
  rng P c= dom F;
  then dom (F*P)=dom P by RELAT_1:27;
  then
A22: dom G= dom F by A3,FUNCT_2:52;
A24: for x9 be object st x9 in dom xG holds xG.x9 = (xF*P9).x9
  proof
    let x9 be object such that
A25: x9 in dom xG;
    reconsider x=x9 as Element of NAT by A25;
A26: dom xG=Seg len xG by FINSEQ_1:def 3;
    then
A27: 1<=x by A25,FINSEQ_1:1;
    then
A28: x-'1=x-1 by XREAL_1:233;
    0<x by A25,A26,FINSEQ_1:1;
    then reconsider x1=x-1 as Element of NAT by NAT_1:20;
A29: dom xF=Seg len xF by FINSEQ_1:def 3;
A30: len xG=len G by AFINSQ_1:def 9;
    then
A31: P.(x-1)+1=P9.x & x in dom P9 by A10,A22,A25,A26,FUNCT_2:52;
    then
A32: P.(x-1)+1 in rng P9 by FUNCT_1:def 3;
A33: x<=len F by A22,A25,A26,A30,FINSEQ_1:1;
    then
A34: xG.x=(F*P).(x-'1) by A3,A22,A27,AFINSQ_1:def 9;
    len xF=len F by AFINSQ_1:def 9;
    then
A35: P.(x-1)+1<=len F by A32,A29,FINSEQ_1:1;
    x1<x1+1 & x-'1=x1 by A27,NAT_1:13,XREAL_1:233;
    then x-'1 < len G by A22,A33,XXREAL_0:2;
    then x-'1 in dom G by AFINSQ_1:86;
    then
A36: P.(x-'1)+1-'1=P.(x-'1) & (F*P).(x-'1)=F.(P.(x-'1)) by A3,FUNCT_1:12
,NAT_D:34;
    1<=P.(x-1)+1 by A32,A29,FINSEQ_1:1;
    then (F*P).(x-'1)=xF.((P.(x-1)+1)) by A35,A28,A36,AFINSQ_1:def 9;
    hence thesis by A31,A34,FUNCT_1:13;
  end;
  len xG=len F by A22,AFINSQ_1:def 9;
  then xG=xF* P9 by A24,A21,A20;
  then
A37: b "**"xG=b"**"xF by A1,A4,FINSOP_1:7;
  b "**"xG=b "**" G by A2,A22,Th43;
  hence thesis by A2,A37,Th43;
end;

theorem :: CARD_FIN:62
  for bFG be XFinSequence of D st b is commutative associative &
         (b is having_a_unity or len F >= 1) &
         len F=len G & len F=len bFG &
         (for n st n in dom bFG holds bFG.n=b.(F.n,G.n))
  holds b "**" F^G = b "**" bFG
proof
  let bFG be XFinSequence of D such that
A1: b is commutative associative and
A2: b is having_a_unity or len F >= 1 and
A3: len F=len G and
A4: len F=len bFG and
A5: for n st n in dom bFG holds bFG.n=b.(F.n,G.n);
  set xG=XFS2FS G;
  set xF=XFS2FS F;
A6: b "**" F=b "**" xF & b "**" G=b "**" xG by A2,A3,Th43;
  set xb=XFS2FS bFG;
A7: len xb=len bFG by AFINSQ_1:def 9;
A8: for k be Nat st k in dom xb holds xb.k = b.(xF.k,xG.k)
  proof
    let k be Nat such that
A9: k in dom xb;
    k in Seg len xb by A9,FINSEQ_1:def 3;
    then k>=1 by FINSEQ_1:1;
    then reconsider k1=k-1 as Element of NAT by NAT_1:21;
A10: k in Seg len xb by A9,FINSEQ_1:def 3;
    then
A11: 1<=k by FINSEQ_1:1;
    then
A12: k1=k-'1 by XREAL_1:233;
    k in Seg len xb by A9,FINSEQ_1:def 3;
    then k1<k1+1 & k<=len xb by FINSEQ_1:1,NAT_1:13;
    then k1<len xb by XXREAL_0:2;
    then k1 in dom bFG by A7,AFINSQ_1:86;
    then
A13: bFG.k1=b.(F.k1,G.k1) by A5;
A14: k<= len bFG by A7,A10,FINSEQ_1:1;
    then bFG.(k-'1)=xb.k & F.(k-'1)=xF.k by A4,A11,AFINSQ_1:def 9;
    hence thesis by A3,A4,A11,A14,A13,A12,AFINSQ_1:def 9;
  end;
  len xF=len F & len G=len xG by AFINSQ_1:def 9;
  then b "**" xb=b.(b "**" xF,b "**" xG) by A1,A2,A3,A4,A7,A8,FINSOP_1:9;
  then b "**" bFG = b.(b "**" F,b "**" G) by A2,A4,A6,Th43;
  hence thesis by A1,A2,A3,Th41;
end;

theorem Th46:
  for D1,D2 be non empty set
    for b1 be BinOp of D1,b2 be BinOp of D2 st
        len F >= 1 &
        D c= D1 /\ D2 &
        for x,y st x in D & y in D holds b1.(x,y)=b2.(x,y) & b1.(x,y) in D
    holds b1 "**" F = b2 "**" F
proof
  let D1,D2 be non empty set;
  let b1 be BinOp of D1,b2 be BinOp of D2 such that
A1:        len F >= 1 and
A2:        D c= D1 /\ D2 and
A3:  for x,y st x in D & y in D holds b1.(x,y) = b2.(x,y) & b1.(x,y) in D;
    D1/\D2 c= D1 & D1/\D2 c= D2 by XBOOLE_1:17;
then A4:D c= D1 & D c= D2 by A2;
rng F c= D1 & rng F c= D2 by A4;
then A5:F is D1-valued & F is D2-valued by RELAT_1:def 19;
then consider F1 be sequence of D1 such that
A6:      F1.0 = F.0 and
A7:      for n st n+1 < len F holds F1.(n + 1) = b1.(F1.n,F.(n + 1)) and
A8:      b1 "**" F = F1.(len F-1) by A1,Def8;
   consider F2 be sequence of D2 such that
A9:      F2.0 = F.0 and
A10:      for n st n+1 < len F holds F2.(n + 1) = b2.(F2.n,F.(n + 1)) and
A11:      b2 "**" F = F2.(len F-1) by A1,Def8,A5;

defpred P[Nat] means $1 < len F implies F1.$1 = F2.$1 & F1.$1 in D;
 0 in dom F by A1,AFINSQ_1:86;
then F.0 in rng F by FUNCT_1:def 3;
then
A12:P[0] by A6,A9;
A13: P[n] implies P[n+1]
proof
   assume A14:P[n];
   assume A15:n+1 < len F;
   then n+1 in dom F & n < len F by NAT_1:13,AFINSQ_1:86;
   then A16:F.(n+1) in rng F & n in dom F by FUNCT_1:def 3,AFINSQ_1:86;
    A17:F1.(n + 1) = b1.(F1.n,F.(n + 1)) by A7,A15;
   then F1.(n + 1)= b2.(F2.n,F.(n + 1)) by A3,A16,A14,AFINSQ_1:86
    .=F2.(n+1) by A10,A15;
   hence thesis by A16,A14,A17,A3,AFINSQ_1:86;
end;
reconsider l1=len F-1 as Element of NAT by A1,NAT_1:21;
A18:l1 < l1+1 by NAT_1:13;
P[n] from NAT_1:sch 2(A12,A13);
hence thesis by A8,A11,A18;
end;

reserve F for XFinSequence,
        rF,rF1,rF2 for real-valued XFinSequence,
        r for Real,
        cF,cF1,cF2 for complex-valued XFinSequence,
        c,c1,c2 for Complex;

Lm2:cF is COMPLEX -valued
proof
rng cF c= COMPLEX by VALUED_0:def 1;
hence thesis by RELAT_1:def 19;
end;

Lm3:rF is REAL -valued
proof
rng rF c= REAL by VALUED_0:def 3;
hence thesis by RELAT_1:def 19;
end;

definition
  let F;
  func Sum F ->Element of COMPLEX equals
    addcomplex "**" F;
  coherence;
end;

registration
  let f be empty complex-valued XFinSequence;
  cluster Sum f -> zero;
  coherence
  proof
    f is COMPLEX-valued & len f = 0 by Lm2;
    hence thesis by Def8,BINOP_2:1;
  end;
end;

theorem Th47:
   F is real-valued implies Sum F = addreal "**" F
proof
    assume A1:F is real-valued;
then  rng F c= REAL by VALUED_0:def 3;
then A2:F is REAL-valued by RELAT_1:def 19;
  rng F c= COMPLEX by A1,MEMBERED:1;
  then A3:F is COMPLEX-valued by RELAT_1:def 19;
  per cases by NAT_1:14;
    suppose A4:len F=0;
      hence addreal "**" F = 0 by Def8,A2,BINOP_2:2
                          .= Sum F by Def8,A3,A4,BINOP_2:1;
    end;
    suppose A5:len F>=1;
        A6: REAL = REAL /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
  now let x,y;assume x in REAL & y in REAL;
  then reconsider X=x,Y=y as Element of REAL;
   addreal.(x,y) = X+Y by BINOP_2:def 9;
   hence addreal.(x,y) =addcomplex.(x,y) & addreal.(x,y) in REAL
     by BINOP_2:def 3,XREAL_0:def 1;
 end;
hence thesis by Th46,A5,A6,A2;
    end;
end;

theorem Th48:
  F is RAT-valued implies Sum F = addrat "**" F
proof
  assume A1:F is RAT-valued;
  rng F c= COMPLEX by A1,MEMBERED:1;
  then A2:F is COMPLEX-valued by RELAT_1:def 19;
  per cases by NAT_1:14;
    suppose A3:len F=0;
      hence addrat "**" F = 0 by Def8,A1,BINOP_2:3
                          .= Sum F by Def8,A2,A3,BINOP_2:1;
    end;
    suppose A4:len F>=1;
         A5: RAT = RAT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
  now let x,y;assume x in RAT & y in RAT;
  then reconsider X=x,Y=y as Element of RAT;
   addrat.(x,y) = X+Y by BINOP_2:def 15;
   hence addrat.(x,y) =addcomplex.(x,y) & addrat.(x,y) in RAT
     by BINOP_2:def 3,RAT_1:def 2;
 end;
hence thesis by Th46,A4,A5,A1;
    end;
end;

theorem Th49:
  F is INT-valued implies Sum F = addint "**" F
proof
      assume A1:F is INT-valued;
  rng F c= COMPLEX by A1,MEMBERED:1;
  then A2:F is COMPLEX-valued by RELAT_1:def 19;
  per cases by NAT_1:14;
    suppose A3:len F=0;
      hence addint "**" F = 0 by Def8,A1,BINOP_2:4
                          .= Sum F by Def8,A2,A3,BINOP_2:1;
    end;
    suppose A4:len F>=1;
         A5: INT = INT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
  now let x,y;assume x in INT & y in INT;
  then reconsider X=x,Y=y as Element of INT;
   addint.(x,y) = X+Y by BINOP_2:def 20;
   hence addint.(x,y) =addcomplex.(x,y) & addint.(x,y) in INT
     by BINOP_2:def 3, INT_1:def 2;
 end;
hence thesis by Th46,A4,A5,A1;
    end;
end;

theorem Th50:
  F is natural-valued implies Sum F = addnat "**" F
proof
      assume A1:F is natural-valued;
      then  rng F c= NAT by VALUED_0:def 6;
then A2:F is NAT-valued by RELAT_1:def 19;
  rng F c= COMPLEX by A1,MEMBERED:1;
  then A3:F is COMPLEX-valued by RELAT_1:def 19;
  per cases by NAT_1:14;
    suppose A4:len F=0;
      hence addnat "**" F = 0 by Def8,A2,BINOP_2:5
                          .= Sum F by Def8,A3,A4,BINOP_2:1;
    end;
    suppose A5:len F>=1;
         A6: NAT = NAT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
  now let x,y;assume x in NAT & y in NAT;
  then reconsider X=x,Y=y as Element of NAT;
   addnat.(x,y) = X+Y by BINOP_2:def 23;
   hence addnat.(x,y) =addcomplex.(x,y) & addnat.(x,y) in NAT
     by BINOP_2:def 3;
 end;
hence thesis by Th46,A5,A6,A2;
    end;
end;

registration
  let F be real-valued XFinSequence;
  cluster Sum F -> real;
  coherence
proof
   Sum F = addreal "**" F by Th47;
   hence thesis;
end;
end;

registration
  let F be RAT-valued XFinSequence;
  cluster Sum F -> rational;
  coherence
proof
   Sum F = addrat "**" F by Th48;
   hence thesis;
end;
end;

registration
  let F be INT-valued XFinSequence;
  cluster Sum F -> integer;
  coherence
proof
   Sum F = addint "**" F by Th49;
   hence thesis;
end;
end;

registration
  let F be natural-valued XFinSequence;
  cluster Sum F -> natural;
  coherence
proof
   Sum F = addnat "**" F by Th50;
   hence thesis;
end;
end;

registration
  cluster natural-valued -> nonnegative-yielding for Relation;
  coherence
proof
  let R be Relation;
assume R is natural-valued;
  then for r be Real st r in rng R holds r >=0;
 hence thesis by PARTFUN3:def 4;
end;
end;

theorem
  cF = {} implies Sum cF = 0;

theorem
   Sum <%c%> = c
proof
  c in COMPLEX by XCMPLX_0:def 2;
  hence thesis by Th37;
end;

theorem
   Sum <%c1,c2%> = c1 + c2
proof
  c1 in COMPLEX & c2 in COMPLEX by XCMPLX_0:def 2;
  then addcomplex "**" <%c1,c2%> = addcomplex.(c1,c2) by Th38
     .= c1+c2 by BINOP_2:def 3;
  hence thesis;
end;

theorem Th54: :: RLVECT_1:58 NUMERAL1:1
  Sum(cF1^cF2)=Sum(cF1)+Sum(cF2)
proof
A1:  cF1 is COMPLEX -valued & cF2 is COMPLEX -valued by Lm2;
  thus Sum(cF1^cF2)=addcomplex.(Sum(cF1),Sum(cF2)) by Th41,A1
    .= Sum(cF1)+Sum(cF2) by BINOP_2:def 3;
end;

theorem :: NUMERAL1:2
  for S being Real_Sequence st rF=S|(n+1) holds Sum rF = Partial_Sums(S).n
proof
  let S be Real_Sequence;
  A1:rF is REAL -valued by Lm3;
  n+1 c= NAT;
  then
A2: n+1 c= dom S by FUNCT_2:def 1;
  assume
A3: rF=S|(n+1);
  then dom rF = dom S /\ (n+1) by RELAT_1:61;
  then
A4: dom rF = n+1 by A2,XBOOLE_1:28;
  then consider f be sequence of REAL such that
A5: f.0 = rF.0 and
A6: for m be Nat st m+1 < len rF holds f.(m + 1) = addreal.(f.m,rF.(m + 1)) and
A7: addreal "**" rF = f.(len rF-1) by Def8,A1;
  defpred P[Nat] means $1 in dom rF implies f.$1=Partial_Sums(S).$1;
A8: now
    let k;
    assume
A9: P[k];
    thus P[k+1]
    proof
      assume
A10:  k+1 in dom rF;
      then
A11:  k+1 < len rF by AFINSQ_1:86;
      then
A12:  k<len rF by NAT_1:13;
      thus f.(k+1)= addreal.(f.k,rF.(k + 1)) by A6,A11
        .= (f.k)+rF.(k + 1) by BINOP_2:def 9
        .= (f.k)+S.(k+1) by A3,A10,FUNCT_1:47
        .= Partial_Sums(S).(k+1) by A9,A12,AFINSQ_1:86,SERIES_1:def 1;
    end;
  end;
  Partial_Sums(S).0=S.0 by SERIES_1:def 1;
  then
A13: P[0] by A3,A5,FUNCT_1:47;
A14: n in Segm(n+1) by NAT_1:45;
  for m holds P[m] from NAT_1:sch 2(A13,A8);
  hence Partial_Sums(S).n=f.n by A4,A14
     .= Sum rF by Th47,A7,A4;
end;

theorem Th56: :: NUMERAL1:4
  len rF1 = len rF2 &
  (for i st i in dom rF1 holds rF1.i<=rF2.i) implies
  Sum rF1 <= Sum rF2
proof
  set d=rF1,e=rF2;
assume that
A1: len d = len e and
A2: for i st i in dom d holds d.i<=e.i;
reconsider d,e as  XFinSequence of REAL by Lm3;
A3:  Sum d = addreal "**" d & Sum e = addreal "**" e by Th47;
per cases by NAT_1:14;
  suppose A4:len d >=1;
  consider f being sequence of REAL such that
A5: f.0 = d.0 and
A6: for n st n+1 < len d holds f.(n + 1) = addreal.
  (f.n,d.(n + 1)) and
A7: Sum d = f.(len d-1) by A4,Def8,A3;
  consider g being sequence of REAL such that
A8: g.0 = e.0 and
A9: for n st n+1 < len e holds g.(n + 1) = addreal.
  (g.n,e.(n + 1)) and
A10: Sum e = g.(len e-1) by A4,A1,Def8,A3;
  defpred P[Nat] means $1 in dom d implies f.$1 <= g.$1;
A11: now
    let i;
    assume
A12: P[i];
    thus P[i+1]
    proof
      assume
A13:  i+1 in dom d;
      then
A14:  i+1 < len d by AFINSQ_1:86;
      then
A15:  i < len d by NAT_1:13;
A16:  d.(i+1) <= e.(i+1) by A2,A13;
A17:  f.(i+1) = addreal.(f.i,d.(i + 1)) by A6,A14
        .= f.i + d.(i+1) by BINOP_2:def 9;
      g.(i+1) = addreal.(g.i,e.(i + 1)) by A1,A9,A14
        .= g.i + e.(i+1) by BINOP_2:def 9;
      hence thesis by A12,A15,A17,A16,AFINSQ_1:86,XREAL_1:7;
    end;
  end;
  reconsider ld=len d-1 as Element of NAT by A4,NAT_1:21;
  len d-1 < len d - 0 by XREAL_1:10;
  then
A18: ld in len d by AFINSQ_1:86;
A19: P[0] by A2,A5,A8;
  for i holds P[i] from NAT_1:sch 2(A19,A11);
  hence thesis by A1,A7,A10,A18;
end;
suppose len d=0;
  then Sum d = the_unity_wrt addreal & Sum e = the_unity_wrt addreal
     by Def8,A3,A1;
  hence thesis;
end;
end;

theorem Th57:
  Sum (n-->c) = n*c
proof
  set Fn= n-->c;
  reconsider Fn as XFinSequence of COMPLEX by Lm2;
A1:dom Fn = n by FUNCOP_1:13;
  now
    per cases;
    suppose
      dom Fn=0;
      hence thesis by A1;
    end;
    suppose
A2:   dom Fn>0;
      then consider f be sequence of COMPLEX such that
A3:   f.0 = Fn.0 and
A4:   for k st k+1 < len Fn holds
         f.(k + 1) = addcomplex.(f.k,Fn.(k + 1)) and
A5:   Sum Fn= f.(len Fn-1) by Def8;
      defpred P[Nat] means $1 < len Fn implies f.$1 =($1+1)*c;
A6:   for m st P[m] holds P[m+1]
      proof
        let m such that
A7:     P[m];
        assume
A8:     m + 1 < len Fn;
        then f.(m+1)=addcomplex.(f.m,Fn.(m+1)) by A4;
        then
A9:     f.(m + 1) = f.m + Fn.(m+1) by BINOP_2:def 3;
        Fn.(m+1) = c by A1,FUNCOP_1:7,A8,AFINSQ_1:86;
        hence thesis by A7,A8,A9,NAT_1:13;
      end;
      reconsider lenFn1=len Fn -1 as Element of NAT by A2,NAT_1:20;
A10:  lenFn1<lenFn1+1 by NAT_1:13;
A11:  P[0] by A3,A1,FUNCOP_1:7,AFINSQ_1:86;
      for m holds P[m] from NAT_1:sch 2(A11,A6);
      hence thesis by A5,A10,A1;
    end;
  end;
  hence thesis;
end;

theorem :: STIRL2_1:50
  (for n st n in dom rF holds rF.n <= r) implies
   Sum rF <= len rF * r
proof
  set L= len rF-->r;
  assume A1:n in dom rF implies rF.n <= r;
  A2:len L=len rF by FUNCOP_1:13;
  now let n;assume n in dom rF;
     then rF.n <= r & L.n = r by A1,FUNCOP_1:7;
     hence rF.n <= L.n;
  end;
  then Sum rF <= Sum L by Th56,A2;
  hence thesis by Th57;
end;

theorem :: STIRL2_1:51
  (for n st n in dom rF holds rF.n >= r) implies
  Sum rF >= len rF *r
proof
  set L=len rF-->r;
  assume A1:n in dom rF implies rF.n >= r;
  A2:len L=len rF by FUNCOP_1:13;
  now let n;assume n in dom rF;
     then rF.n >= r & L.n = r by A1,FUNCOP_1:7;
     hence rF.n >= L.n;
  end;
  then Sum rF >= Sum L by Th56,A2;
  hence thesis by Th57;
end;

theorem Th60: :: STIRL2_1:52
  rF is nonnegative-yielding & len rF > 0 &
  (ex x st x in dom rF & rF.x = r) implies Sum rF >= r
proof
  assume that
A1:rF is nonnegative-yielding and
A2: len rF > 0 and
A3: ex x st x in dom rF & rF.x = r;
  consider x such that
A4: x in dom rF and
A5: rF.x = r by A3;
  reconsider lenrF1=len rF-1 as Element of NAT by A2,NAT_1:20;
A6: dom rF=lenrF1+1;
  reconsider x as Element of NAT by A4;
A7: lenrF1 < lenrF1+1 by NAT_1:13;
A8:  x < len rF by A4,AFINSQ_1:86;
  then
A9: x<=lenrF1 by A6,NAT_1:13;
  rF is REAL-valued by Lm3;then
  consider f be sequence of REAL such that
A10: f.0 = rF.0 and
A11: for n st n+1 < len rF holds f.(n + 1) = addreal.(f.n,rF.(n + 1)) and
A12: addreal "**" rF= f.(len rF-1) by Def8,A2;
defpred P[Nat] means $1 < x implies f.$1 >= 0;
0 in len rF by A2,AFINSQ_1:86;
then rF.0 in rng rF by FUNCT_1:def 3;
then
A13:P[0] by A1,A10,PARTFUN3:def 4;
A14:P[n] implies P[n+1]
proof
  assume A15:P[n];
  assume A16:n+1 < x;
  then n < x & n+1 < len rF by A8,NAT_1:13,XXREAL_0:2;
  then A17:f.(n + 1) = addreal.(f.n,rF.(n + 1)) & f.n >=0 & n+1 in dom rF
       by A11,A15,AFINSQ_1:86;
  then rF.(n+1) in rng rF by FUNCT_1:def 3;
  then rF.(n+1) >=0 by A1,PARTFUN3:def 4;
  then f.n+rF.(n + 1) >=zz+zz by A16,A15,NAT_1:13;
  hence thesis by A17,BINOP_2:def 9;

end;
A18:P[n] from NAT_1:sch 2(A13,A14);
  defpred P[Nat] means x <= $1 & $1 < len rF implies f.$1 >= r;
  now
    per cases;
    suppose
A19:  x=0;
      assume that
      x <= x and
      x < len rF;
      thus f.x>=r by A5,A10,A19;
    end;
    suppose
      x>0;
      then reconsider x1=x-1 as Element of NAT by NAT_1:20;
      assume that
      x <= x and
A20:  x < len rF;
A21:       x1 <x1+1 by NAT_1:13;
      x1+1 < len rF by A20;
      then f.x = addreal.(f.x1,rF.x) by A11;
      then f.x=f.x1+rF.x & f.x1 >=0
       by A21,A18,BINOP_2:def 9;
      then f.x>=r+(0 qua Real) by A5,XREAL_1:7;
      hence f.x>=r;
    end;
  end;
  then
A22: P[x];
A23: for m be Nat st m>=x & P[m] holds P[m+1]
  proof
    let m be Nat such that
A24: m>=x and
A25: P[m];
    reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
    assume that
    x <= m+1 and
A26: m+1 < len rF;
       m+1 in dom rF by A26,AFINSQ_1:86;
then A27:rF.(m+1) in rng rF by FUNCT_1:def 3;
    f.(m1 + 1) = addreal.(f.m1,rF.(m1 + 1)) by A11,A26;
    then f.(m1+1)=f.m1+rF.(m1+1) & rF.(m1+1) >=0
   by A27,A1,BINOP_2:def 9,PARTFUN3:def 4;
    then f.(m+1) >= r+(0 qua Real) by A24,A25,A26,NAT_1:13,XREAL_1:7;
    hence thesis;
  end;
  for m be Nat st m>=x holds P[m] from NAT_1:sch 8(A22,A23);
  then addreal "**" rF >= r by A12,A9,A7;
  hence thesis by Th47;
end;

theorem Th61: :: STIRL2_1:53
  rF is nonnegative-yielding implies
  (Sum rF=0 iff (len rF=0 or rF = len rF --> 0))
proof
assume A1:
  rF is nonnegative-yielding;
  hereby
    assume
A2: Sum rF=0;
    assume
A3:    len rF <>0;
  set L=len rF -->0;
    assume rF <> len rF -->0;
    then consider k  such that
A4: k in dom L & L.k <> rF.k by AFINSQ_1:8,FUNCOP_1:13;
    rF.k in rng rF by A4,FUNCT_1:def 3;
    then L.k = 0 & rF.k >=0 by A4,A1,FUNCOP_1:7,PARTFUN3:def 4;
    hence contradiction by A2,Th60,A1,A4,A3;
 end;
A5:rF is COMPLEX-valued by Lm2;
    assume len rF=0 or rF= len rF -->0 ;
    then Sum rF = 0 or Sum rF = len rF *0 by A5,Th57,Def8,BINOP_2:1;
    hence thesis;
end;

theorem Th62:
  c(#)cF|n = (c(#)cF)|n
proof
  set ccF=c(#)cF;
  set cFn = cF|n;
A1:len ccF = len cF & len (c(#)cFn) = len cFn by VALUED_1:def 5;
  per cases;
    suppose A2:n <= len cF;
        then A3:len(cFn) = n & len (ccF|n)=n by A1,AFINSQ_1:54;
        now let i;
          assume i < len (c(#)cFn);
          then A4: i in dom (c(#)cFn) by AFINSQ_1:86;
          thus (c(#)cFn).i = c* (cFn.i) by VALUED_1:6
                           .= c* (cF.i) by A4,A2,AFINSQ_1:53
                           .=ccF.i by VALUED_1:6
             .=(ccF|n).i by A4,A1,A2,AFINSQ_1:53;
        end;
        hence thesis by A1,A3,AFINSQ_1:9;
    end;
    suppose n > len cF;
       then cF|n= cF & ccF|n=ccF by A1,AFINSQ_1:52;
       hence thesis;
    end;
end;

theorem
  c * Sum cF = Sum (c(#)cF)
proof
    defpred P[Nat] means for cF st len cF=$1 holds
  c * Sum cF = Sum (c(#)cF);
A1: for k st P[k] holds P[k+1]
  proof
    let k such that
A2: P[k];
A3: k<k+1 by NAT_1:13;
    let cF such that
A4: len cF=k+1;
    set cF1 = c(#)cF;
A5: dom cF=dom cF1 by VALUED_1:def 5;
    reconsider cF,cF1 as XFinSequence of COMPLEX by Lm2;
A6: cF|(k+1)=cF by A4;
A7: len (cF|k)=k by A3,AFINSQ_1:11,A4;
    k<k+1 by NAT_1:13;
    then
A8: k in dom cF by A4,AFINSQ_1:86;
    then addcomplex.
      (addcomplex "**" cF|k, cF.k) = addcomplex "**" cF|(k+1) by Th42;
    then
A9: Sum cF=Sum (cF|k)+cF.k by A6,BINOP_2:def 3;
A10: c * Sum (cF|k)= Sum (c(#)(cF|k)) by A2,A7
        .= Sum(cF1|k) by Th62;
A11: c*cF.k=cF1.k by VALUED_1:6;
A12: cF1|(k+1)=cF1 by A4,A5;
    addcomplex.(addcomplex "**" cF1|k,cF1.k)
     =addcomplex "**" cF1|(k+1) by A5,A8,Th42;
    then Sum cF1=Sum (cF1|k)+cF1.k by A12,BINOP_2:def 3;
    hence thesis by A9,A11,A10;
  end;
A13: P[0]
  proof
    let cF such that
A14: len cF=0;
    set cF1 = c(#)cF;
      reconsider cF,cF1 as XFinSequence of COMPLEX by Lm2;
A15: addcomplex "**" cF=0 by Def8,BINOP_2:1,A14;
    len cF1=0 by A14,VALUED_1:def 5;
    hence thesis by A15,Def8,BINOP_2:1;
  end;
 for k holds P[k] from NAT_1:sch 2(A13,A1);
  then P[len cF];
  hence thesis;
end;

theorem Th64: :: CARD_FIN:44
   n in dom cF implies Sum (cF|n) + cF.n = Sum (cF|(n+1))
proof
  assume
A1:  n in dom cF;
    reconsider cF as XFinSequence of COMPLEX by Lm2;
 addcomplex.(addcomplex "**" cF|n, cF.n) = addcomplex "**" cF|(n+1)
      by Th42,A1;
  hence thesis by BINOP_2:def 3;
end;

theorem Th65: ::CARD_FIN:13
for f be Function st
  f.y=x & y in dom f holds {y}\/(f|(dom f\{y}))"{x}=f"{x}
proof
  let f be Function;
  assume that
A1: f.y=x and
A2: y in dom f;
  set d=dom f\{y};
A3: (f|d)"{x} c= f"{x}
  proof
    let x1 be object such that
A4: x1 in (f|d)"{x};
A5: (f|d).x1 in {x} by A4,FUNCT_1:def 7;
A6: x1 in dom (f|d) by A4,FUNCT_1:def 7;
    then dom (f|d)=dom f/\d & f.x1=(f|d).x1 by FUNCT_1:47,RELAT_1:61;
    hence thesis by A6,A5,FUNCT_1:def 7;
  end;
A7: f"{x} c= {y}\/(f|d)"{x}
  proof
    let x1 be object such that
A8: x1 in f"{x};
    x1 in dom f & not x1 in {y} or x1=y by A8,FUNCT_1:def 7,TARSKI:def 1;
    then x1 in dom f & x1 in d & dom (f|d)=dom f/\d or x1=y by RELAT_1:61
,XBOOLE_0:def 5;
    then x1 in dom (f|d) or x1=y by XBOOLE_0:def 4;
    then x1 in dom (f|d) & f.x1=(f|d).x1 & f.x1 in {x} or x1 in {y} by A8,
FUNCT_1:47,def 7,TARSKI:def 1;
    then x1 in (f|d)"{x} or x1 in {y} by FUNCT_1:def 7;
    hence thesis by XBOOLE_0:def 3;
  end;
  {y} c= f"{x}
  proof
    let z be object;
    assume z in {y};
    then
A9: z=y by TARSKI:def 1;
    f.y in {x} by A1,TARSKI:def 1;
    hence thesis by A2,A9,FUNCT_1:def 7;
  end;
  hence thesis by A7,A3,XBOOLE_1:8;
end;

theorem Th66: :: CARD_FIN:15
 for x,y being object
 for f be Function st f.y<>x holds (f|(dom f\{y}))"{x}=f"{x}
proof let x,y be object;
  let f be Function;
  set d=dom f\{y};
  assume
A1: f.y<>x;
A2: f"{x} c= (f|d)"{x}
  proof
A3: dom (f|d)=dom f/\d by RELAT_1:61;
    let x1 be object such that
A4: x1 in f"{x};
A5: f.x1 in {x} by A4,FUNCT_1:def 7;
    f.x1 in {x} by A4,FUNCT_1:def 7;
    then f.x1=x by TARSKI:def 1;
    then
A6: not x1 in {y} by A1,TARSKI:def 1;
    x1 in dom f by A4,FUNCT_1:def 7;
    then x1 in d by A6,XBOOLE_0:def 5;
    then
A7: x1 in dom (f|d) by A3,XBOOLE_0:def 4;
    then f.x1=(f|d).x1 by FUNCT_1:47;
    hence thesis by A7,A5,FUNCT_1:def 7;
  end;
  (f|d)"{x} c= f"{x}
  proof
    let x1 be object such that
A8: x1 in (f|d)"{x};
A9: (f|d).x1 in {x} by A8,FUNCT_1:def 7;
A10: x1 in dom (f|d) by A8,FUNCT_1:def 7;
    then dom (f|d)=dom f/\d & f.x1=(f|d).x1 by FUNCT_1:47,RELAT_1:61;
    hence thesis by A10,A9,FUNCT_1:def 7;
  end;
  hence thesis by A2;
end;

theorem :: CATALAN2:45
  rng cF c= {0,c} implies Sum cF = c * card (cF"{c})
proof
  defpred P[Nat] means for cF,c st len cF=$1 &
  rng cF c= {0,c} holds Sum cF = c* card (cF"{c});
assume
A1: rng cF c= {0,c};
A2: for k st P[k] holds P[k+1]
  proof
    let k such that
A3: P[k];
    let F be complex-valued XFinSequence,
     c be Complex such that
A4: len F=k+1 and
A5: rng F c= {0,c};
    per cases;
    suppose
A6:   c <>0;
      ( not k in k)& Segm k \/ {k}= Segm(k+1) by AFINSQ_1:2;
      then
A7:   dom F\{k}=k by A4,ZFMISC_1:117;
      k <k+1 by NAT_1:13;
      then k in dom F by A4,AFINSQ_1:86;
      then
A8:   F.k in rng F by FUNCT_1:def 3;
      per cases by A5,A8,TARSKI:def 2;
      suppose
A9:     F.k=0;
A10:    F|(k+1)=F by A4;
A11:    k <k+1 by NAT_1:13; then
A12:    Sum (F|k) + (0 qua Real)= Sum F by A9,A10,Th64,A4,AFINSQ_1:86;
A13:    len (F|k)=k by A4,A11,AFINSQ_1:54;
        rng (F|k) c= rng F & (F|k)"{c}=F"{c} by A6,A7,A9,Th66;
        hence thesis by A3,A5,A13,A12,XBOOLE_1:1;
      end;
      suppose
A14:    F.k=c;
        set Fk=(F|k)"{c};
        not k in k;
        then not k in dom (F|k);
        then
A15:    not k in Fk by FUNCT_1:def 7;
A16:    k <k+1 by NAT_1:13;
        then
A17:    k in dom F by A4,AFINSQ_1:86;
        rng (F| k) c= rng F & len (F|k)= k by A4,A16,AFINSQ_1:54;
        then
A18:    Sum (F|k)=c* card ((F|k)"{c}) by A3,A5,XBOOLE_1:1;
        F|(k+1)=F by A4;
        then
A19:    Sum (F|k)+ c = Sum F by A14,A17,Th64;
        {k}\/Fk=F"{c} by A7,A14,A17,Th65;
        then (card Fk)+1=card (F"{c}) by A15,CARD_2:41;
        hence thesis by A18,A19;
      end;
    end;
    suppose
A20:  c = 0;
      for x being object st x in dom F holds F.x = 0
      proof
        let x be object;
        assume x in dom F;
        then F.x in rng F by FUNCT_1:def 3;
        hence thesis by A5,A20,TARSKI:def 2;
      end;
      then F = dom F --> 0 by FUNCOP_1:11;
      then Sum F = len F*0 by Th61;
hence thesis by A20;
    end;
  end;
A21: P[0]
  proof
    let F be complex-valued XFinSequence,
c be Complex such that
A22: len F=0 and
    rng F c= {0,c};
    F"{c} c= 0 & F={} by A22,RELAT_1:132;
then card (F"{c})=0 & Sum F =0;
    hence thesis;
  end;
 for k holds P[k] from NAT_1:sch 2(A21,A2);
then P[len cF];
  hence thesis by A1;
end;

theorem :: CATALAN2:48
  Sum cF = Sum Rev cF
proof
  cF is COMPLEX-valued by Lm2;then
  reconsider Fr2 = cF,Fr1 = Rev cF as XFinSequence of COMPLEX;
A1: len Fr1=len Fr2 by Def1;
  defpred P[object,object] means for i st i=$1 holds $2=len Fr1-(1+i);
A2: card len Fr1 =card len Fr1;
A3: for x being object st x in len Fr1
ex y being object st y in len Fr1 & P[x,y]
  proof
    let x be object such that
A4: x in len Fr1;
     reconsider k=x as Element of NAT by Th1,A4;
    k+1 <= len Fr1 by NAT_1:13,A4,AFINSQ_1:86;
    then
A5: len Fr1-'(1+k)=len Fr1-(1+k) by XREAL_1:233;
    take len Fr1-'(1+k);
    len Fr1 +zz< len Fr1 +(1+k) by XREAL_1:8;
    then len Fr1-(1+k) < len Fr1+(1+k)-(1+k) by XREAL_1:9;
    hence thesis by A5,AFINSQ_1:86;
  end;
  consider P be Function of len Fr1,len Fr1 such that
A6: for x being object st x in len Fr1 holds P[x,P.x] from FUNCT_2:sch 1(A3);
 for x1,x2 be object
    st x1 in len Fr1 & x2 in len Fr1 & P.x1 = P.x2 holds x1 = x2
  proof
    let x1,x2 be object such that
A7: x1 in len Fr1 and
A8: x2 in len Fr1 and
A9: P.x1 = P.x2;
     reconsider i=x1,j=x2 as Element of NAT by A7,A8,Th1;
A10: P.x2=len Fr1-(1+j) by A6,A8;
    P.x1=len Fr1-(1+i) by A6,A7;
    hence thesis by A9,A10;
  end;
  then
A11: P is one-to-one by FUNCT_2:56;
  then P is onto by A2,Lm1;
  then reconsider P as Permutation of dom Fr1 by A11;
A12: now
    let x be object such that
A13: x in dom Fr1;
    reconsider k=x as Element of NAT by A13;
    P.k=len Fr1-(1+k) by A6,A13;
    hence Fr1.x=Fr2.(P.x) by A1,Def1,A13;
  end;
A14: now
    let x be object such that
A15: x in dom Fr1;
    x in dom P by A15,FUNCT_2:52;
    then P.x in rng P by FUNCT_1:3;
    hence x in dom P & P.x in dom Fr2 by A1,A15,FUNCT_2:52;
  end;
  for x being object st x in dom P & P.x in dom Fr2 holds x in dom Fr1;
  then Fr1 = Fr2 * P by A14,A12,FUNCT_1:10;
  hence thesis by A1,Th44;
end;

theorem Th69:
  for f be Function,p,q,fp,fq be XFinSequence st
       rng p c= dom f & rng q c= dom f & fp = f*p & fq = f*q
    holds fp ^ fq = f*(p^q)
proof
  let f be Function,p,q,fp,fq be XFinSequence such that
A1:       rng p c= dom f & rng q c= dom f & fp = f*p & fq = f*q;
set pq=p^q;
A2:rng pq = rng p \/rng q by AFINSQ_1:26;
then A3:dom (f*pq)=dom pq by A1,RELAT_1:27,XBOOLE_1:8;
reconsider fpq = f*pq as XFinSequence by A2,A1,AFINSQ_1:10,XBOOLE_1:8;
A4:dom fp=dom p & dom fq = dom q by A1,RELAT_1:27;
A5:dom pq=len p+len q & dom (fp^fq) = len fp+len fq by AFINSQ_1:def 3;
A6:len fpq = len (fp^fq) by A2,A1,A4,A5,RELAT_1:27,XBOOLE_1:8;
k < len fpq implies (fp^fq).k = fpq.k
proof
  assume A7:k< len fpq;
  then A8:k in dom fpq by AFINSQ_1:86;
  per cases;
   suppose k < len p;
      then k in dom p by AFINSQ_1:86;
      then pq.k = p.k & fp.k = f.(p.k) & (fp^fq).k =fp.k
        by A1,A4,AFINSQ_1:def 3,FUNCT_1:13;
      hence thesis by A8,FUNCT_1:12;
   end;
   suppose A9:k >= len p;
      then reconsider kp=k-len p as Element of NAT by NAT_1:21;
      len p + kp < len p+len q by A5,A2,A1,A7,RELAT_1:27,XBOOLE_1:8;
      then
      kp < len q by XREAL_1:7;
      then pq.k = q.kp & (fp^fq).k = fq.kp & fq.kp = f.(q.kp)
          by A7,A1,A3,A4,A5,A9,AFINSQ_1:18,FUNCT_1:13,AFINSQ_1:86;
      hence thesis by A8,FUNCT_1:12;
   end;
end;
hence thesis by A6,AFINSQ_1:9;
end;

theorem
  for B1,B2 being finite natural-membered set st
     B1 <N< B2 holds
Sum (SubXFinS(cF,B1\/B2))=Sum (SubXFinS(cF,B1))+Sum(SubXFinS(cF,B2))
proof
  let B1,B2 be finite natural-membered set such that A1: B1 <N< B2;
  set B12=B1\/B2;
  set B12L=B12/\len cF;
  set B1L=B1/\len cF;
  set B2L=B2/\len cF;
  B1L\/B2L=B12L by XBOOLE_1:23;
  then A3:Sgm0(B12L) = Sgm0(B1L) ^ Sgm0(B2L) by Th35,A1,Th25;
rng Sgm0(B1L) = B1L & rng Sgm0(B2L) = B2L by Def4;
  then rng Sgm0(B1L) c= dom cF & rng Sgm0(B2L) c= dom cF by XBOOLE_1:17;
  then SubXFinS (cF,B1) ^ SubXFinS (cF,B2) = SubXFinS (cF,B12) by A3,Th69;
hence thesis by Th54;
end;

:: missing, 2010.05.15, A.T.

theorem Th71:
 b is having_a_unity implies b "**" <%>D = the_unity_wrt b
proof
A1: len <%>D = 0;
  assume b is having_a_unity;
  hence thesis by A1,Def8;
end;

definition
  let D be set, F be XFinSequence of D^omega;
  func FlattenSeq F -> Element of D^omega means
  :Def10:
  ex g being BinOp of D^omega st
  (for p, q being Element of D^omega holds g.(p,q) = p^q) & it = g "**" F;
  existence
  proof
    deffunc F(Element of D^omega,Element of D^omega) = $1^$2;
    consider g being BinOp of D^omega such that
A1: for a, b being Element of D^omega holds g.(a,b) = F(a,b)
        from BINOP_1:sch 4;
    take g "**" F, g;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let it1, it2 be Element of D^omega;
    given g1 being BinOp of D^omega such that
A2: for p, q being Element of D^omega holds g1.(p,q) = p^q and
A3: it1 = g1 "**" F;
    given g2 being BinOp of D^omega such that
A4: for p, q being Element of D^omega holds g2.(p,q) = p^q and
A5: it2 = g2 "**" F;
    now
      let a, b be Element of D^omega;
      thus g1.(a,b) = a^b by A2
        .= g2.(a,b) by A4;
    end;
    hence thesis by A3,A5,BINOP_1:2;
  end;
end;

theorem
  for D being set, d be Element of D^omega holds FlattenSeq <%d%> = d
proof
  let D be set, d be Element of D^omega;
  ex g being BinOp of D^omega st
  (for p, q being Element of D^omega holds g.(p,q) = p^q) &
  FlattenSeq <%d%> = g "**" <% d %> by Def10;
  hence thesis by Th37;
end;

theorem
  for D being set holds FlattenSeq <%>(D^omega) = <%>D
proof
  let D be set;
  consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <%>(D^omega) = g "**" <%>(D^omega) by Def10;
A3: {} is Element of D^omega by AFINSQ_1:43;
  reconsider p = {} as Element of D^omega by AFINSQ_1:43;
  now
    let a be Element of D^omega;
    thus g.({},a) = {} ^ a by A1,A3
      .= a;
    thus g.(a,{}) = a ^ {} by A1,A3
      .= a;
  end;
  then
A4: p is_a_unity_wrt g by BINOP_1:3;
  then g "**" <%>(D^omega) = the_unity_wrt g by Th71,SETWISEO:def 2;
  hence thesis by A2,A4,BINOP_1:def 8;
end;

theorem Th74:
  for D being set, F,G be XFinSequence of D^omega holds
  FlattenSeq (F ^ G) = FlattenSeq F ^ FlattenSeq G
proof
  let D be set, F,G be XFinSequence of D^omega;
  consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq (F ^ G) = g "**" F ^ G by Def10;
  now
    let a,b,c be Element of D^omega;
    thus g.(a,g.(b,c)) = a ^ g.(b,c) by A1
      .= a ^ (b ^ c) by A1
      .= a ^ b ^ c by AFINSQ_1:27
      .= g.(a,b) ^ c by A1
      .= g.(g.(a,b),c) by A1;
  end;
  then
A3: g is associative;
A4: {} is Element of D^omega by AFINSQ_1:43;
  reconsider p = {} as Element of D^omega by AFINSQ_1:43;
  now
    let a be Element of D^omega;
    thus g.({},a) = {} ^ a by A1,A4
      .= a;
    thus g.(a,{}) = a ^ {} by A1,A4
      .= a;
  end;
  then p is_a_unity_wrt g by BINOP_1:3;
  then g is having_a_unity or len F >= 1 & len G >= 1 by SETWISEO:def 2;
  hence FlattenSeq (F ^ G) = g.(g "**" F,g "**" G) by A2,A3,Th41
    .= (g "**" F) ^ (g "**" G) by A1
    .= FlattenSeq F ^ (g "**" G) by A1,Def10
    .= FlattenSeq F ^ FlattenSeq G by A1,Def10;
end;

theorem
  for D being set, p,q be Element of D^omega holds FlattenSeq <% p,q %> = p ^ q
proof
  let D be set, p,q be Element of D^omega;
  consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <% p,q %> = g "**" <% p,q %> by Def10;
  thus FlattenSeq <% p,q %> = g.(p,q) by A2,Th38
    .= p ^ q by A1;
end;

theorem
  for D being set, p,q,r be Element of D^omega holds
  FlattenSeq <% p,q,r %> = p ^ q ^ r
proof
  let D be set, p,q,r be Element of D^omega;
  consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <% p,q,r %> = g "**" <% p,q,r %> by Def10;
  thus FlattenSeq <% p,q,r %> = g.(g.(p,q),r) by A2,Th39
    .= g.(p,q) ^ r by A1
    .= p ^ q ^ r by A1;
end;

theorem Th77:
  p c= q implies p ^ (q /^ len p) = q
 proof assume
A1: p c= q;
A2: len p + len (q /^ len p)
       = len p + (len q -' len p) by Def2
      .= len q + len p -' len p by A1,NAT_1:43,NAT_D:38
      .= dom q by NAT_D:34;
A3: for k st k in dom p holds q.k=p.k by A1,GRFUNC_1:2;
   for k st k in dom(q /^ len p) holds q.(len p + k) = (q /^ len p).k
                by Def2;
  hence p ^ (q /^ len p) = q by A2,A3,AFINSQ_1:def 3;
 end;

reserve r,s for XFinSequence;

theorem Th78:
  p c= q implies ex r st p^r = q
proof
 assume
A1: p c= q;
 take r = q /^ len p;
 thus p^r = q by A1,Th77;
end;

theorem Th79:
  for p,q being XFinSequence of D st p c= q
    ex r being XFinSequence of D st p^r = q
proof
 let p,q being XFinSequence of D;
 assume p c= q;
  then consider r such that
A1: p^r = q by Th78;
  reconsider r as XFinSequence of D by A1,AFINSQ_1:31;
 take r;
 thus thesis by A1;
end;

theorem
  q c= r implies p^q c= p^r
proof
  assume q c= r;
  then consider s such that
A1: q^s = r by Th78;
  p^q c= p^q^s by AFINSQ_1:74;
  hence thesis by A1,AFINSQ_1:27;
end;

theorem
  for D being set, F,G be XFinSequence of D^omega holds
    F c= G implies FlattenSeq F c= FlattenSeq G
proof
  let D be set, F,G be XFinSequence of D^omega;
  assume F c= G;
  then consider F9 being XFinSequence of D^omega such that
A1: F ^ F9 = G by Th79;
  FlattenSeq F ^ FlattenSeq F9 = FlattenSeq G by A1,Th74;
  hence thesis by AFINSQ_1:74;
end;

registration let p; let q be non empty XFinSequence;
  cluster p^q -> non empty;
  coherence by AFINSQ_1:30;
  cluster q^p -> non empty;
  coherence by AFINSQ_1:30;
end;

theorem
  CutLastLoc(p^<%x%>) = p
proof set q = CutLastLoc(p^<%x%>);
A1: len(p^<%x%>) -' 1 = len p + 1 -' 1 by AFINSQ_1:75
     .= len p by NAT_D:34;
A2: dom(p^<%x%>) = len(p^<%x%>)
   .= Segm(len p + 1) by AFINSQ_1:75
   .= Segm len p \/ {len p} by AFINSQ_1:2;
A3: not len p in dom p;
 LastLoc(p^<%x%>) = len(p^<%x%>) -' 1 by AFINSQ_1:70;
 hence
A4: dom q = dom(p^<%x%>) \ {len p} by A1,VALUED_1:36
     .= dom p by A2,A3,ZFMISC_1:117;
 let y be object;
 assume
A5: y in dom q;
A6: p c= p^<%x%> by AFINSQ_1:74;
 thus q.y = (p^<%x%>).y by A5,GRFUNC_1:2
      .= p.y by A5,A4,A6,GRFUNC_1:2;
end;

:: generalizes BALLOT_1:1 to empty D
theorem Th17:
  for D being set, p being XFinSequence of D, n being Nat
  holds XFS2FS(p|n) = (XFS2FS p)|n & XFS2FS(p/^n) = (XFS2FS p)/^n
proof
  let D be set, p be XFinSequence of D, n be Nat;
  :: first part
  thus XFS2FS(p|n) = (XFS2FS p)|n
  proof
    A1: now
      let x be object;
      hereby
        assume A2: x in dom XFS2FS(p|n);
        then reconsider m1 = x as Nat;
        A3: 1 <= m1 & m1 <= len XFS2FS(p|n) by A2, FINSEQ_3:25;
        then reconsider m = m1 - 1 as Nat by INT_1:74;
        m+1 in dom XFS2FS(p|n) by A2;
        then m in dom(p|n) by AFINSQ_1:95;
        then A4: m in dom p & m in n by RELAT_1:57;
        then A5: m+1 in dom XFS2FS p by AFINSQ_1:95;
        m in Segm n by A4;
        then m < n by NAT_1:44;
        then m+1 <= n by NAT_1:13;
        then x in dom((XFS2FS p)|Seg n) by A3, A5, FINSEQ_1:1, RELAT_1:57;
        hence x in dom((XFS2FS p)|n) by FINSEQ_1:def 15;
      end;
      assume x in dom((XFS2FS p)|n);
      then x in dom((XFS2FS p)|Seg n) by FINSEQ_1:def 15;
      then A6: x in dom XFS2FS p & x in Seg n by RELAT_1:57;
      then reconsider m1 = x as Nat;
      A7: 1 <= m1 & m1 <= n by A6, FINSEQ_1:1;
      then reconsider m = m1-1 as Nat by INT_1:74;
      m+1 in dom XFS2FS p by A6;
      then A8: m in dom p by AFINSQ_1:95;
      m+1 <= n by A7;
      then m < n by NAT_1:13;
      then m in Segm n by NAT_1:44;
      then m in dom(p|n) by A8, RELAT_1:57;
      then m+1 in dom XFS2FS(p|n) by AFINSQ_1:95;
      hence x in dom XFS2FS(p|n);
    end;
    for k being Nat st k in dom XFS2FS(p|n)
      holds (XFS2FS(p|n)).k = ((XFS2FS p)|n).k
    proof
      let k be Nat;
      assume A9: k in dom XFS2FS(p|n);
      then A10: 1 <= k & k <= len XFS2FS(p|n) by FINSEQ_3:25;
      then reconsider m = k-1 as Nat by INT_1:74;
      m+1 in dom XFS2FS(p|n) by A9;
      then A11: m in dom(p|n) by AFINSQ_1:95;
      then m in Segm len(p|n);
      then m < len(p|n) by NAT_1:44;
      then A12: m+1 <= len(p|n) by NAT_1:13;
      Segm len(p|n) c= Segm len p by RELAT_1:60;
      then len(p|n) <= len p by NAT_1:39;
      then A13: k <= len p by A12, XXREAL_0:2;
      m in Segm n by A11;
      then m < n by NAT_1:44;
      then m+1 <= n by NAT_1:13;
      then A14: k in Seg n by A10, FINSEQ_1:1;
      thus (XFS2FS(p|n)).k = (p|n).(m+1-'1) by A10, A12, AFINSQ_1:def 9
        .= (p|n).m by NAT_D:34
        .= p.m by A11, FUNCT_1:47
        .= p.(m+1-'1) by NAT_D:34
        .= (XFS2FS p).k by A10, A13, AFINSQ_1:def 9
        .= ((XFS2FS p)|Seg n).k by A14, FUNCT_1:49
        .= ((XFS2FS p)|n).k by FINSEQ_1:def 15;
    end;
    hence XFS2FS(p|n) = (XFS2FS p)|n by A1, TARSKI:2;
  end;
  :: second part
  per cases;
  suppose A15: len p <= n;
    then p/^n = {} by Th6;
    then A16: XFS2FS(p/^n) = {};
    len((XFS2FS p)/^n) = 0
    proof
      per cases by A15, XXREAL_0:1;
      suppose len p < n;
        then A17: len p - n < n-n by XREAL_1:14;
        thus len((XFS2FS p)/^n) = len XFS2FS p -' n by RFINSEQ:29
          .= len p -' n by AFINSQ_1:def 9
          .= 0 by A17, XREAL_0:def 2;
      end;
      suppose A18: len p = n;
        thus len((XFS2FS p)/^n) = len XFS2FS p -' n by RFINSEQ:29
          .= 0 + len p -' n by AFINSQ_1:def 9
          .= 0 by A18, NAT_D:34;
      end;
    end;
    hence thesis by A16;
  end;
  suppose A19: n < len p;
    then A20: n <= len XFS2FS p by AFINSQ_1:def 9;
    A21: len XFS2FS(p/^n) = len(p/^n) by AFINSQ_1:def 9
      .= len p -' n by Def2
      .= len XFS2FS p -' n by AFINSQ_1:def 9
      .= len((XFS2FS p)/^n) by RFINSEQ:29;
    now
      let k be Nat;
      assume A22: 1 <= k & k <= len XFS2FS(p/^n);
      then A23: 1 <= k & k <= len(p/^n) by AFINSQ_1:def 9;
      then reconsider m = k-1 as Nat by INT_1:74;
      m+1 <= len(p/^n) by A23;
      then m < len(p/^n) by NAT_1:13;
      then m in Segm len(p/^n) by NAT_1:44;
      then A24: m in dom(p/^n);
      A25: k in dom((XFS2FS p)/^n) by A21, A22, FINSEQ_3:25;
      A26: 1+0 <= k+n by A23, XREAL_1:7;
      k <= len p - n by A19, A23, Th7;
      then A27: k+n <= len p - n + n by XREAL_1:6;
      thus (XFS2FS(p/^n)).k = (p/^n).(m+1-'1) by A23, AFINSQ_1:def 9
        .= (p/^n).m by NAT_D:34
        .= p.(m+n) by A24, Def2
        .= p.(n+m+1-'1) by NAT_D:34
        .= (XFS2FS p).(k+n) by A26, A27, AFINSQ_1:def 9
        .= ((XFS2FS p)/^n).k by A20, A25, RFINSEQ:def 1;
    end;
    hence thesis by A21;
  end;
end;

theorem Th5: :: from BALLOT_1:5
  for D being set
  for d be FinSequence of D holds XFS2FS (FS2XFS d) = d
proof
  let D be set;
  let d be FinSequence of D;
  set Xd=FS2XFS d;
A1: len d = len Xd by AFINSQ_1:def 8;
A2: len Xd = len XFS2FS Xd by AFINSQ_1:def 9;
  now let i such that
A3: 1 <= i and
A4: i <= len d;
    reconsider i1=i-1 as Nat by A3,NAT_1:21;
A5: i1+1 = i;
A6: i-'1 = i1 by XREAL_0:def 2;
    thus d.i = Xd.i1 by A4,A5,NAT_1:13,AFINSQ_1:def 8
            .= (XFS2FS Xd).i by A3,A4,A6,A1,AFINSQ_1:def 9;
  end;
  hence thesis by A1,A2;
end;

registration
  let D be set, f be FinSequence of D;
  reduce XFS2FS (FS2XFS f) to f;
  reducibility by Th5;
end;

theorem
  for D being set, p being FinSequence of D, n being Nat
  holds (FS2XFS p)|n = FS2XFS(p|n) & (FS2XFS p)/^n = FS2XFS(p/^n)
proof
  let D be set, p be FinSequence of D, n be Nat;
  thus (FS2XFS p)|n = FS2XFS XFS2FS((FS2XFS p)|n)
    .= FS2XFS((XFS2FS FS2XFS p)|n) by Th17
    .= FS2XFS(p|n);
  thus (FS2XFS p)/^n = FS2XFS XFS2FS((FS2XFS p)/^n)
    .= FS2XFS((XFS2FS FS2XFS p)/^n) by Th17
    .= FS2XFS(p/^n);
end;

:: analogous theorem of FINSEQ_5:34
theorem
  for D being set, p being one-to-one XFinSequence of D, n being Nat
  holds rng(p|n) misses rng(p/^n)
proof
  let D be set, p be one-to-one XFinSequence of D, n be Nat;
  rng((XFS2FS p)|n) misses rng((XFS2FS p)/^n) by FINSEQ_5:34;
  then rng((XFS2FS p)|n) misses rng(XFS2FS(p/^n)) by Th17;
  then rng(XFS2FS(p|n)) misses rng(XFS2FS(p/^n)) by Th17;
  then rng(XFS2FS(p|n)) misses rng(p/^n) by AFINSQ_1:97;
  hence rng(p|n) misses rng(p/^n) by AFINSQ_1:97;
end;

registration
  cluster finite for Ordinal-Sequence;
  existence
  proof
    reconsider f = 0 --> omega as Ordinal-Sequence;
    take f;
    thus thesis;
  end;
end;

registration
  let A be finite Ordinal-Sequence, n be Nat;
  cluster A /^ n -> Ordinal-yielding;
  coherence
  proof
    consider a being Ordinal such that
    A1: rng A c= a by ORDINAL2:def 4;
    rng(A /^ n) c= rng A by Th9;
    hence thesis by A1, XBOOLE_1:1, ORDINAL2:def 4;
  end;
end;