The Mizar article:

Some Properties of Restrictions of Finite Sequences

by
Czeslaw Bylinski

Received January 25, 1995

Copyright (c) 1995 Association of Mizar Users

MML identifier: FINSEQ_5
[ MML identifier index ]


environ

 vocabulary ARYTM_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_4, REALSET1, RFINSEQ,
      BOOLE, RLSUB_2, FINSEQ_5;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, RELAT_1,
      FUNCT_1, FINSEQ_1, FINSEQ_4, REALSET1, RFINSEQ, TOPREAL1;
 constructors REAL_1, NAT_1, REALSET1, RFINSEQ, TOPREAL1, FINSEQ_4, INT_1,
      MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, FINSEQ_1, RELSET_1, INT_1, TOPREAL1, NAT_1,
      MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, FUNCT_1, XBOOLE_0;
 theorems TARSKI, AXIOMS, ZFMISC_1, REAL_1, NAT_1, RLVECT_1, RLVECT_2,
      PARTFUN2, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, RFINSEQ,
      SPPOL_1, REALSET1, TOPREAL1, TOPREAL4, GOBOARD1, PROB_1, RELAT_1,
      GROUP_5, INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes FINSEQ_1;

begin

reserve i,j,k,m,n for Nat;

theorem Th1:
   i <= n implies n - i + 1 is Nat
 proof assume i <= n;
  then reconsider n_i = n - i as Nat by INT_1:18;
     n_i + 1 is Nat;
  hence thesis;
 end;

theorem Th2:
   i in Seg n implies n - i + 1 in Seg n
 proof
   assume A1: i in Seg n;
then 1 <= i & i <= n by FINSEQ_1:3;
   then reconsider n_i = n - i as Nat by INT_1:18;
   reconsider j = n_i + 1 as Nat;
     0 <= n_i by NAT_1:18;
then A2:  0+1 <= j by AXIOMS:24;
     0 <= i by NAT_1:18;
   then n_i <= n by PROB_1:2;
then A3:  j <= n + 1 by AXIOMS:24;
     now assume j = n + 1;
    then n_i = n + 1 - 1 by XCMPLX_1:26 .= n by XCMPLX_1:26;
    then 0 = n_i-n by XCMPLX_1:14
          .= (-i+n)-n by XCMPLX_0:def 8
          .= -i by XCMPLX_1:26;
    hence contradiction by A1,FINSEQ_1:3,REAL_1:26;
   end;
   then j < n + 1 by A3,REAL_1:def 5;
   then j <= n by NAT_1:38;
   hence thesis by A2,FINSEQ_1:3;
 end;

theorem Th3:
   for f being Function, x,y being set st f"{y} = {x}
    holds x in dom f & y in rng f & f.x = y
 proof let f be Function, x,y be set;
  assume f"{y} = {x};
then A1:  x in f"{y} by TARSKI:def 1;
  hence
A2:  x in dom f by FUNCT_1:def 13;
    f.x in {y} by A1,FUNCT_1:def 13;
  then f.x = y by TARSKI:def 1;
  hence thesis by A2,FUNCT_1:def 5;
 end;

theorem
     for f being Function holds f is one-to-one iff
    for x being set st x in dom f holds f"{f.x} = {x}
 proof let f be Function;
    now
   hereby
    assume
A1:  for x being set st x in dom f holds f is_one-to-one_at x;
    let x be set;
    assume x in dom f;
    then f is_one-to-one_at x by A1;
    hence f"{f.x} = {x} by FINSEQ_4:3;
   end;
   assume
A2:  for x being set st x in dom f holds f"{f.x} = {x};
   let x be set;
   assume
A3:  x in dom f;
   then f"{f.x} = {x} by A2;
   hence f is_one-to-one_at x by A3,FINSEQ_4:3;
  end;
  hence thesis by FINSEQ_4:5;
 end;

theorem
     for f being Function, y1,y2 being set
    st f is one-to-one & y1 in rng f & y2 in rng f & f"{y1} = f"{y2}
   holds y1 = y2
 proof let f be Function, y1,y2 be set such that
A1:  f is one-to-one and
A2:  y1 in rng f and
A3:  y2 in rng f and
A4:  f"{y1} = f"{y2};
   consider x1 being set such that
A5:  f"{y1} = {x1} by A1,A2,FUNCT_1:144;
   consider x2 being set such that
A6:  f"{y2} = {x2} by A1,A3,FUNCT_1:144;
    f.x1 = y1 & f.x2 = y2 by A5,A6,Th3;
   hence thesis by A4,A5,A6,ZFMISC_1:6;
 end;

definition let x be set;
 cluster <*x*> -> non empty;
  coherence
 proof <*x*> = { [1,x] } by FINSEQ_1:52; hence thesis; end;
end;

definition
 cluster empty -> trivial set;
  coherence by REALSET1:def 12;
end;

definition let x be set;
 cluster <*x*> -> trivial;
  coherence
 proof len <*x*> = 1 by FINSEQ_1:56;
  hence thesis by SPPOL_1:2;
 end;

 let y be set;
 cluster <*x,y*> -> non trivial;
  coherence
 proof len <*x,y*> = 2 by FINSEQ_1:61;
  hence thesis by SPPOL_1:2;
 end;
end;

definition
 cluster one-to-one non empty FinSequence;
  existence
 proof consider x being set;
  set f = <*x*>;
    f is non empty & f is one-to-one by FINSEQ_3:102;
  hence thesis;
 end;
end;

theorem Th6:
   for f being non empty FinSequence holds 1 in dom f & len f in dom f
 proof let f be non empty FinSequence;
    len f <> 0 by FINSEQ_1:25;
then A1: len f >= 1 by RLVECT_1:99;
   hence 1 in dom f by FINSEQ_3:27;
   thus len f in dom f by A1,FINSEQ_3:27;
 end;

theorem
     for f being non empty FinSequence ex i st i+1 = len f
 proof let f be non empty FinSequence;
    len f <> 0 by FINSEQ_1:25;
  hence thesis by NAT_1:22;
 end;

theorem Th8:
  for x being set, f being FinSequence holds len(<*x*>^f) = 1 + len f
 proof let x be set, f be FinSequence;
  thus len(<*x*>^f) = len <*x*> + len f by FINSEQ_1:35
                   .= 1 + len f by FINSEQ_1:56;
 end;

scheme domSeqLambda{A()->Nat,F(set) -> set}:
   ex p being FinSequence st len p = A() & for k st k in dom p holds p.k=F(k)
 proof
  deffunc G(Nat) = F($1);
  consider p being FinSequence such that
A1:   len p = A() and
A2:   for k st k in Seg A() holds p.k=G(k) from SeqLambda;
  take p;
  thus len p = A() by A1;
  let k;
  assume k in dom p;
  then k in Seg A() by A1,FINSEQ_1:def 3;
  hence thesis by A2;
 end;

canceled;

theorem
     for f being FinSequence, p,q being set
     st p in rng f & q in rng f & p..f = q..f
    holds p = q
 proof let f be FinSequence, p,q be set such that
A1:  p in rng f and
A2:  q in rng f;
  assume p..f = q..f;
  hence p = f.(q..f) by A1,FINSEQ_4:29 .= q by A2,FINSEQ_4:29;
 end;

theorem Th11:
  for f,g being FinSequence st n+1 in dom f & g = f|Seg n holds
    f|Seg(n+1) = g^<*f.(n+1)*>
 proof let f,g be FinSequence such that
A1: n+1 in dom f and
A2: g = f|Seg n;
  reconsider h = f|Seg(n+1) as FinSequence by FINSEQ_1:19;
    n+1 in Seg(n+1) by FINSEQ_1:6;
then A3: h.(n+1) = f.(n+1) by FUNCT_1:72;
    n <= n+1 by NAT_1:29;
  then Seg n c= Seg(n+1) by FINSEQ_1:7;
then A4: g = h|Seg n by A2,FUNCT_1:82;
    n+1 <= len f by A1,FINSEQ_3:27;
  then len h = n+1 by FINSEQ_1:21;
  hence f|Seg(n+1) = g^<*f.(n+1)*> by A3,A4,FINSEQ_3:61;
 end;

theorem Th12:
   for f being one-to-one FinSequence st i in dom f holds (f.i)..f = i
 proof let f be one-to-one FinSequence; assume
A1:  i in dom f;
  then f.i in rng f by FUNCT_1:def 5;
then A2:  f just_once_values f.i by FINSEQ_4:10;
  then f <- (f.i) = (f.i)..f by FINSEQ_4:35;
  hence (f.i)..f = i by A1,A2,FINSEQ_4:def 3;
 end;

reserve D for non empty set, p for Element of D, f,g for FinSequence of D;

definition let D be non empty set;
 cluster one-to-one non empty FinSequence of D;
  existence
 proof consider x being Element of D;
  set f = <*x*>;
    f is non empty & f is one-to-one by FINSEQ_3:102;
  hence thesis;
 end;
end;

:: FINSEQ_1:17

theorem
     dom f = dom g & (for i st i in dom f holds f/.i = g/.i) implies f = g
 proof assume that
A1: dom f = dom g and
A2: for i st i in dom f holds f/.i = g/.i;
    now let k; assume
A3:  k in dom f;
   hence f.k = f/.k by FINSEQ_4:def 4
            .= g/.k by A2,A3
            .= g.k by A1,A3,FINSEQ_4:def 4;
  end;
  hence thesis by A1,FINSEQ_1:17;
 end;

:: FINSEQ_1:18

theorem Th14:
 len f = len g & (for k st 1 <= k & k <= len f holds f/.k = g/.k)
  implies f = g
 proof assume that
A1: len f = len g and
A2: for k st 1 <= k & k <= len f holds f/.k = g/.k;
    now let k; assume
A3: 1 <= k & k <= len f;
   hence f.k = f/.k by FINSEQ_4:24
            .= g/.k by A2,A3
            .= g.k by A1,A3,FINSEQ_4:24;
  end;
  hence thesis by A1,FINSEQ_1:18;
 end;

theorem Th15:
  len f = 1 implies f = <*f/.1*>
 proof
  assume
A1: len f = 1;
  then f is non empty by FINSEQ_1:25;
  then 1 in dom f by Th6;
  then f.1 = f/.1 by FINSEQ_4:def 4;
  hence thesis by A1,FINSEQ_1:57;
 end;

theorem Th16:
 for D being non empty set, p being Element of D,
     f being FinSequence of D holds
   (<*p*>^f)/.1 = p
 proof let D be non empty set, p be Element of D, f be FinSequence of D;
    len(<*p*>^f) = 1 + len f by Th8;
  then 1 <= 1 & 1 <= len(<*p*>^f) by NAT_1:29;
  then 1 in dom(<*p*>^f) by FINSEQ_3:27;
  then (<*p*>^f)/.1 = (<*p*>^f).1 by FINSEQ_4:def 4;
  hence thesis by FINSEQ_1:58;
 end;

:: FINSEQ_1:def 7
 Lm1:
   i in dom f implies (f^g)/.i=f/.i
 proof assume
A1: i in dom f;
    dom f c= dom(f^g) by FINSEQ_1:39;
  hence (f^g)/.i = (f^g).i by A1,FINSEQ_4:def 4
                .= f.i by A1,FINSEQ_1:def 7
                .= f/.i by A1,FINSEQ_4:def 4;
 end;

canceled;

theorem Th18:
 for D being set, f being FinSequence of D holds
   len(f|i) <= len f
 proof let D be set, f be FinSequence of D;
    i <= len f implies len(f|i) = i by TOPREAL1:3;
  hence thesis by TOPREAL1:2;
 end;

theorem Th19:
 for D being set, f being FinSequence of D holds
   len(f|i) <= i
 proof let D be set, f be FinSequence of D;
    i <= len f implies len(f|i) = i by TOPREAL1:3;
  hence thesis by TOPREAL1:2;
 end;

theorem Th20:
 for D being set, f being FinSequence of D holds
   dom(f|i) c= dom f
 proof let D be set, f be FinSequence of D;
  let j be set;
  assume
A1:  j in dom(f|i);
  then reconsider j as Nat;
A2: len(f|i) <= len f by Th18;
    j <= len (f|i) by A1,FINSEQ_3:27;
then A3: j <= len f by A2,AXIOMS:22;
    1 <= j by A1,FINSEQ_3:27;
  hence thesis by A3,FINSEQ_3:27;
 end;

theorem Th21:
   rng(f|i) c= rng f
 proof
  let p be set;
  assume p in rng(f|i);
  then consider j being Nat such that
A1:  j in dom(f|i) and
A2:  (f|i)/.j = p by PARTFUN2:4;
    dom(f|i) c= dom f by Th20;
  then f/.j in rng f by A1,PARTFUN2:4;
  hence p in rng f by A1,A2,TOPREAL1:1;
 end;

canceled;

theorem Th23:
  for D being set, f being FinSequence of D holds
   f is non empty implies f|1 = <*f/.1*>
 proof 
  let D be set, f be FinSequence of D;  
  assume f is non empty;
  then 1 in dom f by Th6;
  then 1 <= len f by FINSEQ_3:27;
then A1:  len(f|1) = 1 by TOPREAL1:3;
then A2:  1 in dom(f|1) by FINSEQ_3:27;
then A3:  (f|1)/.1 = (f|1).1 by FINSEQ_4:def 4;
    f/.1 = (f|1)/.1 by A2,TOPREAL1:1;
  hence thesis by A1,A3,FINSEQ_1:57;
 end;

theorem
     i+1 = len f implies f = (f|i)^<*f/.len f*>
 proof
  assume
A1: i+1 = len f;
  then f is non empty by FINSEQ_1:25;
then A2: i+1 in dom f by A1,Th6;
A3: f|i = f|Seg i by TOPREAL1:def 1;
    dom f = Seg(i+1) by A1,FINSEQ_1:def 3;
  hence f = f|Seg(i+1) by RELAT_1:97
         .= (f|i)^<*f.(i+1)*> by A2,A3,Th11
         .= (f|i)^<*f/.len f*> by A1,A2,FINSEQ_4:def 4;
 end;

Lm2:
   f is one-to-one implies f|i is one-to-one
 proof assume
A1: f is one-to-one;
    now let n,m such that
A2:  n in dom(f|i) and
A3:  m in dom(f|i) and
A4:  (f|i)/.n = (f|i)/.m;
   A5: dom(f|i) c= dom f by Th20;
     f/.n = (f|i)/.n by A2,TOPREAL1:1 .= f/.m by A3,A4,TOPREAL1:1;
   hence n = m by A1,A2,A3,A5,PARTFUN2:17;
  end;
  hence thesis by PARTFUN2:16;
 end;

definition let i,D; let f be one-to-one FinSequence of D;
 cluster f|i -> one-to-one;
   coherence by Lm2;
end;

theorem Th25:
 for D being set, f, g being FinSequence of D holds
   i <= len f implies (f^g)|i = f|i
 proof
   let D be set, f, g be FinSequence of D;
   assume
A1:  i <= len f;
then A2:  len(f|i) = i by TOPREAL1:3;
     i <= len f+len g by A1,NAT_1:37;
   then i <= len(f^g) by FINSEQ_1:35;
then A3:  len((f^g)|i) = i by TOPREAL1:3;
     now let j;
    assume
A4:  j in Seg i;
    then j <= i by FINSEQ_1:3;
    then 1 <= j & j <= len f by A1,A4,AXIOMS:22,FINSEQ_1:3;
  then j in Seg len f by FINSEQ_1:3;
then A5:  j in dom f by FINSEQ_1:def 3;
    thus ((f^g)|i).j = ((f^g)|(Seg i)).j by TOPREAL1:def 1
                    .= (f^g).j by A4,FUNCT_1:72
                    .= f.j by A5,FINSEQ_1:def 7
                    .= (f|(Seg i)).j by A4,FUNCT_1:72
                    .= (f|i).j by TOPREAL1:def 1;
   end;
   hence (f^g)|i = f|i by A2,A3,FINSEQ_2:10;
 end;

theorem
   for D being set, f, g being FinSequence of D holds
   (f^g)|(len f) = f
 proof
  let D be set, f, g be FinSequence of D;
    f|len f = f|(Seg len f) by TOPREAL1:def 1;
  hence f = f|len f by FINSEQ_2:23 .= (f^g)|(len f) by Th25;
 end;

theorem
   for D being set, f being FinSequence of D holds
  p in rng f implies (f-|p)^<*p*> = f|(p..f)
 proof let D be set, f be FinSequence of D;
  assume
A1:  p in rng f;
  then consider n such that
A2:  n = p..f - 1 and
A3:  f-|p = f | Seg n by FINSEQ_4:def 6;
A4:  n+1 = p..f by A2,XCMPLX_1:27;
  then n+1 in dom f & f.(n+1) = p by A1,FINSEQ_4:29,30;
  hence (f-|p)^<*p*> = f|Seg(n+1) by A3,Th11
                    .= f|(p..f) by A4,TOPREAL1:def 1;
 end;

theorem
     len(f/^i) <= len f
 proof
  per cases;
  suppose
    i <= len f;
   then len(f/^i) = len f - i by RFINSEQ:def 2;
   then len(f/^i)+i = len f by XCMPLX_1:27;
   hence thesis by NAT_1:29;
  suppose len f < i;
   then f/^i = <*>D by RFINSEQ:def 2;
   then len(f/^i) = 0 by FINSEQ_1:32;
   hence thesis by NAT_1:18;
 end;

theorem Th29:
   i in dom(f/^n) implies n+i in dom f
 proof assume
A1: i in dom(f/^n);
  per cases;
   suppose
A2:  n <= len f;
A3:  1 <= i by A1,FINSEQ_3:27;
      i <= i+n by NAT_1:29;
then A4:  1 <= i+n by A3,AXIOMS:22;
      i <= len(f/^n) by A1,FINSEQ_3:27;
    then i <= len f - n by A2,RFINSEQ:def 2;
    then n+i <= len f by REAL_1:84;
    hence n+i in dom f by A4,FINSEQ_3:27;
   suppose n > len f;
    then f/^n = <*>D by RFINSEQ:def 2;
    hence thesis by A1,FINSEQ_1:26;
 end;

theorem Th30:
   i in dom(f/^n) implies (f/^n)/.i = f/.(n+i)
 proof assume
A1: i in dom(f/^n);
  per cases;
   suppose
A2:  n <= len f;
A3:  n+i in dom f by A1,Th29;
    thus (f/^n)/.i = (f/^n).i by A1,FINSEQ_4:def 4
                  .= f.(n+i) by A1,A2,RFINSEQ:def 2
                  .= f/.(n+i) by A3,FINSEQ_4:def 4;
   suppose n > len f;
    then f/^n = <*>D by RFINSEQ:def 2;
    hence thesis by A1,FINSEQ_1:26;
 end;

theorem Th31:
   f/^0 = f
 proof
A1: 0 <= len f by NAT_1:18;
then A2: len(f/^0) = len f - 0 by RFINSEQ:def 2
             .= len f;
    now
   let i;
   assume 1 <= i & i <= len(f/^0);
   then i in dom(f/^0) by FINSEQ_3:27;
   hence (f/^0).i = f.(i+0) by A1,RFINSEQ:def 2
                 .= f.i;
  end;
  hence thesis by A2,FINSEQ_1:18;
 end;

theorem
     f is non empty implies f = <*f/.1*>^(f/^1)
 proof assume f is non empty;
  then f|1 = <*f/.1*> by Th23;
  hence thesis by RFINSEQ:21;
 end;

theorem
     i+1 = len f implies f/^i = <*f/.len f*>
 proof assume
A1: i+1 = len f;
  then i <= len f by NAT_1:29;
then A2:  len(f/^i) = len f - i by RFINSEQ:def 2
              .= 1 by A1,XCMPLX_1:26;
   then A3:  1 in dom(f/^i) by FINSEQ_3:27;
  thus f/^i = <*(f/^i)/.1*> by A2,Th15
           .= <*f/.len f*> by A1,A3,Th30;
 end;

theorem Th34:
   j+1 = i & i in dom f implies <*f/.i*>^(f/^i) = f/^j
 proof assume that
A1: j+1 = i and
A2: i in dom f;
  set g = <*f/.i*>^(f/^i);
A3: i <= len f by A2,FINSEQ_3:27;
      j <= i by A1,NAT_1:29;
then A4: j <= len f by A3,AXIOMS:22;
A5: len g = len(f/^i) + 1 by Th8;
then A6: len g = len f - i + 1 by A3,RFINSEQ:def 2
         .= len f - j - 1 + 1 by A1,XCMPLX_1:36
         .= len f - j by XCMPLX_1:27
         .= len(f/^j) by A4,RFINSEQ:def 2;
    now let k;
   assume that
A7: 1 <= k and
A8: k <= len g;
A9: k in dom(f/^j) by A6,A7,A8,FINSEQ_3:27;
   per cases;
   suppose
A10:   k = 1;
    hence g.k = f/.i by FINSEQ_1:58
             .= f.i by A2,FINSEQ_4:def 4
             .= (f/^j).k by A1,A4,A9,A10,RFINSEQ:def 2;
   suppose
     k <> 1;
then A11:   1 < k by A7,REAL_1:def 5;
    reconsider k' = k-1 as Nat by A7,INT_1:18;
       k'+1 = k by XCMPLX_1:27;
then A12:  1 <= k' by A11,NAT_1:38;
      k' <= len g - 1 by A8,REAL_1:49;
    then k' <= len(f/^i) by A5,XCMPLX_1:26;
then A13:   k' in dom(f/^i) by A12,FINSEQ_3:27;
      len <*f/.i*> = 1 by FINSEQ_1:56;
    hence g.k = (f/^i).k' by A8,A11,FINSEQ_1:37
             .= f.(k'+i) by A3,A13,RFINSEQ:def 2
             .= f.(k'+1+j) by A1,XCMPLX_1:1
             .= f.(k+j) by XCMPLX_1:27
             .= (f/^j).k by A4,A9,RFINSEQ:def 2;
  end;
  hence <*f/.i*>^(f/^i) = f/^j by A6,FINSEQ_1:18;
 end;

theorem Th35:
 for D being set, f being FinSequence of D holds
   len f <= i implies f/^i is empty
 proof
 let D be set, f be FinSequence of D;
  assume
A1: len f <= i;
  per cases;
   suppose len f = i;
     then len(f/^i) = len f - len f by RFINSEQ:def 2
                   .= 0 by XCMPLX_1:14;
    hence thesis by FINSEQ_1:25;
   suppose len f <> i;
    then len f < i by A1,REAL_1:def 5;
    then f/^i = <*>D by RFINSEQ:def 2;
    hence thesis;
 end;

theorem Th36:
   rng(f/^n) c= rng f
 proof
  let p be set;
  assume p in rng(f/^n);
  then consider j being Nat such that
A1:  j in dom(f/^n) and
A2:  (f/^n)/.j = p by PARTFUN2:4;
    j+n in dom f by A1,Th29;
  then f/.(j+n) in rng f by PARTFUN2:4;
  hence p in rng f by A1,A2,Th30;
 end;

Lm3:
   f is one-to-one implies f/^i is one-to-one
 proof assume
A1: f is one-to-one;
    now let n,m such that
A2:  n in dom(f/^i) and
A3:  m in dom(f/^i) and
A4:  (f/^i)/.n = (f/^i)/.m;
A5: i+n in dom f & i+m in dom f by A2,A3,Th29;
     f/.(i+n) = (f/^i)/.n by A2,Th30 .= f/.(i+m) by A3,A4,Th30;
   then i+n = i+m by A1,A5,PARTFUN2:17;
   hence n = m by XCMPLX_1:2;
  end;
  hence thesis by PARTFUN2:16;
 end;

definition let i,D; let f be one-to-one FinSequence of D;
 cluster f/^i -> one-to-one;
  coherence by Lm3;
end;

theorem Th37:
   f is one-to-one implies rng(f|n) misses rng(f/^n)
 proof assume
A1: f is one-to-one;
  assume rng(f|n) meets rng(f/^n);
  then consider x being set such that
A2: x in rng(f|n) and
A3: x in rng(f/^n) by XBOOLE_0:3;
  consider i such that
A4:  i in dom(f|n) and
A5:  (f|n)/.i = x by A2,PARTFUN2:4;
  consider j such that
A6:  j in dom(f/^n) and
A7:  (f/^n)/.j = x by A3,PARTFUN2:4;
   A8: dom(f|n) c= dom f by Th20;
A9:  j+n in dom f by A6,Th29;
A10:  f/.(j+n) = (f/^n)/.j by A6,Th30
             .= f/.i by A4,A5,A7,TOPREAL1:1;
    now assume
A11: i = j+n;
A12: i <= len(f|n) by A4,FINSEQ_3:27;
     len(f|n) <= n by Th19;
then A13: i <= n by A12,AXIOMS:22;
     n <= i by A11,NAT_1:29;
   then i = n by A13,AXIOMS:21;
 then j = n-n by A11,XCMPLX_1:26
     .= 0 by XCMPLX_1:14;
   hence contradiction by A6,FINSEQ_3:27;
  end;
  hence contradiction by A1,A4,A8,A9,A10,PARTFUN2:17;
 end;

theorem
     p in rng f implies f |-- p = f/^(p..f)
 proof assume
A1:  p in rng f;
then A2:  len (f|--p) = len f - p..f by FINSEQ_4:def 7;
A3:  p..f <= len f by A1,FINSEQ_4:31;
then A4:  len (f/^(p..f)) = len f - p..f by RFINSEQ:def 2;
A5:  Seg len (f|--p) = dom (f|--p) & Seg len (f/^(p..f)) = dom (f/^(p..f))
      by FINSEQ_1:def 3;
    now let i;
   assume
A6:  i in dom (f|--p);
   hence (f|--p).i = f.(i + p..f) by A1,FINSEQ_4:def 7
                 .= (f/^(p..f)).i by A2,A3,A4,A5,A6,RFINSEQ:def 2;
  end;
  hence thesis by A2,A4,A5,FINSEQ_2:10;
 end;

theorem Th39:
   (f^g)/^(len f + i) = g/^i
 proof
A1:  len(f^g) = len f + len g by FINSEQ_1:35;
  per cases;
   suppose
A2:  i <= len g;
  then len f + i <= len f + len g by AXIOMS:24;
then A3:  len((f^g)/^(len f + i)) = len g + len f - (len f + i) by A1,RFINSEQ:
def 2
                            .= len g + len f - len f - i by XCMPLX_1:36
                            .= len g - i by XCMPLX_1:26
                            .= len(g/^i) by A2,RFINSEQ:def 2;
      now let k;
     assume
A4:    1 <= k & k <= len(g/^i);
then A5:    k in dom(g/^i) by FINSEQ_3:27;
then A6:    i+k in dom g by Th29;
       k in dom((f^g)/^(len f + i)) by A3,A4,FINSEQ_3:27;
     hence ((f^g)/^(len f + i))/.k = (f^g)/.(len f + i + k) by Th30
                                  .= (f^g)/.(len f + (i+k)) by XCMPLX_1:1
                                  .= g/.(i+k) by A6,GROUP_5:96
                                  .= (g/^i)/.k by A5,Th30;
    end;
    hence (f^g)/^(len f + i) = g/^i by A3,Th14;
   suppose
A7:  i > len g;
    then len f + i > len(f^g) by A1,REAL_1:53;
    hence (f^g)/^(len f+i) = <*>D by RFINSEQ:def 2
                          .= g/^i by A7,RFINSEQ:def 2;
 end;

theorem
     (f^g)/^(len f) = g
 proof
  thus (f^g)/^(len f) = (f^g)/^(len f + 0)
                     .= g/^0 by Th39
                     .= g by Th31;
 end;

theorem Th41:
   p in rng f implies f/.(p..f) = p
 proof assume p in rng f;
  then p..f in dom f & f.(p..f) = p by FINSEQ_4:29,30;
  hence thesis by FINSEQ_4:def 4;
 end;

theorem Th42:
   i in dom f implies f/.i..f <= i
 proof assume that
A1:  i in dom f;
  set p = f/.i;
A2:  p..f = Sgm(f"{p}).1 by FINSEQ_4:def 5;
    f"{p} c= dom f by RELAT_1:167;
then A3:  f"{p} c= Seg len f by FINSEQ_1:def 3;
    f/.i = f.i by A1,FINSEQ_4:def 4;
  then f.i in {p} by TARSKI:def 1;
  then i in f"{p} by A1,FUNCT_1:def 13;
  then i in rng Sgm(f"{p}) by A3,FINSEQ_1:def 13;
  then consider l being set such that
A4: l in dom Sgm(f"{p}) and
A5: Sgm(f"{p}).l = i by FUNCT_1:def 5;
  reconsider l as Nat by A4;
      1 <= l & l <= len(Sgm(f"{p})) by A4,FINSEQ_3:27;
  hence p..f <= i by A2,A3,A5,FINSEQ_3:46;
 end;

theorem
     p in rng(f|i) implies p..(f|i) = p..f
 proof assume
A1: p in rng(f|i);
then A2: p..(f|i) in dom(f|i) by FINSEQ_4:30;
   A3: dom(f|i) c= dom f by Th20;
  A4: rng(f|i) c= rng f by Th21;
    f/.(p..(f|i)) = (f|i)/.(p..(f|i)) by A2,TOPREAL1:1
               .= p by A1,Th41;
  then A5: p..f <= p..(f|i) by A2,A3,Th42;
A6: 1 <= p..f by A1,A4,FINSEQ_4:31;
    p..(f|i) <= len(f|i) by A1,FINSEQ_4:31;
  then p..f <= len(f|i) by A5,AXIOMS:22;
then A7:  p..f in dom(f|i) by A6,FINSEQ_3:27;
  then (f|i)/.(p..f) = f/.(p..f) by TOPREAL1:1
                  .= p by A1,A4,Th41;
  then p..(f|i) <= p..f by A7,Th42;
  hence thesis by A5,AXIOMS:21;
 end;

theorem
     i in dom f & f is one-to-one implies f/.i..f = i
 proof
  assume
A1: i in dom f;
  assume f is one-to-one;
  then (f.i)..f = i by A1,Th12;
  hence thesis by A1,FINSEQ_4:def 4;
 end;

definition let D, f; let p be set;
 func f-:p -> FinSequence of D equals
:Def1:  f|(p..f);
  correctness;
end;

theorem Th45:
   p in rng f implies len(f-:p) = p..f
 proof
  assume
    p in rng f;
  then p..f in dom f by FINSEQ_4:30;
then A1:  p..f <= len f by FINSEQ_3:27;
    f-:p = f|(p..f) by Def1;
  hence thesis by A1,TOPREAL1:3;
 end;

theorem Th46:
   p in rng f & i in Seg(p..f) implies (f-:p)/.i = f/.i
 proof assume that
A1:  p in rng f and
A2:  i in Seg(p..f);
A3:  p..f in dom f by A1,FINSEQ_4:30;
  thus (f-:p)/.i = (f|(p..f))/.i by Def1 .= f/.i by A2,A3,GOBOARD1:10;
 end;

theorem
     p in rng f implies (f-:p)/.1 = f/.1
 proof assume
A1:  p in rng f;
  then 1 <= p..f by FINSEQ_4:31;
  then 1 in Seg(p..f) by FINSEQ_1:3;
  hence (f-:p)/.1 = f/.1 by A1,Th46;
 end;

theorem
     p in rng f implies (f-:p)/.(p..f) = p
 proof
  assume
A1:  p in rng f;
  then 1 <= p..f & p..f <= p..f by FINSEQ_4:31;
then A2:  p..f in Seg(p..f) by FINSEQ_1:3;
A3:  p..f in dom f by A1,FINSEQ_4:30;
  thus (f-:p)/.(p..f) = f/.(p..f) by A1,A2,Th46
                   .= f.(p..f) by A3,FINSEQ_4:def 4
                   .= p by A1,FINSEQ_4:29;
 end;

theorem
   for x being set holds
   x in rng f & p in rng f & x..f<=p..f implies x in rng(f-:p)
 proof
  let x be set; assume that
A1:  x in rng f and
A2:  p in rng f and
A3:  x..f<=p..f;
  set g = f-:p, i = x..f;
A4:  i in dom f by A1,FINSEQ_4:30;
    1 <= i by A1,FINSEQ_4:31;
then A5:  i in Seg (p..f) by A3,FINSEQ_1:3;
    Seg len g = dom g by FINSEQ_1:def 3;
then A6:  i in dom g by A2,A5,Th45;
  then g.i in rng g by FUNCT_1:def 5;
  then g/.i in rng g by A6,FINSEQ_4:def 4;
  then f/.i in rng g by A2,A5,Th46;
  then f.i in rng g by A4,FINSEQ_4:def 4;
  hence thesis by A1,FINSEQ_4:29;
 end;

theorem
     p in rng f implies f-:p is non empty
 proof
  assume
A1: p in rng f;
  then 1 <= p..f by FINSEQ_4:31;
  then 1 <= len(f-:p) by A1,Th45;
  hence thesis by FINSEQ_3:27,RELAT_1:60;
 end;

theorem
     rng(f-:p) c= rng f
 proof f-:p = f|(p..f) by Def1;
  hence thesis by Th21;
 end;

definition let D,p; let f be one-to-one FinSequence of D;
 cluster f-:p -> one-to-one;
  coherence
 proof f-:p = f|(p..f) by Def1;
  hence thesis;
 end;
end;

definition let D, f, p;
 func f:-p -> FinSequence of D equals
:Def2:  <*p*>^(f/^p..f);
 correctness;
end;

theorem Th52:
  p in rng f implies ex i st i+1 = p..f & f:-p = f/^i
 proof assume
A1:  p in rng f;
  then 1 <= p..f by FINSEQ_4:31;
  then reconsider i = p..f - 1 as Nat by INT_1:18;
  take i;
  thus
A2:  i+1 = p..f by XCMPLX_1:27;
A3:  p..f in dom f by A1,FINSEQ_4:30;
  thus f:-p = <*p*>^(f/^p..f) by Def2
           .= <*f/.(p..f)*>^(f/^p..f) by A1,Th41
           .= f/^i by A2,A3,Th34;
 end;

theorem Th53:
   p in rng f implies len (f:-p) = len f - p..f + 1
 proof
  assume
A1:  p in rng f;
  then consider i such that
A2:  i+1 = p..f and
A3:  f:-p = f/^i by Th52;
    i <= p..f & p..f <= len f by A1,A2,FINSEQ_4:31,NAT_1:29;
  then i <= len f by AXIOMS:22;
  hence len(f:-p) = len f - i by A3,RFINSEQ:def 2
                 .= len f - (p..f - 1) by A2,XCMPLX_1:26
                 .= len f - p..f + 1 by XCMPLX_1:37;
 end;

theorem Th54:
  p in rng f & j+1 in dom(f:-p) implies j+p..f in dom f
 proof assume that
A1:  p in rng f and
A2:  j+1 in dom(f:-p);
    j+1 <= len(f:-p) by A2,FINSEQ_3:27;
  then j+1 <= len f - p..f + 1 by A1,Th53;
  then j <= len f - p..f by REAL_1:53;
then A3: j+p..f <= len f by REAL_1:84;
    1 <= p..f & p..f <= j+p..f by A1,FINSEQ_4:31,NAT_1:29;
  then 1 <= j+p..f by AXIOMS:22;
  hence j+p..f in dom f by A3,FINSEQ_3:27;
 end;

Lm4:
   f:-p is non empty
 proof f:-p = <*p*>^(f/^p..f) by Def2;
  then len(f:-p) = 1 + len(f/^p..f) by Th8;
  hence thesis by FINSEQ_1:25;
 end;

definition let D,p,f;
 cluster f:-p -> non empty;
  coherence by Lm4;
end;

theorem Th55:
   p in rng f & j+1 in dom(f:-p) implies (f:-p)/.(j+1) = f/.(j+p..f)
 proof assume that
A1:  p in rng f and
A2:  j+1 in dom(f:-p);
  set i = j+1;
  consider k such that
A3:  k+1 = p..f and
A4:  f:-p = f/^k by A1,Th52;
    k <= p..f & p..f <= len f by A1,A3,FINSEQ_4:31,NAT_1:29;
then A5:  k <= len f by AXIOMS:22;
A6:  j+p..f in dom f by A1,A2,Th54;
  thus (f:-p)/.i = (f:-p).i by A2,FINSEQ_4:def 4
                .= f.(i+k) by A2,A4,A5,RFINSEQ:def 2
                .= f.(j+p..f) by A3,XCMPLX_1:1
                .= f/.(j+p..f) by A6,FINSEQ_4:def 4;
 end;

theorem
    (f:-p)/.1 = p
 proof f:-p = <*p*>^(f/^p..f) by Def2;
  hence thesis by Th16;
 end;

theorem
     p in rng f implies (f:-p)/.(len(f:-p)) = f/.len f
 proof assume
A1:  p in rng f;
  then p..f <= len f by FINSEQ_4:31;
  then reconsider j = len f - p..f as Nat by INT_1:18;
A2:  len(f:-p) = j + 1 by A1,Th53;
    len(f:-p) in dom(f:-p) by Th6;
  hence (f:-p)/.(len(f:-p)) = f/.(j+p..f) by A1,A2,Th55
                         .= f/.len f by XCMPLX_1:27;
 end;

theorem
     p in rng f implies rng(f:-p) c= rng f
 proof assume p in rng f;
  then ex i st i+1 = p..f & f:-p = f/^i by Th52;
  hence thesis by Th36;
 end;

theorem
     p in rng f & f is one-to-one implies f:-p is one-to-one
 proof assume p in rng f;
  then ex i st i+1 = p..f & f:-p = f/^i by Th52;
  hence thesis by Lm3;
 end;

definition let f be FinSequence;
 func Rev f -> FinSequence means :Def3:
 len it = len f & for i st i in dom it holds it.i = f.(len f - i + 1);
  existence
  proof
    deffunc F(Nat) = f.(len f - $1 + 1);
    ex p being FinSequence st len p = len f &
    for k st k in dom p holds p.k = F(k) from domSeqLambda;
    hence thesis;
  end;
  uniqueness
 proof let f1,f2 be FinSequence such that
A1: len f1 = len f and
A2: for i st i in dom f1 holds f1.i = f.(len f - i + 1) and
A3: len f2 = len f and
A4: for i st i in dom f2 holds f2.i = f.(len f - i + 1);
A5:  dom f1 = Seg len f1 & dom f2 = Seg len f2 & dom f = Seg len f
      by FINSEQ_1:def 3;
     now let i; assume i in dom f;
    then f1.i = f.(len f - i + 1) & f2.i = f.(len f - i + 1)
     by A1,A2,A3,A4,A5;
    hence f1.i = f2.i;
   end;
  hence thesis by A1,A3,A5,FINSEQ_2:10;
 end;
end;

theorem Th60:
   for f being FinSequence holds dom f = dom Rev f & rng f = rng Rev f
 proof let f be FinSequence;
  thus
A1:  dom f = Seg len f by FINSEQ_1:def 3
            .= Seg len (Rev f) by Def3
            .= dom(Rev f) by FINSEQ_1:def 3;
A2: len f = len(Rev f) by Def3;
  hereby let x be set;
   assume x in rng f;
   then consider i such that
A3: i in dom f and
A4: f.i = x by FINSEQ_2:11;
     i <= len f by A3,FINSEQ_3:27;
   then reconsider j = len f - i + 1 as Nat by Th1;
A5:   len f - j + 1 = len f - (len f - i) - 1 + 1 by XCMPLX_1:36
                   .= len f - (len f - i) by XCMPLX_1:27
                   .= len f - len f + i by XCMPLX_1:37
                   .= 0 + i by XCMPLX_1:14
                   .= i;
     dom f = Seg len f by FINSEQ_1:def 3;
  then j in Seg len (Rev f) by A2,A3,Th2;
then A6:  j in dom(Rev f) by FINSEQ_1:def 3;
   then (Rev f).j = f.(len f - j + 1) by Def3;
   hence x in rng(Rev f) by A4,A5,A6,FUNCT_1:def 5;
  end;
  let x be set;
  assume x in rng(Rev f);
   then consider i such that
A7: i in dom(Rev f) and
A8: (Rev f).i = x by FINSEQ_2:11;
A9: (Rev f).i = f.(len f - i + 1) by A7,Def3;
    i <= len f by A2,A7,FINSEQ_3:27;
  then reconsider j = len f - i + 1 as Nat by Th1;
     i in Seg len(Rev f) by A7,FINSEQ_1:def 3;
   then j in Seg len (Rev f) by A2,Th2;
   then j in dom (Rev f) by FINSEQ_1:def 3;
  hence x in rng f by A1,A8,A9,FUNCT_1:def 5;
 end;

theorem Th61:
  for f being FinSequence st i in dom f holds (Rev f).i = f.(len f - i + 1)
 proof let f be FinSequence;
    dom f = dom(Rev f) by Th60;
  hence thesis by Def3;
 end;

theorem Th62:
  for f being FinSequence, i,j being Nat
    st i in dom f & i+j = len f + 1
  holds j in dom Rev f
 proof let f be FinSequence, i,j be Nat such that
A1: i in dom f and
A2: i+j = len f + 1;
A3: dom f = Seg len f by FINSEQ_1:def 3;
A4: j = len f + 1 - i by A2,XCMPLX_1:26
     .= len f - i + 1 by XCMPLX_1:29;
    dom f = dom Rev f by Th60;
  hence j in dom Rev f by A1,A3,A4,Th2;
 end;

definition let f be empty FinSequence;
 cluster Rev f -> empty;
  coherence
 proof len {} = 0 by FINSEQ_1:25;
  then len (Rev {}) = 0 by Def3;
  hence thesis by FINSEQ_1:25;
 end;
end;

theorem
     for x being set holds Rev <*x*> = <*x*>
 proof let x be set;
  set f = <*x*>;
A1:  len f = 1 by FINSEQ_1:56;
     now let i; assume i in dom f;
    then i in Seg len f by FINSEQ_1:def 3;
then i = 1 by A1,FINSEQ_1:4,TARSKI:def 1;
    hence f.i = f.(len f - i + 1) by A1;
   end;
  hence thesis by Def3;
 end;

theorem
     for x1,x2 being set holds Rev <*x1,x2*> = <*x2,x1*>
 proof let x1,x2 be set;
  set f = <*x1,x2*>, g = <*x2,x1*>;
A1:  len f = 2 & len g = 2 by FINSEQ_1:61;
     now let i; assume i in dom g;
    then A2: i in Seg len f by A1,FINSEQ_1:def 3;
    per cases by A1,A2,FINSEQ_1:4,TARSKI:def 2;
    suppose
A3:   i = 1;
     hence g.i = x2 by FINSEQ_1:61
              .= f.(len f - i + 1) by A1,A3,FINSEQ_1:61;
    suppose
A4:   i = 2;
     hence g.i = x1 by FINSEQ_1:61
              .= f.(len f - i + 1) by A1,A4,FINSEQ_1:61;
   end;
  hence thesis by A1,Def3;
 end;

theorem Th65:
  for f being FinSequence
   holds f.1 = (Rev f).(len f) & f.(len f) = (Rev f).1
 proof let f be FinSequence;
   per cases;
   suppose A1: f is empty;
    then A2:   dom Rev f = {} by Th60,RELAT_1:60;
     thus f.1 = {} by A1,FUNCT_1:def 4,RELAT_1:60 .= (Rev f).(len f) by A2,
FUNCT_1:def 4;
    thus f.(len f) = {} by A1,FUNCT_1:def 4,RELAT_1:60 .= (Rev f).1 by A2,
FUNCT_1:def 4;
   suppose f is non empty;
    then A3: len f <> 0 by FINSEQ_1:25;
  then len f in Seg len f by FINSEQ_1:5;
  then len f in dom f by FINSEQ_1:def 3;
  hence (Rev f).(len f) = f.(len f - len f + 1) by Th61
                     .= f.(0 + 1) by XCMPLX_1:14
                     .= f.1;
    1 >= 1 & len f >= 1 by A3,RLVECT_1:99;
  then 1 in dom f by FINSEQ_3:27;
  hence (Rev f).1 = f.(len f - 1 + 1) by Th61
               .= f.(len f) by XCMPLX_1:27;
 end;

definition let f be one-to-one FinSequence;
 cluster Rev f -> one-to-one;
  coherence
 proof
  set g = Rev f;
  let x1,x2 be set such that
A1:  x1 in dom g & x2 in dom g and
A2:  g.x1 = g.x2;
  reconsider i1 = x1, i2 = x2 as Nat by A1;
A3:  dom g = Seg len g by FINSEQ_1:def 3;
A4:  len g = len f by Def3;
  then i1 <= len f & i2 <= len f by A1,FINSEQ_3:27;
  then reconsider i1' = len f - i1 + 1, i2' = len f - i2 + 1 as Nat by Th1;
    dom f = Seg len f by FINSEQ_1:def 3;
then A5:  i1' in dom f & i2' in dom f by A1,A3,A4,Th2;
    f.i1' = g.x1 by A1,Def3
            .= f.i2' by A1,A2,Def3;
  then i1' = i2' by A5,FUNCT_1:def 8;
  then len f - i1 = len f - i2 by XCMPLX_1:2;
  hence x1 = x2 by XCMPLX_1:20;
 end;
end;

theorem Th66:
  for f being FinSequence, x being set holds Rev(f^<*x*>) = <*x*>^(Rev f)
 proof let f be FinSequence, x be set;
  set n = len f + 1, g = <*x*>;
A1: len (f^g) = n by FINSEQ_2:19;
A2: len(g^(Rev f)) = len g + len (Rev f) by FINSEQ_1:35
                    .= 1 + len (Rev f) by FINSEQ_1:56
                    .= n by Def3;
A3: len(Rev(f^g)) = n by A1,Def3;
    now let i; assume
A4:  i in Seg n;
then A5:  1 <= i & i <= n by FINSEQ_1:3;
A6:  len g = 1 by FINSEQ_1:57;
A7:  i in dom(Rev(f^g)) by A3,A4,FINSEQ_1:def 3;
   per cases by A5,REAL_1:def 5;
   suppose
A8:  i = 1;
      Seg len g = dom g by FINSEQ_1:def 3;
then A9:  1 in dom g by A6,FINSEQ_1:4,TARSKI:def 1;
    thus (Rev(f^g)).i = (f^g).(n-1+1) by A1,A7,A8,Def3
                    .= (f^g).n by XCMPLX_1:27
                    .= x by FINSEQ_1:59
                    .= g.1 by FINSEQ_1:57
                    .= (g^(Rev f)).i by A8,A9,FINSEQ_1:def 7;
   suppose
A10:  i > 1;
    then reconsider j = i-1 as Nat by RLVECT_2:103;
    reconsider k = n - i + 1 as Nat by A5,Th1;
    0 < i by A10,AXIOMS:22;
    then consider l being Nat such that
A11:   i = l + 1 by NAT_1:22;
      l <> 0 by A10,A11;
    then 1 <= l by RLVECT_1:99;
then A12:   1 <= j by A11,XCMPLX_1:26;
      j <= n - 1 by A5,REAL_1:49;
    then j <= len f by XCMPLX_1:26;
then A13:  j in dom f by A12,FINSEQ_3:27;
      i - i <= n - i by A5,REAL_1:49;
    then 0 <= n - i by XCMPLX_1:14;
    then A14:   0 + 1 <= k by AXIOMS:24;
      n < len f + i by A10,REAL_1:67;
    then n - i < len f + i - i by REAL_1:54;
    then n - i < len f by XCMPLX_1:26;
    then k < len f + 1 by REAL_1:53;
    then k <= len f by NAT_1:38;
then A15:   k in dom f by A14,FINSEQ_3:27;
    thus (Rev(f^g)).i = (f^g).(n - i + 1) by A1,A7,Def3
                    .= f.k by A15,FINSEQ_1:def 7
                    .= f.(len f + (1 - i) + 1) by XCMPLX_1:29
                    .= f.(len f - j + 1) by XCMPLX_1:38
                    .= (Rev f).j by A13,Th61
                    .= (g^(Rev f)).i by A2,A5,A6,A10,FINSEQ_1:37;
  end;
  hence thesis by A2,A3,FINSEQ_2:10;
 end;

theorem
     for f,g being FinSequence holds Rev(f^g) = (Rev g)^(Rev f)
 proof let f be FinSequence;
   defpred P[FinSequence] means Rev(f^$1) = (Rev $1)^(Rev f);
A1:  P[{}]
    proof set g = {};
     thus Rev(f^g) = Rev f by FINSEQ_1:47
                 .= (Rev g)^(Rev f) by FINSEQ_1:47;
    end;
A2:  for g being FinSequence, x being set st P[g] holds P[g^<*x*>]
    proof let g be FinSequence, x be set such that
A3:   P[g];
     thus Rev(f^(g^<*x*>)) = Rev(f^g^<*x*>) by FINSEQ_1:45
                          .= <*x*>^((Rev g)^(Rev f)) by A3,Th66
                          .= <*x*>^(Rev g)^(Rev f) by FINSEQ_1:45
                          .= (Rev(g^<*x*>))^(Rev f) by Th66;
    end;
  thus for g being FinSequence holds P[g] from IndSeq(A1,A2);
 end;

definition let D,f;
 redefine func Rev f -> FinSequence of D;
  coherence
 proof set n = len f;
A1: dom f = Seg n by FINSEQ_1:def 3;
    now let i;
   set j = n - i + 1;
   assume i in dom (Rev f);
     then i in Seg len Rev f by FINSEQ_1:def 3;
then A2:  i in Seg n by Def3;
   then i <= n by A1,FINSEQ_3:27;
   then j in Seg n & j is Nat by A2,Th1,Th2;
   then f.j in D by A1,FINSEQ_2:13;
   hence Rev f.i in D by A1,A2,Th61;
  end;
  hence thesis by FINSEQ_2:14;
 end;
end;

theorem
     f is non empty implies f/.1 = (Rev f)/.len f & f/.len f = (Rev f)/.1
 proof assume
A1: f is non empty;
then A2: 1 in dom f by Th6;
A3: len f in dom f by A1,Th6;
A4: dom f = dom Rev f by Th60;
  thus f/.1 = f.1 by A2,FINSEQ_4:def 4
             .= (Rev f).len f by Th65
             .= (Rev f)/.len f by A3,A4,FINSEQ_4:def 4;
  thus f/.len f = f.(len f) by A3,FINSEQ_4:def 4
                 .= (Rev f).1 by Th65
                 .= (Rev f)/.1 by A2,A4,FINSEQ_4:def 4;
 end;

theorem
     i in dom f & i+j = len f + 1 implies f/.i = (Rev f)/.j
 proof assume that
A1: i in dom f and
A2: i+j = len f + 1;
A3: i = len f + 1 - j by A2,XCMPLX_1:26
     .= len f - j + 1 by XCMPLX_1:29;
A4: j in dom Rev f by A1,A2,Th62;
  thus f/.i = f.i by A1,FINSEQ_4:def 4
             .= (Rev f).j by A3,A4,Def3
             .= (Rev f)/.j by A4,FINSEQ_4:def 4;
 end;

definition let D,f,p,n;
  func Ins(f,n,p) -> FinSequence of D equals
:Def4:  (f|n)^<*p*>^(f/^n);
   correctness;
end;

theorem
     Ins(f,0,p) = <*p*>^f
 proof
  thus Ins(f,0,p) = (f|0)^<*p*>^(f/^0) by Def4
                 .= <*p*>^(f/^0) by FINSEQ_1:47
                 .= <*p*>^f by Th31;
 end;

theorem Th71:
   len f <= n implies Ins(f,n,p) = f^<*p*>
 proof assume
A1: len f <= n;
then A2: f/^n is empty by Th35;
  thus Ins(f,n,p) = (f|n)^<*p*>^(f/^n) by Def4
                 .= (f|n)^<*p*> by A2,FINSEQ_1:47
                 .= f^<*p*> by A1,TOPREAL1:2;
 end;

theorem Th72:
   len(Ins(f,n,p)) = len f + 1
 proof
  per cases;
   suppose
A1:  n <= len f;
    thus len Ins(f,n,p)
       = len((f|n)^<*p*>^(f/^n)) by Def4
      .= len((f|n)^<*p*>) + len(f/^n) by FINSEQ_1:35
      .= len((f|n)^<*p*>) + (len f - n) by A1,RFINSEQ:def 2
      .= len(f|n)+len<*p*> + (len f - n) by FINSEQ_1:35
      .= len(f|n)+1+(len f - n) by FINSEQ_1:56
      .= n+1+(len f - n) by A1,TOPREAL1:3
      .= len f - n + n + 1 by XCMPLX_1:1
      .= len f + 1 by XCMPLX_1:27;
   suppose len f < n;
     then Ins(f,n,p) = f^<*p*> by Th71;
    hence thesis by FINSEQ_2:19;
 end;

theorem Th73:
   rng Ins(f,n,p) = {p} \/ rng f
 proof
  thus rng Ins(f,n,p)
     = rng((f|n)^<*p*>^(f/^n)) by Def4
    .= rng((f|n)^<*p*>) \/ rng(f/^n) by FINSEQ_1:44
    .= rng(f|n) \/ rng<*p*> \/ rng(f/^n) by FINSEQ_1:44
    .= rng(f|n) \/ rng(f/^n) \/ rng<*p*> by XBOOLE_1:4
    .= rng((f|n)^(f/^n)) \/ rng<*p*> by FINSEQ_1:44
    .= rng<*p*> \/ rng f by RFINSEQ:21
    .= {p} \/ rng f by FINSEQ_1:55;
 end;

definition let D,f,n,p;
 cluster Ins(f,n,p) -> non empty;
  coherence
 proof
    len(Ins(f,n,p)) = len f + 1 by Th72;
  hence thesis by FINSEQ_1:25;
 end;
end;

theorem
     p in rng Ins(f,n,p)
 proof
    p in {p} by TARSKI:def 1;
  then p in {p} \/ rng f by XBOOLE_0:def 2;
  hence thesis by Th73;
 end;

theorem Th75:
   i in dom(f|n) implies (Ins(f,n,p))/.i = f/.i
 proof assume
A1: i in dom(f|n);
  thus (Ins(f,n,p))/.i = ((f|n)^<*p*>^(f/^n))/.i by Def4
                      .= ((f|n)^(<*p*>^(f/^n)))/.i by FINSEQ_1:45
                      .= (f|n)/.i by A1,Lm1
                      .= f/.i by A1,TOPREAL1:1;
 end;

theorem
     n <= len f implies (Ins(f,n,p))/.(n+1) = p
 proof assume
   n <= len f;
then A1: len(f|n) = n by TOPREAL1:3;
then A2: len((f|n)^<*p*>) = n+1 by FINSEQ_2:19;
     1 <= n+1 by NAT_1:29;
then A3: n+1 in dom((f|n)^<*p*>) by A2,FINSEQ_3:27;
  thus (Ins(f,n,p))/.(n+1) = ((f|n)^<*p*>^(f/^n))/.(n+1) by Def4
                        .= ((f|n)^<*p*>)/.(n+1) by A3,Lm1
                        .= p by A1,TOPREAL4:1;
 end;

theorem
     n+1 <= i & i <= len f implies (Ins(f,n,p))/.(i+1) = f/.i
 proof assume that
A1: n+1 <= i and
A2: i <= len f;
     n <= n+1 by NAT_1:29;
   then n <= i by A1,AXIOMS:22;
then A3: n <= len f by A2,AXIOMS:22;
 then len(f|n) = n by TOPREAL1:3;
then A4: len((f|n)^<*p*>) = n+1 by FINSEQ_2:19;
  reconsider j = i - (n+1) as Nat by A1,INT_1:18;
A5:  n+1+j = i by XCMPLX_1:27;
then A6:  n+1+(j+1) = i+1 by XCMPLX_1:1;
A7:  1 <= j+1 by NAT_1:29;
     n+(j+1) <= len f by A2,A5,XCMPLX_1:1;
   then j+1 <= len f - n by REAL_1:84;
   then j+1 <= len(f/^n) by A3,RFINSEQ:def 2;
then A8:  j+1 in dom(f/^n) by A7,FINSEQ_3:27;
  thus (Ins(f,n,p))/.(i+1) = ((f|n)^<*p*>^(f/^n))/.(i+1) by Def4
                        .= (f/^n)/.(j+1) by A4,A6,A8,GROUP_5:96
                        .= f/.(n+(j+1)) by A8,Th30
                        .= f/.i by A5,XCMPLX_1:1;
 end;

theorem
     1 <= n & f is non empty implies (Ins(f,n,p))/.1 = f/.1
 proof assume that
A1: 1 <= n and
A2: f is non empty;
    len f <> 0 by A2,FINSEQ_1:25;
then A3: 1 <= len f by RLVECT_1:99;
   n <= len f implies len(f|n) = n by TOPREAL1:3;
  then 1 <= len(f|n) by A1,A3,TOPREAL1:2;
  then 1 in dom(f|n) by FINSEQ_3:27;
  hence thesis by Th75;
 end;

theorem
     f is one-to-one & not p in rng f implies Ins(f,n,p) is one-to-one
 proof assume that
A1: f is one-to-one and
A2: not p in rng f;
A3: f|n is one-to-one by A1,Lm2;
A4: <*p*> is one-to-one by FINSEQ_3:102;
    now let x be set;
   assume x in rng<*p*>;
   then x in {p} by FINSEQ_1:55;
then A5:   not x in rng f by A2,TARSKI:def 1;
     rng(f|n) c= rng f by Th21;
   hence not x in rng(f|n) by A5;
  end;
  then rng(f|n) misses rng<*p*> by XBOOLE_0:3;
then A6:  (f|n) ^ <*p*> is one-to-one by A3,A4,FINSEQ_3:98;
A7:  f/^n is one-to-one by A1,Lm3;
    now let x be set;
   assume
A8:  x in rng(f/^n);
     rng(f|n) misses rng(f/^n) by A1,Th37;
then A9:  not x in rng(f|n) by A8,XBOOLE_0:3;
     rng(f/^n) c= rng f by Th36;
   then x in rng f by A8;
   then not x in {p} by A2,TARSKI:def 1;
   then not x in rng<*p*> by FINSEQ_1:55;
   then not x in rng(f|n) \/ rng<*p*> by A9,XBOOLE_0:def 2;
   hence not x in rng((f|n) ^ <*p*>) by FINSEQ_1:44;
  end;
  then rng((f|n) ^ <*p*>) misses rng(f/^n) by XBOOLE_0:3;
  then (f|n) ^ <*p*> ^ (f/^n) is one-to-one by A6,A7,FINSEQ_3:98;
  hence thesis by Def4;
 end;

Back to top