:: Functions and Finite Sequences of Real Numbers
::  by Jaros{\l}aw Kotowicz
::
:: Received March 15, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, REAL_1, FINSEQ_1, RELAT_1, FINSET_1, CLASSES1,
      ORDINAL4, CARD_1, ARYTM_3, FUNCT_2, XBOOLE_0, TARSKI, NAT_1, FUNCT_1,
      ARYTM_1, XXREAL_0, CARD_3, VALUED_0, FUNCOP_1, FUNCT_4, RFINSEQ;
 notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, NUMBERS, RELAT_1, FUNCT_1,
      RELSET_1, FUNCT_2, FINSEQ_1, XCMPLX_0, XREAL_0, ORDINAL1, NAT_1, REAL_1,
      SEQ_1, CLASSES1, SEQM_3, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_4, RVSUM_1,
      XXREAL_0;
 constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, BINOP_2, SEQM_3,
      FINSEQ_4, FINSOP_1, RVSUM_1, SEQ_1, FUNCOP_1, CLASSES1, RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XREAL_0, NAT_1,
      MEMBERED, FINSEQ_1, FUNCOP_1, VALUED_0, CARD_1, INT_1, RELSET_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, SEQM_3, RVSUM_1, FUNCOP_1, CLASSES1, RELAT_1;
 theorems TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, NAT_1, FUNCT_1, FUNCT_2,
      CARD_1, CARD_2, RVSUM_1, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
      XREAL_1, FINSEQ_4, XXREAL_0, FINSOP_1, SEQM_3, FUNCOP_1, FUNCT_4,
      ORDINAL1, XREAL_0, CLASSES1, INT_1;
 schemes NAT_1, FINSEQ_1;

begin

reserve x,y for set,
  n,m for Element of NAT,
  r,s for Real;

registration
  let f be FinSequence, x be set;
  cluster Coim(f,x) -> finite;
  coherence;
end;

theorem Th1:
  for f,g,h be FinSequence holds f,g are_fiberwise_equipotent iff
  f^h, g^h are_fiberwise_equipotent
proof
  let f,g,h be FinSequence;
  thus f,g are_fiberwise_equipotent implies f^h, g^h are_fiberwise_equipotent
  proof
    assume
A1: f,g are_fiberwise_equipotent;
    now
      let y;
      card Coim(f,y) = card Coim(g,y) by A1,CLASSES1:def 9;
      hence card Coim(f^h,y) = card Coim(g,y) + card Coim(h,y) by FINSEQ_3:57
        .= card Coim(g^h,y) by FINSEQ_3:57;
    end;
    hence thesis by CLASSES1:def 9;
  end;
  assume
A2: f^h,g^h are_fiberwise_equipotent;
  now
    let x;
A3: card Coim(f^h,x) = card Coim(f,x)+card Coim(h,x) & card Coim(g^h,x) =
    card Coim(g,x)+card Coim(h,x) by FINSEQ_3:57;
    card Coim(f^h,x) = card Coim(g^h,x) by A2,CLASSES1:def 9;
    hence card Coim(f,x) = card Coim(g,x) by A3;
  end;
  hence thesis by CLASSES1:def 9;
end;

theorem
  for f,g be FinSequence holds f^g, g^f are_fiberwise_equipotent
proof
  let f,g be FinSequence;
  let y;
  thus card Coim(f^g,y) = card(g"{y})+ card(f"{y}) by FINSEQ_3:57
    .= card Coim(g^f,y) by FINSEQ_3:57;
end;

theorem Th3:
  for f,g be FinSequence st f,g are_fiberwise_equipotent holds len
  f = len g & dom f = dom g
proof
  let f,g be FinSequence;
A1: dom f = Seg len f by FINSEQ_1:def 3;
  assume f,g are_fiberwise_equipotent;
  then
A2: card(f"(rng f)) = card(g"(rng f)) & rng f = rng g by CLASSES1:75,78;
A3: Seg len g = dom g by FINSEQ_1:def 3;
  thus len f = card(Seg len f) by FINSEQ_1:57
    .= card(g"(rng g)) by A1,A2,RELAT_1:134
    .= card(Seg len g) by A3,RELAT_1:134
    .= len g by FINSEQ_1:57;
  hence thesis by A1,FINSEQ_1:def 3;
end;

theorem Th4:
  for f,g be FinSequence holds f,g are_fiberwise_equipotent iff ex
  P be Permutation of dom g st f = g*P
proof
  let f,g be FinSequence;
  thus f,g are_fiberwise_equipotent implies ex P be Permutation of dom g st f
  = g*P
  proof
    assume
A1: f,g are_fiberwise_equipotent;
    then dom f = dom g by Th3;
    hence thesis by A1,CLASSES1:80;
  end;
  given P be Permutation of dom g such that
A2: f = g*P;
  dom g = {} implies dom g = {};
  then rng P c= dom g & dom P = dom g by FUNCT_2:def 1,RELAT_1:def 19;
  then dom f = dom g by A2,RELAT_1:27;
  hence thesis by A2,CLASSES1:80;
end;

defpred P[Nat] means for X be finite set,F be Function st card(dom(F|X)) = $1
ex a be FinSequence st F|X, a are_fiberwise_equipotent;

Lm1: P[0]
proof
  let X be finite set, F be Function;
  assume
A1: card(dom(F|X)) = 0;
  take A = {};
  let x;
  dom(F|X) = {} by A1;
  hence card Coim(F|X,x) = card Coim(A,x) by RELAT_1:132,XBOOLE_1:3;
end;

Lm2: for n st P[n] holds P[n+1]
proof
  let n be Element of NAT;
  assume
A1: P[n];
  let X be finite set, F be Function;
  reconsider dx = dom(F|X) as finite set;
  set x = the Element of dx;
  set Y = X\{x}, dy = dom(F|Y);
A2: dy = dom F /\ Y by RELAT_1:61;
A3: dx = dom F /\ X by RELAT_1:61;
A4: dy = dx \ {x}
  proof
    thus dy c= dx \ {x}
    proof
      let y;
      assume
A5:   y in dy;
      then y in X \ {x} by A2,XBOOLE_0:def 4;
      then
A6:   not y in {x} by XBOOLE_0:def 5;
      y in dom F by A2,A5,XBOOLE_0:def 4;
      then y in dx by A2,A3,A5,XBOOLE_0:def 4;
      hence thesis by A6,XBOOLE_0:def 5;
    end;
    let y;
    assume
A7: y in dx \{x};
    then ( not y in {x})& y in X by A3,XBOOLE_0:def 4,def 5;
    then
A8: y in Y by XBOOLE_0:def 5;
    y in dom F by A3,A7,XBOOLE_0:def 4;
    hence thesis by A2,A8,XBOOLE_0:def 4;
  end;
  assume
A9: card dom(F|X) = n+1;
  then {x} c= dx by CARD_1:27,ZFMISC_1:31;
  then card(dom(F|Y)) = card dx - card {x} by A4,CARD_2:44
    .= n+1-1 by A9,CARD_1:30
    .= n;
  then consider a be FinSequence such that
A10: F|Y, a are_fiberwise_equipotent by A1;
  take A = a^<* F.x *>;
  dx <> {} by A9;
  then x in dx;
  then
A11: x in dom F /\ X by RELAT_1:61;
  then x in dom F by XBOOLE_0:def 4;
  then
A12: {x} c= dom F by ZFMISC_1:31;
  x in X by A11,XBOOLE_0:def 4;
  then
A13: {x} c= X by ZFMISC_1:31;
  now
    let y;
A14: Y misses {x} by XBOOLE_1:79;
A15: (F|Y)"{y} \/ (F|{x})"{y} = (Y /\ F"{y}) \/ (F|{x})"{y} by FUNCT_1:70
      .= (Y /\ F"{y}) \/ ({x} /\ F"{y}) by FUNCT_1:70
      .= (Y \/ {x}) /\ F"{y} by XBOOLE_1:23
      .= (X \/ {x}) /\ F"{y} by XBOOLE_1:39
      .= X /\ F"{y} by A13,XBOOLE_1:12
      .= (F|X)"{y} by FUNCT_1:70;
    reconsider FF = <*F.x*>"{y} as finite set;
A16: card Coim(F|Y,y) = card Coim(a,y) by A10,CLASSES1:def 9;
A17: dom(F|{x}) = {x} by A12,RELAT_1:62;
A18: dom<*F.x*> = {1} by FINSEQ_1:2,38;
A19: now
      per cases;
      case
A20:    y = F.x;
A21:    {x} c= (F|{x})"{y}
        proof
          let z be set;
A22:      y in {y} by TARSKI:def 1;
          assume
A23:      z in {x};
          then z = x by TARSKI:def 1;
          then y = (F|{x}).z by A17,A20,A23,FUNCT_1:47;
          hence thesis by A17,A23,A22,FUNCT_1:def 7;
        end;
        (F|{x})"{y} c= {x} by A17,RELAT_1:132;
        then (F|{x})"{y} = {x} by A21,XBOOLE_0:def 10;
        then
A24:    card((F|{x})"{y}) = 1 by CARD_1:30;
A25:    {1} c= <*F.x*>"{y}
        proof
          let z be set;
A26:      y in {y} by TARSKI:def 1;
          assume
A27:      z in {1};
          then z = 1 by TARSKI:def 1;
          then y = <*F.x*>.z by A20,FINSEQ_1:40;
          hence thesis by A18,A27,A26,FUNCT_1:def 7;
        end;
        <*F.x*>"{y} c= {1} by A18,RELAT_1:132;
        then <*F.x*>"{y} = {1} by A25,XBOOLE_0:def 10;
        hence card((F|{x})"{y}) = card FF by A24,CARD_1:30;
      end;
      case
A28:    y <> F.x;
A29:    now
          set z = the Element of <*F.x*>"{y};
          assume
A30:      <*F.x*>"{y} <> {};
          then <*F.x*>.z in {y} by FUNCT_1:def 7;
          then
A31:      <*F.x*>.z = y by TARSKI:def 1;
          z in {1} by A18,A30,FUNCT_1:def 7;
          then z = 1 by TARSKI:def 1;
          hence contradiction by A28,A31,FINSEQ_1:40;
        end;
        now
          set z = the Element of (F|{x})"{y};
          assume
A32:      (F|{x})"{y} <> {};
          then (F|{x}).z in {y} by FUNCT_1:def 7;
          then
A33:      (F|{x}).z = y by TARSKI:def 1;
A34:      z in {x} by A17,A32,FUNCT_1:def 7;
          then z = x by TARSKI:def 1;
          hence contradiction by A17,A28,A34,A33,FUNCT_1:47;
        end;
        hence card((F|{x})"{y}) = card FF by A29;
      end;
    end;
    (F|Y)"{y} /\ (F|{x})"{y} = Y /\ (F"{y}) /\ (F|{x})"{y} by FUNCT_1:70
      .= Y /\ F"{y} /\ ({x} /\ F"{y}) by FUNCT_1:70
      .= F"{y} /\ Y /\ {x} /\ F"{y} by XBOOLE_1:16
      .= F"{y} /\ (Y /\ {x}) /\ F"{y} by XBOOLE_1:16
      .= {} /\ F"{y} by A14,XBOOLE_0:def 7
      .= {};
    hence card Coim(F|X,y) = card((F|Y)"{y}) + card FF - card {} by A15,A19,
CARD_2:45
      .= card Coim(A,y) by A16,FINSEQ_3:57;
  end;
  hence thesis by CLASSES1:def 9;
end;

theorem
  for F be Function, X be finite set ex f be FinSequence st F|X, f
  are_fiberwise_equipotent
proof
  let F be Function, X be finite set;
A1: card(dom(F|X)) = card(dom(F|X));
  for n holds P[n] from NAT_1:sch 1(Lm1,Lm2);
  hence thesis by A1;
end;

definition
  let n be Nat, f be FinSequence;
  func f /^ n -> FinSequence means
  :Def1:
  len it = len f - n & for m be Nat st
  m in dom it holds it.m = f.(m+n) if n<=len f otherwise it = {};
  existence
  proof
    thus n<=len f implies ex p1 be FinSequence st len p1 = len f - n & for m
    be Nat st m in dom p1 holds p1.m = f.(m+n)
    proof
      assume n<=len f;
      then reconsider k = len f - n as Element of NAT by NAT_1:21;
      deffunc F(Nat)=f.($1+n);
      consider p be FinSequence such that
A1:   len p = k & for m be Nat st m in dom p holds p.m = F(m) from
      FINSEQ_1:sch 2;
      take p;
      thus len p = len f - n by A1;
      let m be Nat;
      assume m in dom p;
      hence thesis by A1;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let p1,p2 be FinSequence;
    thus n<=len f & (len p1 = len f - n & for m be Nat st m in dom p1 holds p1
.m = f.(m+n)) & (len p2 = len f - n & for m be Nat st m in dom p2 holds p2.m =
    f.(m+n)) implies p1 = p2
    proof
      assume that
      n<=len f and
A2:   len p1 = len f - n and
A3:   for m be Nat st m in dom p1 holds p1.m = f.(m+n) and
A4:   len p2 = len f - n and
A5:   for m be Nat st m in dom p2 holds p2.m = f.(m+n);
A6:   dom p1 = Seg len p1 & Seg len p2 = dom p2 by FINSEQ_1:def 3;
      now
        let m be Nat;
        assume
A7:     m in dom p1;
        then p1.m = f.(m+n) by A3;
        hence p1.m = p2.m by A2,A4,A5,A6,A7;
      end;
      hence thesis by A2,A4,FINSEQ_2:9;
    end;
    thus thesis;
  end;
  consistency;
end;

definition
  let D be set, n be Nat, f be FinSequence of D;
  redefine func f /^ n -> FinSequence of D;
  coherence
  proof
    set p = f /^ n;
    per cases;
    suppose
A1:   n<=len f;
      then reconsider k = len f - n as Element of NAT by NAT_1:21;
A2:   len p = k by A1,Def1;
      rng p c= rng f
      proof
        let x;
        assume x in rng p;
        then consider m being Nat such that
A3:     m in dom p and
A4:     p.m = x by FINSEQ_2:10;
        m<=len p by A3,FINSEQ_3:25;
        then
A5:     m+n<=len f by A2,XREAL_1:19;
A6:     m<=m+n by NAT_1:11;
        1<=m by A3,FINSEQ_3:25;
        then 1<=m+n by A6,XXREAL_0:2;
        then
A7:     m+n in dom f by A5,FINSEQ_3:25;
        p.m = f.(m+n) by A1,A3,Def1;
        hence thesis by A4,A7,FUNCT_1:def 3;
      end;
      then rng p c= D by XBOOLE_1:1;
      hence thesis by FINSEQ_1:def 4;
    end;
    suppose len f < n;
      then f /^ n = <*>D by Def1;
      hence thesis;
    end;
  end;
end;

Lm3: for n be Nat for D be non empty set, f be FinSequence of D st len f<=n
holds (f|n) = f
proof
  let n be Nat;
  let D be non empty set,f be FinSequence of D;
A1: dom f = Seg len f by FINSEQ_1:def 3;
  assume len f<=n;
  then f|n = f|Seg n & dom f c= Seg n by A1,FINSEQ_1:5,def 15;
  hence thesis by RELAT_1:68;
end;

theorem Th6:
  for D be non empty set, f be FinSequence of D, n,m be Nat holds
  n in dom f & m in Seg n implies (f|n).m = f.m & m in dom f
proof
  let D be non empty set,f be FinSequence of D, n,m be Nat;
  assume that
A1: n in dom f and
A2: m in Seg n;
A3: f|n = f|Seg n by FINSEQ_1:def 15;
  dom f = Seg len f & n<=len f by A1,FINSEQ_1:def 3,FINSEQ_3:25;
  then
A4: Seg n c= dom f by FINSEQ_1:5;
  then Seg n = dom f /\ Seg n by XBOOLE_1:28
    .= dom(f|n) by A3,RELAT_1:61;
  hence thesis by A2,A3,A4,FUNCT_1:47;
end;

theorem Th7:
  for D be non empty set, f be FinSequence of D, n be Nat, x be
  set st len f = n+1 & x = f.(n+1) holds f = (f|n) ^ <*x*>
proof
  let D be non empty set, f be FinSequence of D, n be Nat,x;
  assume that
A1: len f = n+1 and
A2: x = f.(n+1);
  set fn = f|n;
A3: len fn = n by A1,FINSEQ_1:59,NAT_1:11;
A4: dom f = Seg len f by FINSEQ_1:def 3;
A5: n<=n+1 by NAT_1:11;
A6: now
    let m be Nat;
    assume
A7: m in dom f;
    then
A8: 1<=m by A4,FINSEQ_1:1;
A9: m<=len f by A4,A7,FINSEQ_1:1;
    now
      per cases;
      case
        m = len f;
        hence f.m = (fn^<*x*>).m by A1,A2,A3,FINSEQ_1:42;
      end;
      case
        m <> len f;
        then m<n+1 by A1,A9,XXREAL_0:1;
        then
A10:    m<=n by NAT_1:13;
        then 1<=n by A8,XXREAL_0:2;
        then
A11:    n in dom f by A1,A5,FINSEQ_3:25;
A12:    Seg len fn = dom fn by FINSEQ_1:def 3;
A13:    m in dom fn by A3,A8,A10,FINSEQ_3:25;
        hence (fn^<*x*>).m = fn.m by FINSEQ_1:def 7
          .= f.m by A3,A13,A11,A12,Th6;
      end;
    end;
    hence f.m = (fn^<*x*>).m;
  end;
  len (fn^<*x*>) = n + len <*x*> by A3,FINSEQ_1:22
    .= len f by A1,FINSEQ_1:40;
  hence thesis by A6,FINSEQ_2:9;
end;

theorem Th8:
  for D be non empty set, f be FinSequence of D, n be Nat holds
  (f|n)^(f/^n) = f
proof
  let D be non empty set, f be FinSequence of D,n be Nat;
  set fn = f/^n;
  now
    per cases;
    case
      len f<n;
      then f/^n = <*>D & f|n = f by Def1,Lm3;
      hence thesis by FINSEQ_1:34;
    end;
    case
A1:   n<=len f;
A2:   dom f = Seg len f by FINSEQ_1:def 3;
A3:   len (f|n) = n by A1,FINSEQ_1:59;
A4:   len fn = len f - n by A1,Def1;
      then
A5:   len ((f|n)^(f/^n)) = n+(len f - n) by A3,FINSEQ_1:22
        .= len f;
A6:   dom(f|n) = Seg n by A3,FINSEQ_1:def 3;
      now
        let m be Nat;
        assume
A7:     m in dom f;
        then
A8:     m<=len f by A2,FINSEQ_1:1;
A9:     1<=m by A2,A7,FINSEQ_1:1;
        now
          per cases;
          case
A10:        m<=n;
            then 1<=n by A9,XXREAL_0:2;
            then
A11:        n in dom f by A1,FINSEQ_3:25;
A12:        m in Seg n by A9,A10,FINSEQ_1:1;
            hence ((f|n)^(f/^n)).m = (f|n).m by A6,FINSEQ_1:def 7
              .= f.m by A12,A11,Th6;
          end;
          case
A13:        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;
            n+1<=m by A13,NAT_1:13;
            then
A14:        1<=k by XREAL_1:19;
            k<=len fn by A4,A8,XREAL_1:9;
            then
A15:        k in dom fn by A14,FINSEQ_3:25;
            thus ((f|n) ^ (f/^n)).m = fn.k by A3,A5,A8,A13,FINSEQ_1:24
              .= f.(k+n) by A1,A15,Def1
              .= f.m;
          end;
        end;
        hence ((f|n) ^ (f/^n)).m = f.m;
      end;
      hence thesis by A5,FINSEQ_2:9;
    end;
  end;
  hence thesis;
end;

theorem
  for R1,R2 be FinSequence of REAL st R1,R2 are_fiberwise_equipotent
  holds Sum R1 = Sum R2
proof
  let R1,R2 be FinSequence of REAL;
  defpred P[Nat] means for f,g be FinSequence of REAL st f,g
  are_fiberwise_equipotent & len f = $1 holds Sum f = Sum g;
  assume
A1: R1,R2 are_fiberwise_equipotent;
A2: len R1 = len R1;
A3: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A4: P[n];
    let f,g be FinSequence of REAL;
    assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n+1;
    set a = f.(n+1);
A7: rng f = rng g by A5,CLASSES1:75;
    0<n+1 by NAT_1:3;
    then 0 qua Nat+1<=n+1 by NAT_1:13;
    then n+1 in dom f by A6,FINSEQ_3:25;
    then a in rng g by A7,FUNCT_1:def 3;
    then consider m being Nat such that
A8: m in dom g and
A9: g.m = a by FINSEQ_2:10;
    set gg = g/^m, gm = g|m;
    m<=len g by A8,FINSEQ_3:25;
    then
A10: len gm = m by FINSEQ_1:59;
A11: 1<=m by A8,FINSEQ_3:25;
    then max(0,m-1) = m-1 by FINSEQ_2:4;
    then reconsider m1 = m-1 as Element of NAT by FINSEQ_2:5;
A12: m = m1+1;
    then m1<=m by NAT_1:11;
    then
A13: Seg m1 c= Seg m by FINSEQ_1:5;
    m in Seg m by A11,FINSEQ_1:1;
    then gm.m = a by A8,A9,Th6;
    then
A14: gm = (gm|m1)^<*a*> by A10,A12,Th7;
    set fn = f|n;
A15: g = (g|m)^(g/^m) by Th8;
A16: gm|m1 = gm|(Seg m1) by FINSEQ_1:def 15
      .= (g|(Seg m))|(Seg m1) by FINSEQ_1:def 15
      .= g|((Seg m)/\(Seg m1)) by RELAT_1:71
      .= g|(Seg m1) by A13,XBOOLE_1:28
      .= g|m1 by FINSEQ_1:def 15;
A17: f = fn ^ <*a*> by A6,Th7;
    now
      let x;
      card Coim(f,x) = card Coim(g,x) by A5,CLASSES1:def 9;
      then
      card(fn"{x}) + card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x}) by A15
,A14,A16,A17,FINSEQ_3:57
        .= card(((g|m1)^<*a*>)"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
        .= card((g|m1)"{x})+ card(<*a*>"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
        .= card((g|m1)"{x}) + card((g/^m)"{x})+ card(<*a*>"{x})
        .= card(((g|m1)^(g/^m))"{x})+ card(<*a*>"{x}) by FINSEQ_3:57;
      hence card Coim(fn,x) = card Coim((g|m1)^(g/^m),x);
    end;
    then
A18: fn, (g|m1)^(g/^m) are_fiberwise_equipotent by CLASSES1:def 9;
    len fn = n by A6,FINSEQ_1:59,NAT_1:11;
    then Sum fn = Sum((g|m1)^gg) by A4,A18;
    hence Sum f = Sum((g|m1)^gg) + Sum <*a*> by A17,RVSUM_1:75
      .= Sum(g|m1) + Sum gg+ Sum <*a*> by RVSUM_1:75
      .= Sum(g|m1)+ Sum <*a*> + Sum gg
      .= Sum gm + Sum gg by A14,A16,RVSUM_1:75
      .= Sum g by A15,RVSUM_1:75;
  end;
A19: P[0]
  proof
    let f,g be FinSequence of REAL;
    assume f,g are_fiberwise_equipotent & len f = 0;
    then
A20:   len g = 0 & f = <*>REAL by Th3;
     then g = <*>REAL;
    hence thesis by A20;
  end;
  for n holds P[n] from NAT_1:sch 1(A19,A3);
  hence thesis by A1,A2;
end;

definition
  let R be FinSequence of REAL;
  func MIM(R) -> FinSequence of REAL means
  :Def2:
  len it = len R & it.(len it) = R.(len R) &
  for n be Nat st 1 <= n & n <= len it - 1 holds it.n = (R.n) - (R.(n+1));
  existence
  proof
    per cases;
    suppose
A1:   len R = 0;
      take a = R;
      thus len a = len R & a.(len a) = R.(len R);
      let n be Nat;
      assume 1<=n & n<=len a - 1;
      hence thesis by A1,XXREAL_0:2;
    end;
    suppose
      len R <> 0;
      then 0<len R by NAT_1:3;
      then 0 qua Nat+1<=len R by NAT_1:13;
      then max(0,len R -1) = len R - 1 by FINSEQ_2:4;
      then reconsider l = len R -1 as Element of NAT by FINSEQ_2:5;
      defpred P[Nat,set] means $2 = R.$1 - R.($1+1);
      set t = R.(len R);
A2:   for n be Nat st n in Seg l ex x be Real st P[n,x];
      consider p be FinSequence of REAL such that
A3:   dom p = Seg l & for n be Nat st n in Seg l holds P[n,p.n] from
      FINSEQ_1:sch 5(A2);
      take a = p^<*t*>;
      thus
A4:   len a = len p + len <*t*> by FINSEQ_1:22
        .= l+len <*t*> by A3,FINSEQ_1:def 3
        .= l+1 by FINSEQ_1:39
        .= len R;
      hence a.(len a) = a.(l+1) .= a.(len p +1) by A3,FINSEQ_1:def 3
        .= R.(len R) by FINSEQ_1:42;
      let n be Nat;
      assume 1<=n & n<=len a - 1;
      then
A5:   n in Seg l by A4,FINSEQ_1:1;
      then p.n = R.n - R.(n+1) by A3;
      hence thesis by A3,A5,FINSEQ_1:def 7;
    end;
  end;
  uniqueness
  proof
    let p1,p2 be FinSequence of REAL;
    assume that
A6: len p1 = len R and
A7: p1.(len p1) = R.(len R) and
A8: for n be Nat st 1<=n & n<=len p1 - 1 holds p1.n = R.n - R.(n+1) and
A9: len p2 = len R and
A10: p2.(len p2) = R.(len R) and
A11: for n be Nat st 1<=n & n<=len p2 - 1 holds p2.n = R.n - R.(n+1);
A12: dom p1 = Seg len R by A6,FINSEQ_1:def 3;
    now
      let n be Nat;
      set r = R.n;
      assume
A13:  n in dom p1;
      then
A14:  1<=n by A12,FINSEQ_1:1;
A15:  n<=len R by A12,A13,FINSEQ_1:1;
      now
        per cases;
        case
          n = len R;
          hence p1.n = p2.n by A6,A7,A9,A10;
        end;
        case
A16:      n <> len R;
          set s = R.(n+1);
          n<len R by A15,A16,XXREAL_0:1;
          then n+1<=len R by NAT_1:13;
          then
A17:      n<=len R - 1 by XREAL_1:19;
          then p1.n = r-s by A6,A8,A14;
          hence p1.n = p2.n by A9,A11,A14,A17;
        end;
      end;
      hence p1.n = p2.n;
    end;
    hence thesis by A6,A9,FINSEQ_2:9;
  end;
end;

theorem Th10:
  for R be FinSequence of REAL, r be Real, n be Element of NAT st
  len R = n+2 & R.(n+1) = r holds MIM(R|(n+1)) = MIM(R)|n ^ <* r *>
proof
  let R be FinSequence of REAL, s,n;
  assume that
A1: len R = n+2 and
A2: R.(n+1) = s;
  set f1 = R|(n+1), m1 = MIM(f1), mf = MIM(R), fn = mf|n;
  0<n+1 by NAT_1:3;
  then
A3: 0 qua Nat+1<=n+1 by NAT_1:13;
A4: n+1+1 = n+(1+1);
  then n+1<=n+2 by NAT_1:11;
  then
A5: Seg len R = dom R & n+1 in Seg(n+2) by A3,FINSEQ_1:1,def 3;
A6: len f1 = n+1 by A1,A4,FINSEQ_1:59,NAT_1:11;
  then
A7: len MIM(f1) = n+1 by Def2;
  then
A8: dom m1 = Seg(n+1) by FINSEQ_1:def 3;
  n+1 in Seg(n+1) by A3,FINSEQ_1:1;
  then f1.(n+1) = s by A1,A2,A5,Th6;
  then
A9: m1.(n+1) = s by A6,A7,Def2;
A10: Seg len fn = dom fn by FINSEQ_1:def 3;
A11: Seg len mf = dom mf by FINSEQ_1:def 3;
A12: len mf = n+2 by A1,Def2;
  then
A13: len fn = n by FINSEQ_1:59,NAT_1:11;
A14: n<=n+2 by NAT_1:11;
A15: now
    let m be Nat;
    assume
A16: m in dom m1;
    then
A17: 1<=m by A8,FINSEQ_1:1;
A18: m<=n+1 by A8,A16,FINSEQ_1:1;
    now
      per cases;
      case
        m = n+1;
        hence m1.m = (fn^<*s*>).m by A13,A9,FINSEQ_1:42;
      end;
      case
        m <> n+1;
        then
A19:    m<n+1 by A18,XXREAL_0:1;
        then
A20:    m<=n by NAT_1:13;
        then
A21:    m in Seg n by A17,FINSEQ_1:1;
        set r2 = R.(m+1);
        set r1 = R.m;
A22:    len mf -1 = n+1 by A12;
        1<=n by A17,A20,XXREAL_0:2;
        then n in Seg(n+2) by A14,FINSEQ_1:1;
        then fn.m = mf.m by A12,A11,A21,Th6;
        then
A23:    r1 - r2 = fn.m by A17,A18,A22,Def2
          .= (fn^<*s*>).m by A13,A10,A21,FINSEQ_1:def 7;
        1<=m+1 & m+1<=n+1 by A19,NAT_1:11,13;
        then m+1 in Seg(n+1) by FINSEQ_1:1;
        then
A24:    f1.(m+1) = r2 by A1,A5,Th6;
        len m1 -1 = n & f1.m = r1 by A1,A7,A5,A8,A16,Th6;
        hence m1.m = (fn^<*s*>).m by A17,A20,A23,A24,Def2;
      end;
    end;
    hence m1.m = (fn^<*s*>).m;
  end;
  len(fn^<*s*>) = n + len <*s*> by A13,FINSEQ_1:22
    .= n+1 by FINSEQ_1:40;
  hence thesis by A7,A15,FINSEQ_2:9;
end;

theorem Th11:
  for R be FinSequence of REAL, r,s be Real, n be Element of NAT
  st len R = n+2 & R.(n+1) = r & R.(n+2) = s holds
  MIM(R) = MIM(R)|n ^ <* r-s,s *>
proof
  let R be FinSequence of REAL, r,s,n;
  set mf = MIM(R), nf = mf|n;
  assume that
A1: len R = n+2 and
A2: R.(n+1) = r and
A3: R.(n+2) = s;
A4: len mf = n+2 by A1,Def2;
  then
A5: dom mf = Seg(n+2) by FINSEQ_1:def 3;
A6: n+(1+1) = n+1+1;
  then n+1<=n+2 by NAT_1:11;
  then
A7: n<n+2 by NAT_1:13;
A8: len nf = n by A4,FINSEQ_1:59,NAT_1:11;
  then len (nf^<* r-s,s *>) = n + len <* r-s,s *> by FINSEQ_1:22;
  then
A9: len(nf^<* r-s,s *>) = n+2 by FINSEQ_1:44;
A10: n<=n+2 by NAT_1:11;
  now
    let m be Nat;
    assume
A11: m in dom mf;
    then
A12: 1<=m by A5,FINSEQ_1:1;
A13: m<=n+2 by A5,A11,FINSEQ_1:1;
    now
      per cases;
      case
A14:    m = n+2;
        hence mf.m = s by A1,A3,A4,Def2
          .= <* r-s,s *>.(n+2-n) by FINSEQ_1:44
          .= (nf ^ <* r-s,s *>).m by A8,A9,A7,A14,FINSEQ_1:24;
      end;
      case
        m <> n+2;
        then m<n+2 by A13,XXREAL_0:1;
        then
A15:    m<=n+1 by A6,NAT_1:13;
A16:    len mf - 1 = n+1 by A4;
        now
          per cases;
          case
A17:        m = n+1;
            then
A18:        n<m by NAT_1:13;
            thus mf.m = r - s by A2,A3,A6,A12,A16,A17,Def2
              .= <* r-s,s *>.(n+1-n) by FINSEQ_1:44
              .= (nf ^ <* r-s,s *>).m by A8,A9,A13,A17,A18,FINSEQ_1:24;
          end;
          case
            m <> n+1;
            then m<n+1 by A15,XXREAL_0:1;
            then
A19:        m<=n by NAT_1:13;
            then
A20:        m in Seg n by A12,FINSEQ_1:1;
            1<=n by A12,A19,XXREAL_0:2;
            then
A21:        n in Seg(n+2) by A10,FINSEQ_1:1;
A22:        dom nf = Seg len nf by FINSEQ_1:def 3;
            dom mf = Seg len mf by FINSEQ_1:def 3;
            hence mf.m = nf.m by A4,A20,A21,Th6
              .= (nf ^ <* r-s,s *>).m by A8,A20,A22,FINSEQ_1:def 7;
          end;
        end;
        hence mf.m = (nf ^ <* r-s,s *>).m;
      end;
    end;
    hence mf.m = (nf ^ <* r-s,s *>).m;
  end;
  hence thesis by A4,A9,FINSEQ_2:9;
end;

theorem Th12:
  MIM( <*>REAL ) = <*>REAL
proof
  set o = <*>REAL, mo = MIM(o);
  len mo = len o by Def2;
  hence thesis;
end;

theorem Th13:
  for r be Real holds MIM(<*r*>) = <*r*>
proof
  let r be Real;
  set f = <*r*>;
A1: len f = 1 by FINSEQ_1:40;
  then
A2: len MIM(f) = 1 by Def2;
  then
A3: dom MIM(f) = Seg 1 by FINSEQ_1:def 3;
  now
    let n be Nat;
    assume n in dom MIM(f);
    then n = 1 by A3,FINSEQ_1:2,TARSKI:def 1;
    hence MIM(f).n = f.n by A1,A2,Def2;
  end;
  hence thesis by A1,A2,FINSEQ_2:9;
end;

theorem
  for r,s be Real holds MIM(<*r,s*>) = <*r-s,s*>
proof
  let r,s be Real;
  set f = <*r,s*>;
A1: len f = 2 & f.1 = r by FINSEQ_1:44;
A2: f.2 = s by FINSEQ_1:44;
  0 qua Nat+2 = 2 & 0 qua Nat +1 = 1;
  then MIM(f) = MIM(f)|0 ^ <*r-s,s*> by A1,A2,Th11;
  hence thesis by FINSEQ_1:34;
end;

theorem
  for R be FinSequence of REAL, n be Element of NAT holds MIM(R) /^ n =
  MIM(R/^n)
proof
  let R be FinSequence of REAL,n;
  set mf = MIM(R), fn = R/^n, mn = MIM(fn);
A1: len mf = len R by Def2;
A2: len mn = len fn by Def2;
  now
    per cases;
    case
A3:   len R<n;
      then mf /^ n = <*>REAL by A1,Def1;
      hence thesis by A3,Def1,Th12;
    end;
    case
A4:   n<=len R;
      then
A5:   len(mf/^n) = len R - n by A1,Def1;
A6:   len mn = len fn by Def2;
      then
A7:   dom mn = Seg len fn by FINSEQ_1:def 3;
A8:   Seg len(mf/^n) = dom(mf/^n) by FINSEQ_1:def 3;
A9:   len fn = len R - n by A4,Def1;
A10:  Seg len fn = dom fn by FINSEQ_1:def 3;
      now
        let m be Nat;
        set r1 = R.(m+n);
        assume
A11:    m in dom mn;
        then
A12:    1<=m by A7,FINSEQ_1:1;
A13:    m<=len fn by A7,A11,FINSEQ_1:1;
A14:    fn.m = r1 by A4,A10,A7,A11,Def1;
        m<=m+n by NAT_1:11;
        then
A15:    1<=m+n by A12,XXREAL_0:2;
        now
          per cases;
          case
A16:        m = len fn;
            thus (mf/^n).m = mf.(m+n) by A1,A4,A5,A9,A8,A7,A11,Def1
              .= r1 by A1,A9,A16,Def2
              .= mn.m by A6,A14,A16,Def2;
          end;
          case
            m <> len fn;
            then m<len fn by A13,XXREAL_0:1;
            then
A17:        m+1<=len fn by NAT_1:13;
            then
A18:        m<=len fn - 1 by XREAL_1:19;
            set r2 = R.(m+1+n);
A19:        m+1+n = m+n+1;
            1<=m+1 by NAT_1:11;
            then m+1 in dom fn by A17,FINSEQ_3:25;
            then
A20:        fn.(m+1) = r2 by A4,Def1;
            m+1+n<=len R by A9,A17,XREAL_1:19;
            then
A21:        m+n<=len R - 1 by A19,XREAL_1:19;
            thus (mf/^n).m = mf.(m+n) by A1,A4,A5,A9,A8,A7,A11,Def1
              .= r1-r2 by A1,A15,A19,A21,Def2
              .= mn.m by A2,A12,A14,A18,A20,Def2;
          end;
        end;
        hence (mf/^n).m = mn.m;
      end;
      hence thesis by A5,A9,A6,FINSEQ_2:9;
    end;
  end;
  hence thesis;
end;

theorem Th16:
  for R be FinSequence of REAL st len R <> 0 holds Sum MIM(R) = R. 1
proof
  defpred P[Nat] means for R be FinSequence of REAL st len R <> 0 & len R = $1
  holds Sum MIM(R) = R.1;
  let R be FinSequence of REAL;
  assume
A1: len R <> 0;
A2: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A3: P[n];
    let R be FinSequence of REAL;
    assume that
    len R <> 0 and
A4: len R = n+1;
    now
      per cases;
      case
        n = 0;
        then
A5:     R = <*R.1*> by A4,FINSEQ_1:40;
        then MIM(R) = R by Th13;
        hence thesis by A5,FINSOP_1:11;
      end;
      case
        n <> 0;
        then 0<n by NAT_1:3;
        then 0 qua Nat+1<=n by NAT_1:13;
        then max(0,n-1) = n-1 by FINSEQ_2:4;
        then reconsider n1 = n-1 as Element of NAT by FINSEQ_2:5;
A6:     0 qua Nat+1<=n1+1 by NAT_1:11;
        then
A7:     Seg len R = dom R & 1 in Seg(n1+1) by FINSEQ_1:1,def 3;
        n1+2 = n1+1+1;
        then n1+1<=n1+2 by NAT_1:11;
        then
A8:     n1+1 in Seg(n1+2) by A6,FINSEQ_1:1;
        set f1 = R|(n1+1);
        set s = R.(n1+2);
        set r = R.(n1+1);
A9:     n1+2 = len R by A4;
A10:    len f1 = n1+1 by A4,FINSEQ_1:59,NAT_1:11;
        thus Sum MIM(R) = Sum((MIM(R)|n1) ^ <* r-s,s *>) by A4,Th11
          .= Sum(MIM(R)|n1) + Sum(<* r-s,s *>) by RVSUM_1:75
          .= Sum(MIM(R)|n1) + (r-s + s) by RVSUM_1:77
          .= Sum((MIM(R)|n1) ^<*r*>) by RVSUM_1:74
          .= Sum MIM(f1) by A9,Th10
          .= f1.1 by A3,A10
          .= R.1 by A4,A8,A7,Th6;
      end;
    end;
    hence thesis;
  end;
A11: P[0];
  for n holds P[n] from NAT_1:sch 1(A11,A2);
  hence thesis by A1;
end;

theorem
  for R be FinSequence of REAL, n be Element of NAT st n<len R holds Sum
  MIM(R/^n) = R.(n+1)
proof
  let R be FinSequence of REAL,n;
  assume
A1: n<len R;
  then
A2: len(R/^n) = len R - n by Def1;
  n+1<=len R by A1,NAT_1:13;
  then 1<=len R - n by XREAL_1:19;
  then
A3: 1 in dom(R/^n) by A2,FINSEQ_3:25;
  len(R/^n) <> 0 by A1,A2;
  hence Sum MIM(R/^n) = (R/^n).1 by Th16
    .= R.(n+1) by A1,A3,Def1;
end;

definition
  let IT be FinSequence of REAL;
  redefine attr IT is non-increasing means
  :Def3:
  for n be Element of NAT st n in dom IT & n+1 in dom IT holds
  IT.n >= IT.(n+1);
  compatibility
  proof
    thus IT is non-increasing implies for n be Element of NAT st n in dom IT &
    n+1 in dom IT holds IT.n >= IT.(n+1)
    proof
      assume
A1:   IT is non-increasing;
      let n be Element of NAT such that
A2:   n in dom IT & n+1 in dom IT;
      n+(0 qua Nat) <= n+1 by XREAL_1:6;
      hence thesis by A1,A2,SEQM_3:def 4;
    end;
    assume
A3: for n be Element of NAT st n in dom IT & n+1 in dom IT holds IT.n
    >= IT.(n+1);
    let m, n such that
A4: m in dom IT and
A5: n in dom IT & m <= n;
    defpred P[Nat] means $1 in dom IT & m <= $1 implies IT.m >= IT.$1;
A6: for k being Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT such that
A7:   P[k] and
A8:   k+1 in dom IT;
      assume m <= k+1;
      then
A9:   m < k+1 or m = k+1 by XXREAL_0:1;
      per cases by A9,NAT_1:13;
      suppose
A10:    m <= k;
        k+(0 qua Nat) <= k+1 & k+1 <= len IT by A8,FINSEQ_3:25,XREAL_1:6;
        then
A11:    k <= len IT by XXREAL_0:2;
        1 <= m by A4,FINSEQ_3:25;
        then
A12:    1 <= k by A10,XXREAL_0:2;
        then k in dom IT by A11,FINSEQ_3:25;
        then IT.k >= IT.(k+1) by A3,A8;
        hence thesis by A7,A10,A12,A11,FINSEQ_3:25,XXREAL_0:2;
      end;
      suppose
        m = k+1;
        hence thesis;
      end;
    end;
A13: P[0] by FINSEQ_3:24;
    for k being Element of NAT holds P[k] from NAT_1:sch 1(A13,A6);
    hence thesis by A5;
  end;
end;

registration
  cluster non-increasing for FinSequence of REAL;
  existence
  proof
    take <*>REAL;
    let n;
    thus thesis;
  end;
end;

theorem Th18:
  for R be FinSequence of REAL st len R = 0 or len R = 1 holds
  R is non-increasing
proof
  let R be FinSequence of REAL;
  assume
A1: len R = 0 or len R = 1;
  now
    per cases by A1;
    case
      len R = 0;
      then R = <*>REAL;
      then for n st n in dom R & n+1 in dom R holds R.n>=R.(n+1);
      hence thesis by Def3;
    end;
    case
      len R = 1;
      then
A2:   dom R = {1} by FINSEQ_1:2,def 3;
      now
        let n;
        assume that
A3:     n in dom R and
A4:     n+1 in dom R;
        n = 1 by A2,A3,TARSKI:def 1;
        hence R.n>=R.(n+1) by A2,A4,TARSKI:def 1;
      end;
      hence thesis by Def3;
    end;
  end;
  hence thesis;
end;

theorem Th19:
  for R be FinSequence of REAL holds R is non-increasing iff for n
  ,m be Element of NAT st n in dom R & m in dom R & n<m holds R.n>=R.m
proof
  let R be FinSequence of REAL;
  thus R is non-increasing implies for n,m st n in dom R & m in dom R & n<m
  holds R.n>=R.m
  proof
    defpred P[Nat] means $1 in dom R implies for n st n in dom R & n<$1 holds
    R.n>=R.$1;
    assume
A1: R is non-increasing;
A2: for m st P[m] holds P[m+1]
    proof
      let m;
      assume
A3:   P[m];
      assume
A4:   m+1 in dom R;
      then m+1<=len R by FINSEQ_3:25;
      then
A5:   m<=len R by NAT_1:13;
      let n;
      assume that
A6:   n in dom R and
A7:   n<m+1;
      set t = R.m, r = R.n, s = R.(m+1);
A8:   n<=m by A7,NAT_1:13;
      1<=n by A6,FINSEQ_3:25;
      then
A9:   1<=m by A8,XXREAL_0:2;
      then
A10:  m in dom R by A5,FINSEQ_3:25;
      now
        per cases;
        case
          n = m;
          hence thesis by A1,A4,A6,Def3;
        end;
        case
          n <> m;
          then n<m by A8,XXREAL_0:1;
          then
A11:      r>=t by A3,A6,A9,A5,FINSEQ_3:25;
          t>=s by A1,A4,A10,Def3;
          hence thesis by A11,XXREAL_0:2;
        end;
      end;
      hence thesis;
    end;
    Seg len R = dom R by FINSEQ_1:def 3;
    then
A12: P[0] by FINSEQ_1:1;
    for m holds P[m] from NAT_1:sch 1(A12,A2);
    hence thesis;
  end;
  assume
A13: for n,m st n in dom R & m in dom R & n<m holds R.n>=R.m;
  let n;
A14: n<n+1 by NAT_1:13;
  assume n in dom R & n+1 in dom R;
  hence thesis by A13,A14;
end;

theorem Th20:
  for R be non-increasing FinSequence of REAL, n be Element of NAT
  holds R|n is non-increasing FinSequence of REAL
proof
  let f be non-increasing FinSequence of REAL, n;
  set fn = f|n;
  now
    per cases;
    case
      n = 0;
      then len fn = 0;
      hence thesis by Th18;
    end;
    case
      n <> 0;
      then 0<n by NAT_1:3;
      then
A1:   0 qua Nat+1<=n by NAT_1:13;
      now
        per cases;
        case
          len f<=n;
          hence thesis by Lm3;
        end;
        case
          n<len f;
          then
A2:       n in dom f & len fn = n by A1,FINSEQ_1:59,FINSEQ_3:25;
          now
            let m;
A3:         dom fn = Seg len fn by FINSEQ_1:def 3;
            assume
A4:         m in dom fn & m+1 in dom fn;
            then
A5:         m in dom f & m+1 in dom f by A2,A3,Th6;
            f.m = fn.m & f.(m+1) = fn.(m+1) by A2,A4,A3,Th6;
            hence fn.m>=fn.(m+1) by A5,Def3;
          end;
          hence thesis by Def3;
        end;
      end;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem
  for R be non-increasing FinSequence of REAL, n be Element of NAT holds
  R /^ n is non-increasing
proof
  let f be non-increasing FinSequence of REAL, n;
  set fn = f /^ n;
  now
    let m;
    assume that
A1: m in dom fn and
A2: m+1 in dom fn;
A3: m<=m+n by NAT_1:11;
    1<=m by A1,FINSEQ_3:25;
    then
A4: 1<=m+n by A3,XXREAL_0:2;
A5: 1<=m+n+1 by NAT_1:11;
A6: m+1<=len fn by A2,FINSEQ_3:25;
    set r = fn.m, s = fn.(m+1);
A7: m+1+n = m+n+1;
A8: m<=len fn by A1,FINSEQ_3:25;
    now
      per cases;
      case
A9:     n<=len f;
        then
A10:    len fn = len f - n by Def1;
        then m+n<=len f by A8,XREAL_1:19;
        then
A11:    m+n in dom f by A4,FINSEQ_3:25;
        m+n+1<=len f by A6,A7,A10,XREAL_1:19;
        then
A12:    m+n+1 in dom f by A5,FINSEQ_3:25;
        r = f.(m+n) & s = f.(m+n+1) by A1,A2,A7,A9,Def1;
        hence r>=s by A11,A12,Def3;
      end;
      case
        len f<n;
        then fn = <*>REAL by Def1;
        hence r>=s;
      end;
    end;
    hence r>=s;
  end;
  hence thesis by Def3;
end;

Lm4: for f,g be non-increasing FinSequence of REAL, n st len f = n+1 & len f =
len g & f,g are_fiberwise_equipotent holds f.(len f) = g.(len g) & f|n, g|n
are_fiberwise_equipotent
proof
  let f,g be non-increasing FinSequence of REAL, n;
  assume that
A1: len f = n+1 and
A2: len f = len g and
A3: f,g are_fiberwise_equipotent;
  set r = f.(n+1), s = g.(n+1);
  0<n+1 by NAT_1:3;
  then
A4: 0 qua Nat+1<=n+1 by NAT_1:13;
  then
A5: n+1 in dom f by A1,FINSEQ_3:25;
A6: f = (f|n)^<*r*> by A1,Th7;
A7: n+1 in dom g by A1,A2,A4,FINSEQ_3:25;
A8: now
A9: rng f = rng g by A3,CLASSES1:75;
    assume
A10: r <> s;
    now
      per cases by A10,XXREAL_0:1;
      case
A11:    r>s;
        s in rng f by A7,A9,FUNCT_1:def 3;
        then consider m be Nat such that
A12:    m in dom f and
A13:    f.m = s by FINSEQ_2:10;
A14:    m<=len f by A12,FINSEQ_3:25;
        now
          per cases;
          case
            m = len f;
            hence contradiction by A1,A11,A13;
          end;
          case
            m <> len f;
            then m<n+1 by A1,A14,XXREAL_0:1;
            hence contradiction by A5,A11,A12,A13,Th19;
          end;
        end;
        hence contradiction;
      end;
      case
A15:    r<s;
        r in rng g by A5,A9,FUNCT_1:def 3;
        then consider m be Nat such that
A16:    m in dom g and
A17:    g.m = r by FINSEQ_2:10;
A18:    m<=len g by A16,FINSEQ_3:25;
        now
          per cases;
          case
            m = len g;
            hence contradiction by A1,A2,A15,A17;
          end;
          case
            m <> len g;
            then m<n+1 by A1,A2,A18,XXREAL_0:1;
            hence contradiction by A7,A15,A16,A17,Th19;
          end;
        end;
        hence contradiction;
      end;
    end;
    hence contradiction;
  end;
  hence f.(len f) = g.(len g) by A1,A2;
A19: g = (g|n)^<*r*> by A1,A2,A8,Th7;
  now
    let x;
    card Coim(f|n,x) + card(<*r*>"{x}) = card Coim(f,x) by A6,FINSEQ_3:57
      .= card Coim(g,x) by A3,CLASSES1:def 9
      .= card Coim(g|n,x) + card(<*r*>"{x}) by A19,FINSEQ_3:57;
    hence card Coim(f|n,x) = card Coim(g|n,x);
  end;
  hence thesis by CLASSES1:def 9;
end;

defpred P[Nat] means for R be FinSequence of REAL st $1 = len R ex b be
non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent;

Lm5: P[0]
proof
  let R be FinSequence of REAL;
  assume len R = 0;
  then reconsider a = R as non-increasing FinSequence of REAL by Th18;
  take a;
  thus thesis;
end;

Lm6: for n st P[n] holds P[n+1]
proof
  let n;
  assume
A1: P[n];
  let R be FinSequence of REAL;
  set fn = R|(Seg n);
A2: fn = R|n by FINSEQ_1:def 15;
  set q = R.(n+1);
  reconsider fn as FinSequence by FINSEQ_1:15;
  rng fn c= rng R by RELAT_1:70;
  then rng fn c= REAL by XBOOLE_1:1;
  then reconsider fn as FinSequence of REAL by FINSEQ_1:def 4;
  n<=n+1 by NAT_1:11;
  then
A3: dom fn = dom R /\ Seg n & Seg n c= Seg(n+1) by FINSEQ_1:5,RELAT_1:61;
  assume
A4: n+1 = len R;
  then dom R = Seg(n+1) by FINSEQ_1:def 3;
  then dom fn = Seg n by A3,XBOOLE_1:28;
  then
A5: len fn = n by FINSEQ_1:def 3;
  then consider a be non-increasing FinSequence of REAL such that
A6: fn,a are_fiberwise_equipotent by A1;
A7: len fn = len a by A6,Th3;
A8: Seg len a = dom a by FINSEQ_1:def 3;
  now
    per cases;
    case
A9:   for t be Real st t in rng a holds q<=t;
      set b = a^<*q*>;
A10:  len b = n + len <*q*> by A5,A7,FINSEQ_1:22
        .= n+1 by FINSEQ_1:39;
      now
        let m;
        assume that
A11:    m in dom b and
A12:    m+1 in dom b;
A13:    1<=m+1 by A12,FINSEQ_3:25;
        set r = b.m, s = b.(m+1);
A14:    1<=m by A11,FINSEQ_3:25;
A15:    m+1<=len b by A12,FINSEQ_3:25;
        then m<=n+1-1 by A10,XREAL_1:19;
        then m in Seg n by A14,FINSEQ_1:1;
        then
A16:    m in dom a by A5,A7,FINSEQ_1:def 3;
        then
A17:    r = a.m by FINSEQ_1:def 7;
A18:    a.m in rng a by A16,FUNCT_1:def 3;
        now
          per cases;
          case
            m+1 = len b;
            then s = q by A5,A7,A10,FINSEQ_1:42;
            hence r>=s by A9,A17,A18;
          end;
          case
            m+1 <> len b;
            then m+1<len b by A15,XXREAL_0:1;
            then m+1<=n+1-1 by A10,NAT_1:13;
            then m+1 in Seg n by A13,FINSEQ_1:1;
            then
A19:        m+1 in dom a by A5,A7,FINSEQ_1:def 3;
            then a.(m+1) = s by FINSEQ_1:def 7;
            hence r>=s by A16,A17,A19,Def3;
          end;
        end;
        hence r>=s;
      end;
      then reconsider b as non-increasing FinSequence of REAL by Def3;
      take b;
      fn^<*q*> = R by A4,A2,Th7;
      hence R,b are_fiberwise_equipotent by A6,Th1;
    end;
    case
A20:  ex t be Real st t in rng a & not q<=t;
      defpred Q[Nat] means $1 in dom a & for r st r = a.$1 holds r<q;
A21:  ex k be Nat st Q[k]
      proof
        consider t be Real such that
A22:    t in rng a and
A23:    t<q by A20;
        consider k be Nat such that
A24:    k in dom a and
A25:    a.k = t by A22,FINSEQ_2:10;
        reconsider k as Element of NAT by ORDINAL1:def 12;
        take k;
        thus k in dom a by A24;
        let r;
        assume r = a.k;
        hence thesis by A23,A25;
      end;
      consider mi be Nat such that
A26:  Q[mi] & for m be Nat st Q[m] holds mi <= m from NAT_1:sch 5(A21
      );
      1<=mi by A26,FINSEQ_3:25;
      then max(0,mi-1) = mi-1 by FINSEQ_2:4;
      then reconsider k = mi-1 as Element of NAT by FINSEQ_2:5;
      mi<mi+1 by NAT_1:13;
      then
A27:  k<=mi by XREAL_1:19;
A28:  mi<=len a by A26,FINSEQ_3:25;
      then
A29:  k<=len a by A27,XXREAL_0:2;
      then
A30:  len(a/^k) = len a - k by Def1;
A31:  dom((a|k)^<*q*>) = Seg len((a|k)^<*q*>) by FINSEQ_1:def 3;
A32:  dom (a|k) c= dom((a|k)^<*q*>) by FINSEQ_1:26;
      set ak = a/^k, b = (a|k)^<*q*>^ak;
A33:  dom (a|k) = Seg len (a|k) by FINSEQ_1:def 3;
A34:  len(a|k) = k by A28,A27,FINSEQ_1:59,XXREAL_0:2;
      then
A35:  len((a|k)^<*q*>) = k+len <*q*> by FINSEQ_1:22
        .= k+1 by FINSEQ_1:39;
      then
A36:  len b = k+1 + len(a/^k) by FINSEQ_1:22;
      k+1<=len a by A26,FINSEQ_3:25;
      then
A37:  1<=len(a/^k) by A30,XREAL_1:19;
      now
        let m;
        assume that
A38:    m in dom b and
A39:    m+1 in dom b;
A40:    1<=m+1 by A39,FINSEQ_3:25;
A41:    m+1<=len b by A39,FINSEQ_3:25;
        set r = b.m, s = b.(m+1);
A42:    1<=m by A38,FINSEQ_3:25;
A43:    m<=len b by A38,FINSEQ_3:25;
        now
          per cases;
          case
A44:        m+1<=k;
            dom(a|k) c= dom((a|k)^(a/^k)) by FINSEQ_1:26;
            then
A45:        dom(a|k) c= dom a by Th8;
A46:        dom a = Seg len a by FINSEQ_1:def 3;
            m<=k by A44,NAT_1:13;
            then
A47:        m in Seg k by A42,FINSEQ_1:1;
            1<=k by A40,A44,XXREAL_0:2;
            then
A48:        k in dom a by A29,A46,FINSEQ_1:1;
            then
A49:        a.m = (a|k).m by A47,Th6;
A50:        m+1 in Seg k by A40,A44,FINSEQ_1:1;
            then
A51:        a.(m+1) = (a|k).(m+1) by A48,Th6;
A52:        b.(m+1) = ((a|k)^<*q*>).(m+1) by A34,A33,A32,A50,FINSEQ_1:def 7
              .= a.(m+1) by A34,A33,A50,A51,FINSEQ_1:def 7;
            b.m = ((a|k)^<*q*>).m by A34,A33,A32,A47,FINSEQ_1:def 7
              .= a.m by A34,A33,A47,A49,FINSEQ_1:def 7;
            hence r>=s by A34,A33,A47,A50,A52,A45,Def3;
          end;
          case
            k<m+1;
            then
A53:        k<=m by NAT_1:13;
            now
              per cases;
              case
A54:            k = m;
                then m+1 in dom((a|k)^<*q*>) by A35,A31,FINSEQ_1:4;
                then
A55:            b.(m+1) = ((a|k)^<*q*>).(k+1) by A54,FINSEQ_1:def 7
                  .= q by A34,FINSEQ_1:42;
A56:            m in Seg k by A42,A54,FINSEQ_1:1;
A57:            k in dom a by A8,A29,A42,A54,FINSEQ_1:1;
                then
A58:            a.m = (a|k).m by A56,Th6;
A59:            b.m = ((a|k)^<*q*>).m by A34,A33,A32,A56,FINSEQ_1:def 7
                  .= a.m by A34,A33,A56,A58,FINSEQ_1:def 7;
                now
                  assume s>r;
                  then for t be Real st t = a.k holds t<q by A54,A59,A55;
                  then mi<=k by A26,A57;
                  hence contradiction by XREAL_1:44;
                end;
                hence r>=s;
              end;
              case
                k <> m;
                then k<m by A53,XXREAL_0:1;
                then
A60:            k+1<=m by NAT_1:13;
                then
A61:            k+1<m+1 by NAT_1:13;
                max(0,m-(k+1)) = m-(k+1) by A60,FINSEQ_2:4;
                then reconsider l = m-(k+1) as Element of NAT by FINSEQ_2:5;
A62:            l+1 = m+1-(k+1);
                then
A63:            l+1<=len b -(k+1) by A41,XREAL_1:13;
                l<=l+1 by NAT_1:11;
                then
A64:            l<=len(a/^k) by A36,A63,XXREAL_0:2;
                1<=l+1 by NAT_1:11;
                then
A65:            l+1 in dom(a/^k) by A36,A63,FINSEQ_3:25;
                1<=l+1+k by A38,FINSEQ_3:25;
                then
A66:            k+l+1<=len a by A30,A36,A63,XREAL_1:19;
                then
A67:            k+l+1 in dom a by A42,FINSEQ_3:25;
                k+l<=k+l+1 by NAT_1:11;
                then
A68:            k+l<=len a by A66,XXREAL_0:2;
A69:            k+(l+1) <=len a by A30,A36,A63,XREAL_1:19;
                now
                  per cases;
                  case
A70:                k+1 = m;
                    then m in Seg (k+1) by A42,FINSEQ_1:1;
                    then
A71:                b.m = ((a|k)^<*q*>).(k+1) by A35,A31,A70,FINSEQ_1:def 7
                      .= q by A34,FINSEQ_1:42;
A72:                1 in dom(a/^k) by A37,FINSEQ_3:25;
                    b.(m+1) = (a/^k).(k+1+1 - (k+1)) by A35,A41,A61,A70,
FINSEQ_1:24
                      .= a.mi by A29,A72,Def1;
                    hence r>=s by A26,A71;
                  end;
                  case
                    k+1 <> m;
                    then
A73:                k+1<m by A60,XXREAL_0:1;
                    then k+1+1<=m by NAT_1:13;
                    then
A74:                1<=l by XREAL_1:19;
                    then
A75:                l in dom(a/^k) by A64,FINSEQ_3:25;
                    l<=k+l by NAT_1:11;
                    then 1<=k+l by A74,XXREAL_0:2;
                    then
A76:                k+l in dom a by A68,FINSEQ_3:25;
A77:                b.m = (a/^k).l by A35,A43,A73,FINSEQ_1:24
                      .= a.(k+l) by A29,A75,Def1;
                    b.(m+1) = (a/^k).(l+1) by A35,A41,A61,A62,FINSEQ_1:24
                      .= a.(k+l+1) by A29,A65,A69,Def1;
                    hence r>=s by A67,A77,A76,Def3;
                  end;
                end;
                hence r>=s;
              end;
            end;
            hence r>=s;
          end;
        end;
        hence r>=s;
      end;
      then reconsider b as non-increasing FinSequence of REAL by Def3;
      take b;
      now
        let x;
A78:    card Coim(fn,x) = card Coim(a,x) by A6,CLASSES1:def 9;
        thus card Coim(b,x) = card (((a|k)^<*q*>)"{x}) + card(ak"{x}) by
FINSEQ_3:57
          .= card((a|k)"{x}) + card(<*q*>"{x}) + card(ak"{x}) by FINSEQ_3:57
          .= card((a|k)"{x}) + card(ak"{x}) + card(<*q*>"{x})
          .= card(((a|k)^ak)"{x}) + card(<*q*>"{x}) by FINSEQ_3:57
          .= card(fn"{x}) + card(<*q*>"{x}) by A78,Th8
          .= card((fn^<*q*>)"{x}) by FINSEQ_3:57
          .= card Coim(R,x) by A4,A2,Th7;
      end;
      hence R,b are_fiberwise_equipotent by CLASSES1:def 9;
    end;
  end;
  hence thesis;
end;

theorem Th22:
  for R be FinSequence of REAL ex R1 be non-increasing FinSequence of
  REAL st R,R1 are_fiberwise_equipotent
proof
  let R be FinSequence of REAL;
A1: len R = len R;
  for n holds P[n] from NAT_1:sch 1(Lm5,Lm6);
  hence thesis by A1;
end;

Lm7: for n holds for g1,g2 be non-increasing FinSequence of REAL st n = len g1
& g1,g2 are_fiberwise_equipotent holds g1 = g2
proof
  defpred P[Nat] means for g1,g2 be non-increasing FinSequence of REAL st $1 =
  len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2;
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: P[n];
    let g1,g2 be non-increasing FinSequence of REAL;
    set r = g1.(n+1);
    reconsider g1n = g1|n, g2n = g2|n as non-increasing FinSequence of REAL by
Th20;
    assume that
A3: len g1 = n+1 and
A4: g1,g2 are_fiberwise_equipotent;
A5: len g2 = len g1 by A4,Th3;
    then
A6: g1.(len g1) = g2.(len g2) by A3,A4,Lm4;
A7: (g1|n)^<*r*> = g1 by A3,Th7;
    len(g1|n) = n by A3,FINSEQ_1:59,NAT_1:11;
    then g1n = g2n by A2,A3,A4,A5,Lm4;
    hence thesis by A3,A5,A6,A7,Th7;
  end;
A8: P[0]
  proof
    let g1,g2 be non-increasing FinSequence of REAL;
    assume len g1 = 0 & g1,g2 are_fiberwise_equipotent;
    then len g2 = len g1 & g1 = <*>REAL by Th3;
    hence thesis;
  end;
  thus for n holds P[n] from NAT_1:sch 1(A8,A1);
end;

theorem
  for R1,R2 be non-increasing FinSequence of REAL st R1,R2
  are_fiberwise_equipotent holds R1 = R2
proof
  let g1,g2 be non-increasing FinSequence of REAL;
A1: len g1 = len g1;
  assume g1,g2 are_fiberwise_equipotent;
  hence thesis by A1,Lm7;
end;

theorem
  for R be FinSequence of REAL, r,s be Real st r <> 0 holds R"{s/r} = (r
  *R)"{ s }
proof
  let R be FinSequence of REAL, r,s;
A1: Seg len R = dom R & dom(r*R) = Seg len(r*R) by FINSEQ_1:def 3;
  assume
A2: r <> 0;
  thus R"{s/r} c= (r*R)"{s}
  proof
    let x;
    assume
A3: x in R"{s/r};
    then reconsider i = x as Element of NAT;
    R.i in {s/r} by A3,FUNCT_1:def 7;
    then R.i = s/r by TARSKI:def 1;
    then r*(R.i) = s by A2,XCMPLX_1:87;
    then (r*R).i = s by RVSUM_1:44;
    then
A4: (r*R).i in {s} by TARSKI:def 1;
    i in dom R by A3,FUNCT_1:def 7;
    then i in dom (r*R) by A1,FINSEQ_2:33;
    hence thesis by A4,FUNCT_1:def 7;
  end;
  let x;
  assume
A5: x in (r*R)"{s};
  then reconsider i = x as Element of NAT;
  (r*R).i in {s} by A5,FUNCT_1:def 7;
  then (r*R).i = s by TARSKI:def 1;
  then r*R.i = s by RVSUM_1:44;
  then R.i = s/r by A2,XCMPLX_1:89;
  then
A6: R.i in {s/r} by TARSKI:def 1;
  i in dom(r*R) by A5,FUNCT_1:def 7;
  then i in dom R by A1,FINSEQ_2:33;
  hence thesis by A6,FUNCT_1:def 7;
end;

theorem
  for R be FinSequence of REAL holds (0*R)"{0} = dom R
proof
  let R be FinSequence of REAL;
A1: Seg len(0*R) = dom(0*R) by FINSEQ_1:def 3;
A2: len(0*R) = len R & dom R = Seg len R by FINSEQ_1:def 3,FINSEQ_2:33;
  hence (0*R)"{0} c= dom R by A1,RELAT_1:132;
  let x;
  assume
A3: x in dom R;
  then reconsider i = x as Element of NAT;
  (0*R).i = 0*R.i by RVSUM_1:44
    .= 0;
  then (0*R).i in {0} by TARSKI:def 1;
  hence thesis by A2,A1,A3,FUNCT_1:def 7;
end;

begin :: Addenda
:: from VECTSP_9, 2006.01.06, A.T.

reserve f, g for Function;

theorem
  for f, g st rng f = rng g & f is one-to-one & g is one-to-one holds
  f,g are_fiberwise_equipotent
proof
  let f, g be Function such that
A1: rng f = rng g and
A2: f is one-to-one and
A3: g is one-to-one;
  let x;
  per cases;
  suppose
A4: x in rng f;
    then card Coim(f,x) = 1 by A2,FINSEQ_4:73;
    hence thesis by A1,A3,A4,FINSEQ_4:73;
  end;
  suppose
A5: not x in rng f;
    then card(f"{x}) = 0 by CARD_1:27,FUNCT_1:72;
    hence thesis by A1,A5,CARD_1:27,FUNCT_1:72;
  end;
end;

:: from REVROT_1, 2007.03.18, A.T.

theorem
  for D being set, f being FinSequence of D holds f /^ len f = {}
proof
  let D be set, f be FinSequence of D;
  len (f /^ len f) = len f - len f by Def1
    .= 0;
  hence thesis;
end;

:: from SCMBSORT, 2007.07.26, A.T.

theorem
  for f,g be Function,m,n be set st f.m=g.n & f.n=g.m & m in dom f & n
in dom f & dom f = dom g & (for k be set st k<>m & k<>n & k in dom f holds f.k=
  g.k) holds f,g are_fiberwise_equipotent
proof
  let f,g be Function,m,n be set;
  assume that
A1: f.m=g.n and
A2: f.n=g.m and
A3: m in dom f and
A4: n in dom f and
A5: dom f = dom g and
A6: for k be set st k<>m & k<>n & k in dom f holds f.k=g.k;
  set t=id dom f, nm=n .--> m,mn=m .--> n, p=t +* nm +* mn;
A7: dom nm ={ n } by FUNCOP_1:13;
A8: dom t = dom f;
A9: rng t = dom (t") by FUNCT_1:33
    .= dom f by A8,FUNCT_1:45;
  dom mn ={ m } by FUNCOP_1:13;
  then
A10: dom p = dom (t +* nm) \/ {m} by FUNCT_4:def 1
    .= dom t \/ {n} \/ {m} by A7,FUNCT_4:def 1
    .= dom f \/ {n} \/ {m}
    .= dom f \/ {m} by A4,ZFMISC_1:40
    .= dom f by A3,ZFMISC_1:40;
A11: now
    let x be set;
    assume
A12: x in dom f;
    then
A13: (p*p).x=p.(p.x) by A10,FUNCT_1:13;
    per cases;
    suppose
A14:  x=m;
      hence (p*p).x=p.n by A13,FUNCT_4:89
        .=x by A14,FUNCT_4:90;
    end;
    suppose
A15:  x<>m;
      now
        per cases;
        suppose
A16:      x=n;
          hence (p*p).x=p.m by A13,FUNCT_4:90
            .=x by A16,FUNCT_4:89;
        end;
        suppose
A17:      x<>n;
          hence (p*p).x=p.(t.x) by A13,A15,FUNCT_4:91
            .=p.x by A12,FUNCT_1:17
            .=t.x by A15,A17,FUNCT_4:91
            .=x by A12,FUNCT_1:17;
        end;
      end;
      hence (p*p).x=x;
    end;
  end;
  rng nm ={m} by FUNCOP_1:8;
  then rng t \/ rng nm =dom f by A3,ZFMISC_1:40;
  then
A18: rng(t +* nm) \/ rng mn c= dom f \/ rng mn by FUNCT_4:17,XBOOLE_1:9;
  for z be set st z in rng(p*p) holds z in rng p by FUNCT_1:14;
  then
A19: rng(p*p) c= rng p by TARSKI:def 3;
A20: rng p c= rng(t +* nm) \/ rng mn by FUNCT_4:17;
A21: rng mn ={n} by FUNCOP_1:8;
  then dom f \/ rng mn =dom p by A4,A10,ZFMISC_1:40;
  then
A22: dom (p*p) =dom f by A10,A18,A20,RELAT_1:27,XBOOLE_1:1;
  then p*p=t by A11,FUNCT_1:17;
  then
A23: p is one-to-one by A10,FUNCT_1:31;
  rng p c= dom f \/ rng mn by A18,A20,XBOOLE_1:1;
  then
A24: rng p c= dom p by A4,A10,A21,ZFMISC_1:40;
  then
A25: dom (g*p) =dom f by A5,A10,RELAT_1:27;
  now
    let x be set;
    assume
A26: x in dom f;
    then
A27: (g*p).x=g.(p.x) by A25,FUNCT_1:12;
    per cases;
    suppose
      x=m;
      hence (g*p).x=f.x by A1,A27,FUNCT_4:89;
    end;
    suppose
A28:  x<>m;
      now
        per cases;
        suppose
          x=n;
          hence (g*p).x=f.x by A2,A27,FUNCT_4:90;
        end;
        suppose
A29:      x<>n;
          hence (g*p).x=g.(t.x) by A27,A28,FUNCT_4:91
            .=g.x by A26,FUNCT_1:17
            .=f.x by A6,A26,A28,A29;
        end;
      end;
      hence (g*p).x=f.x;
    end;
  end;
  then
A30: f=g*p by A25,FUNCT_1:2;
  rng(p*p)=dom f by A9,A22,A11,FUNCT_1:17;
  then rng p = dom g by A5,A10,A24,A19,XBOOLE_0:def 10;
  hence thesis by A10,A23,A30,CLASSES1:77;
end;

:: form BINARITH, 2008.08.20, A.T.

theorem
  for D being non empty set, f being FinSequence of D, k being Nat holds
  len (f/^k)=len f-'k
proof
  let D be non empty set, f be FinSequence of D,k be Nat;
  per cases;
  suppose
A1: k<=len f;
    then len f-'k=len f-k by XREAL_1:233;
    hence thesis by A1,Def1;
  end;
  suppose
A2: k>len f;
    then (f/^k)=<*>D by Def1;
    then
A3: len (f/^k)=0;
    len f-k<0 by A2,XREAL_1:49;
    hence thesis by A3,XREAL_0:def 2;
  end;
end;

:: from SCPQSORT, 2008.10.12, A.T.

theorem Th30: :: RFINSEQ:17
  for f,g be FinSequence,x be set st x in dom g & f,g
  are_fiberwise_equipotent holds ex y be set st y in dom g & f.x=g.y
proof
  let f,g be FinSequence,x be set;
  assume that
A1: x in dom g and
A2: f,g are_fiberwise_equipotent;
  consider P be Permutation of dom g such that
A3: f = g*P by A2,Th4;
  take y=P.x;
  thus y in dom g by A1,FUNCT_2:5;
  thus thesis by A1,A3,FUNCT_2:15;
end;

theorem Th31:
  for f,g,h be FinSequence holds f,g are_fiberwise_equipotent iff
  h^f, h^g are_fiberwise_equipotent
proof
  let f,g,h be FinSequence;
  thus f,g are_fiberwise_equipotent implies h^f, h^g are_fiberwise_equipotent
  proof
    assume
A1: f,g are_fiberwise_equipotent;
    now
      let y be set;
      card Coim(f,y) = card Coim(g,y) by A1,CLASSES1:def 9;
      hence card Coim(h^f,y) = card(g"{y}) + card(h"{y}) by FINSEQ_3:57
        .= card Coim(h^g,y) by FINSEQ_3:57;
    end;
    hence thesis by CLASSES1:def 9;
  end;
  assume
A2: h^f,h^g are_fiberwise_equipotent;
  now
    let x be set;
A3: card Coim(h^f,x) = card Coim(f,x)+card(h"{x}) & card((h^g)"{x}) =
    card(g"{x} )+card(h"{x}) by FINSEQ_3:57;
    card Coim(h^f,x) = card Coim(h^g,x) by A2,CLASSES1:def 9;
    hence card Coim(f,x) = card Coim(g,x) by A3;
  end;
  hence thesis by CLASSES1:def 9;
end;

theorem
  for f,g be FinSequence,m,n,j be Element of NAT st f,g
are_fiberwise_equipotent & m<=n & n <= len f & (for i be Element of NAT st 1<=i
& i<=m holds f.i=g.i) & (for i be Element of NAT st n<i & i<=len f holds f.i=g.
  i) & m<j & j<=n holds ex k be Element of NAT st m<k & k<=n & f.j=g.k
proof
  let f,g be FinSequence,m,n,j be Element of NAT;
  assume
A1: f,g are_fiberwise_equipotent;
  assume that
A2: m<=n and
A3: n <= len f;
  assume
A4: for i be Element of NAT st 1<=i & i<=m holds f.i=g.i;
  reconsider m3=len f-n as Element of NAT by A3,INT_1:3,XREAL_1:48;
  len g=n+m3 by A1,Th3;
  then consider s2,r2 be FinSequence such that
A5: len s2 = n and
A6: len r2 = m3 and
A7: g = s2^r2 by FINSEQ_2:22;
A8: len f=n+m3;
  then consider s1,r1 be FinSequence such that
A9: len s1 = n and
A10: len r1 = m3 and
A11: f = s1^r1 by FINSEQ_2:22;
A12: dom r1 = Seg m3 by A10,FINSEQ_1:def 3;
  assume
A13: for i be Element of NAT st n<i & i<=len f holds f.i=g.i;
  now
    let i be Nat;
    reconsider a = i as Element of NAT by ORDINAL1:def 12;
A14: n < n+1 by XREAL_1:29;
    assume
A15: i in dom r1;
    then
A16: i in dom r2 by A6,A12,FINSEQ_1:def 3;
    1 <= i by A12,A15,FINSEQ_1:1;
    then n+1 <= n+i by XREAL_1:6;
    then
A17: n< i+n by A14,XXREAL_0:2;
    i <= m3 by A12,A15,FINSEQ_1:1;
    then
A18: len s1+i <= len f by A8,A9,XREAL_1:6;
    thus r1.i=f.(len s1+i) by A11,A15,FINSEQ_1:def 7
      .=g.(len s2+a) by A13,A9,A5,A17,A18
      .=r2.i by A7,A16,FINSEQ_1:def 7;
  end;
  then r1=r2 by A10,A6,FINSEQ_2:9;
  then
A19: s1,s2 are_fiberwise_equipotent by A1,A11,A7,Th1;
  reconsider m2=n-m as Element of NAT by A2,INT_1:3,XREAL_1:48;
A20: m+1 > m by XREAL_1:29;
  len s2=m+m2 by A5;
  then consider p2,q2 be FinSequence such that
A21: len p2 = m and
A22: len q2 = m2 and
A23: s2 = p2^q2 by FINSEQ_2:22;
A24: Seg m = dom p2 by A21,FINSEQ_1:def 3;
  len s1=m+m2 by A9;
  then consider p1,q1 be FinSequence such that
A25: len p1 = m and
A26: len q1 = m2 and
A27: s1 = p1^q1 by FINSEQ_2:22;
A28: f=p1^(q1^r1) by A11,A27,FINSEQ_1:32;
A29: dom p1 = Seg m by A25,FINSEQ_1:def 3;
A30: g=p2^(q2^r2) by A7,A23,FINSEQ_1:32;
  now
    let i be Nat;
    reconsider a = i as Element of NAT by ORDINAL1:def 12;
    assume
A31: i in dom p1;
    then
A32: 1<= i & i <= m by A29,FINSEQ_1:1;
    thus p1.i=f.i by A28,A31,FINSEQ_1:def 7
      .=g.a by A4,A32
      .=p2.i by A30,A24,A29,A31,FINSEQ_1:def 7;
  end;
  then p1=p2 by A25,A21,FINSEQ_2:9;
  then
A33: q1,q2 are_fiberwise_equipotent by A27,A23,A19,Th31;
  assume that
A34: m<j and
A35: j<=n;
  j-len p1 > 0 by A34,A25,XREAL_1:50;
  then reconsider x=j-len p1 as Element of NAT by INT_1:3;
A36: x <= n-len p1 by A35,XREAL_1:9;
A37: Seg m2 = dom q2 by A22,FINSEQ_1:def 3;
A38: 1+ 0<= x by A34,A25,INT_1:7,XREAL_1:50;
  then x in dom q2 by A25,A37,A36,FINSEQ_1:1;
  then consider y be set such that
A39: y in dom q2 and
A40: q1.x=q2.y by A33,Th30;
  reconsider y as Element of NAT by A39;
A41: len p2 + y in dom s2 by A23,A39,FINSEQ_1:28;
  reconsider k=len p2+y as Element of NAT by ORDINAL1:def 12;
  take k;
  1<=y by A37,A39,FINSEQ_1:1;
  then k>=len p2+1 by XREAL_1:6;
  hence m<k by A21,A20,XXREAL_0:2;
  y<=m2 by A37,A39,FINSEQ_1:1;
  then k <= m2+len p2 by XREAL_1:6;
  hence k<=n by A21;
  Seg m2 = dom q1 by A26,FINSEQ_1:def 3;
  then
A42: x in dom q1 by A25,A38,A36,FINSEQ_1:1;
  then len p1 + x in dom s1 by A27,FINSEQ_1:28;
  hence f.j=s1.(len p1+x) by A11,FINSEQ_1:def 7
    .=q2.y by A27,A40,A42,FINSEQ_1:def 7
    .=s2.(len p2+y) by A23,A39,FINSEQ_1:def 7
    .=g.k by A7,A41,FINSEQ_1:def 7;
end;

theorem
  for t being FinSequence of INT holds ex u being FinSequence of REAL
  st t,u are_fiberwise_equipotent & u is FinSequence of INT
  & u is non-increasing
proof
  let t be FinSequence of INT;
  t is FinSequence of REAL by FINSEQ_3:117;
  then consider u be non-increasing FinSequence of REAL such that
A1: t,u are_fiberwise_equipotent by Th22;
  take u;
  thus t,u are_fiberwise_equipotent by A1;
  rng t = rng u by A1,CLASSES1:75;
  hence u is FinSequence of INT by FINSEQ_1:def 4;
  thus thesis;
end;