:: Euler's Polyhedron Formula
::  by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies FINSET_1, FUNCT_1, FUNCT_2, CARD_1, SUBSET_1, TARSKI, BOOLE,
      RELAT_1, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, RLVECT_1, GROUP_1, ARYTM_1,
      FINSEQ_1, FINSEQ_2, QC_LANG1, RLSUB_1, BSPACE, RANKNULL, RLVECT_3,
      MATRLIN, FINSEQ_4, POLYFORM, VECTSP10, SEQ_1, PRALG_1, MATRIX_2, POWER,
      FUNCOP_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
      FUNCT_1, RELSET_1, PARTFUN1, WELLORD2, MCART_1, FUNCT_2, FUNCT_3,
      BINOP_1, NUMBERS, ORDINAL1, ORDINAL2, ARYTM_3, FUNCOP_1, FINSET_1,
      SETWISEO, XCMPLX_0, COMPLEX1, XXREAL_0, REAL_1, NAT_1, INT_1, CARD_1,
      CARD_2, FINSEQ_1, SEQ_1, FINSEQ_2, MCART_2, FINSEQ_4, POWER, FINSOP_1,
      RVSUM_1, NEWTON, WSIERP_1, REALSET1, ABIAN, STRUCT_0, LATTICES, RLVECT_1,
      GROUP_1, ALGSTR_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
      MOD_2, FVSUM_1, GR_CY_1, MATRLIN, VECTSP_9, RANKNULL, BSPACE;
 constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1, ZFMISC_1,
      SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL1, ORDINAL2,
      RLVECT_1, LATTICES, GROUP_1, VECTSP_1, VECTSP_9, INT_1, STRUCT_0,
      BINOP_1, MCART_2, FRAENKEL, ENUMSET1, RELSET_1, PARTFUN1, REALSET1,
      FINSEQ_1, FINSOP_1, XXREAL_0, FINSEQ_2, FVSUM_1, SETWOP_2, WELLORD2,
      SETWISEO, ALGSTR_1, VECTSP_4, BSPACE, SETFAM_1, RELAT_2, PBOOLE, REAL_1,
      COMPLEX1, INT_2, BINOP_2, FINSEQOP, NAT_D, GROUP_2, GROUP_3, GROUP_4,
      MATRIX_2, WELLORD1, FUNCT_3, RANKNULL, MOD_2, VECTSP_6, VECTSP_7,
      MATRLIN, FINSEQ_4, RFINSEQ, VECTSP_5, NEWTON, WSIERP_1, RVSUM_1, GR_CY_1,
      FUNCOP_1, ABIAN, ARYTM_3, POWER, XREAL_0, SEQ_1, CARD_2, INT_3, XCMPLX_0;
 registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1,
      SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0, RLVECT_1, RELSET_1, FVSUM_1,
      FINSEQ_1, REALSET1, FINSEQ_2, SETWISEO, VECTSP_4, ZFMISC_1, RANKNULL,
      MOD_2, VECTSP_7, CARD_1, MATRLIN, BSPACE, VECTSP_9, FINSEQ_4, RFINSEQ,
      ORDINAL1, ORDINAL2, VECTSP_5, NEWTON, RVSUM_1, GR_CY_1, FUNCOP_1,
      FUNCT_7, POLYNOM1, ABIAN, ARYTM_3, XREAL_0, SEQ_1, NUMBERS, JORDAN23,
      INT_3, INT_2, ARMSTRNG, GOBRD13, XCMPLX_0, PARTFUN1, XXREAL_0, GROUP_1,
      FINSUB_1, ALGSTR_1;
 requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
 definitions XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, MCART_2, ENUMSET1,
      RLVECT_1, BINOP_1, STRUCT_0, GROUP_1, VECTSP_1, TARSKI, REALSET1,
      FVSUM_1, FINSEQ_1, ZFMISC_1, FINSEQ_2, VECTSP_4, BSPACE, RANKNULL, MOD_2,
      VECTSP_6, VECTSP_7, CARD_1, MATRLIN, VECTSP_9, FUNCT_3, FINSEQ_4,
      RFINSEQ, ORDINAL1, ORDINAL2, VECTSP_5, NEWTON, WSIERP_1, RVSUM_1,
      GR_CY_1, FUNCOP_1, ABIAN, ARYTM_3, INT_1, POWER, XREAL_0, SEQ_1, CARD_2,
      INT_3, INT_2;
 theorems XBOOLE_0, FUNCT_1, RELAT_1, XBOOLE_1, TARSKI, ZFMISC_1, FUNCT_2,
      GROUP_1, RLVECT_1, VECTSP_1, FVSUM_1, FINSEQ_2, CARD_1, FINSEQ_1, NAT_1,
      FINSOP_1, VECTSP_4, BSPACE, RANKNULL, VECTSP_9, ORDINAL1, NEWTON,
      RVSUM_1, GR_CY_1, FUNCOP_1, XREAL_1, XXREAL_0, INT_1, JORDAN16, POWER,
      FIB_NUM2, SEQ_1, NUMBERS, CARD_2, PRE_CIRC, FINSEQ_3, SUBSET_1, MOD_2,
      MATRIX_3, CALCUL_1, PARTFUN1;
 schemes FUNCT_2, FINSEQ_1, FINSEQ_2;

begin

theorem Th1:
for X,c,d being set
  st (ex a,b being set st a <> b & X = {a,b}) &
     c in X &
     d in X &
     c <> d
  holds X = {c,d}
proof
  let X,c,d be set such that
    A1: ex a,b being set st a <> b & X = {a,b} and
    A2: c in X and
    A3: d in X and
    A4: c <> d;
  consider a,b being set such that
    a <> b and
    A5: X = {a,b} by A1;
  A6: {c,d} c= X by A2,A3,ZFMISC_1:38;
  X c= {c,d}
  proof
    A7: c = a or c = b by A2,A5,TARSKI:def 2;
    A8: d = a or d = b by A3,A5,TARSKI:def 2;
    let x be set such that
      A9: x in X;
    per cases by A5,A9,TARSKI:def 2;
    suppose x = a;
      hence thesis by A4,A7,A8,TARSKI:def 2;
    end;
    suppose x = b;
      hence thesis by A4,A7,A8,TARSKI:def 2;
    end;
  end;
  hence thesis by A6,XBOOLE_0:def 10;
end;

theorem Th2:
for f being Function st f is one-to-one
  holds Card (dom f) = Card (rng f)
proof
  let f be Function such that
    A1: f is one-to-one;
  A2: dom f, f .: (dom f) are_equipotent by A1,CARD_1:60;
  f .: (dom f) = rng f by RELAT_1:146;
  hence thesis by A2,CARD_1:21;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Arithmetical Preliminaries
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

reserve n for Nat,
        k for Integer;

theorem Th3:
1 <= k implies k is Nat
proof
  assume A1: 1 <= k;
  reconsider k as Element of NAT by A1,INT_1:16;
  k is Nat;
  hence thesis;
end;

definition
  let a be Integer,
      b be Nat;
  redefine func
    a*b -> Element of INT;
  coherence by INT_1:def 2;
end;

theorem Th4:
1 is odd
proof
  1 = 2*0 + 1;
  hence thesis;
end;

theorem Th5:
2 is even
proof
  2 = 2*1;
  hence thesis;
end;

theorem Th6:
3 is odd
proof
  3 = 2*1 + 1;
  hence thesis;
end;

theorem Th7:
4 is even
proof
  4 = 2*2;
  hence thesis;
end;

theorem Th8:
n is even implies (-1)|^n = 1
proof
  assume A1: n is even;
  reconsider n as Element of NAT by ORDINAL1:def 13;
  (-1)|^n = (-1) to_power n by POWER:48;
  hence thesis by A1,FIB_NUM2:5;
end;

theorem Th9:
n is odd implies (-1)|^n = -1
proof
  assume A1: n is odd;
  reconsider n as Element of NAT by ORDINAL1:def 13;
  (-1)|^n = (-1) to_power n by POWER:46;
  hence thesis by A1,FIB_NUM2:3;
end;

theorem Th10:
(-1) |^ n is Integer
proof
  per cases;
  suppose n is even;
    hence thesis by Th8;
  end;
  suppose n is odd;
    hence thesis by Th9;
  end;
end;

definition
  let a be Integer,
      n be Nat;
  redefine func
    a |^ n -> Element of INT;
  coherence
  proof
    consider b being Element of NAT such that
      A1: a = b or a = -b by INT_1:8;
    per cases by A1;
    suppose A2: a = b;
      reconsider a as Element of NAT by A2;
      reconsider s = a |^ n as Element of NAT by ORDINAL1:def 13;
      s in NAT;
      hence thesis by NUMBERS:17;
    end;
    suppose A3: a = -b;
      A4: -b = (-1)*b;
      reconsider bn = b |^ n as Element of NAT by ORDINAL1:def 13;
      A5: (-1) |^n is Integer by Th10;
      reconsider l = (-1) |^ n as Element of INT by A5,INT_1:def 2;
      a |^ n = l*bn by A3,A4,NEWTON:12;
      hence thesis;
    end;
  end;
end;

Lm1: for x being Element of NAT st 0 < x holds 0+1 <= x by NAT_1:13;

theorem Th11:
for p,q,r being FinSequence holds
  len (p ^ q) <= len (p ^ (q ^ r))
proof
  let p,q,r be FinSequence;
  len ((p ^ q) ^ r) = len (p ^ (q ^ r)) by FINSEQ_1:45;
  hence thesis by CALCUL_1:6;
end;

theorem Th12:
1 < n + 2
proof
  0 < n + 1 implies 1 < n + 2
  proof
    assume 0 < n + 1;
    0 + 1 = 1;
    hence thesis by XREAL_1:10;
  end;
  hence thesis;
end;

theorem Th13:
(-1)|^2 = 1
proof
  (-1)|^2 = (-1)|^(1+1)
         .= ((-1)|^1)*((-1)|^1) by NEWTON:13
         .= ((-1)|^1)*(-1) by NEWTON:10
         .= (-1)*(-1) by NEWTON:10;
  hence thesis;
end;

theorem Th14:
for n being Nat
  holds (-1)|^n = (-1)|^(n+2)
proof
  let n be Nat;
  (-1)|^(n+2) = ((-1)|^n)*((-1)|^2) by NEWTON:13
             .= (-1)|^n by Th13;
  hence thesis;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries on Finite Sequences
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

registration
  let f be FinSequence of INT,
      k be Nat;
  cluster f.k -> integer;
  coherence
  proof
    per cases;
    suppose k in dom f;
      then f.k = f/.k by PARTFUN1:def 8;
      hence thesis;
    end;
    suppose not k in dom f;
      hence thesis by FUNCT_1:def 4;
    end;
  end;
end;

:: A theorem on telescoping sequences of integers.
theorem Th15:
for a,b,s being FinSequence of INT
  st len s > 0 &
     len a = len s &
     len b = len s &
     (for n being Nat
        st 1 <= n & n <= len s
        holds s.n = a.n + b.n) &
     (for k being Nat
        st 1 <= k & k < len s
        holds b.k = -(a.(k+1)))
  holds Sum s = (a.1) + (b.(len s))
proof
  let a,b,s be FinSequence of INT such that
    A1: len s > 0 and
    A2: len a = len s and
    A3: len b = len s and
    A4: for n being Nat
        st 1 <= n & n <= len s
        holds s.n = a.n + b.n and
    A5: for k being Nat
          st 1 <= k & k < len s
          holds b.k = -(a.(k+1));
  defpred P[FinSequence of INT] means
    len $1 > 0 implies
      for a,b being FinSequence of INT
        st len a = len $1 &
           len b = len $1 &
           (for n being Nat
             st 1 <= n & n <= len $1
             holds $1.n = a.n + b.n) &
           (for k being Nat
             st 1 <= k & k < len $1
             holds b.k = -(a.(k+1)))
        holds Sum $1 = a.1 + b.(len $1);
  A6: P[<*>INT] by FINSEQ_1:32;
  A7: for p being FinSequence of INT,
          x being Element of INT
         st P[p]
        holds P[p^<*x*>]
  proof
    let p be FinSequence of INT,
        x be Element of INT such that
      A8: P[p];
    set t = p ^ <*x*>;
    assume len t > 0; :: this is outright provable, of course
    let a,b be FinSequence of INT such that
      A9: len a = len t and
      A10: len b = len t  and
      A11: for n being Nat
            st 1 <= n & n <= len t
            holds t.n = a.n + b.n and
      A12: for k being Nat
            st 1 <= k & k < len t
            holds b.k = -(a.(k+1));
    A13: Sum t = (Sum p) + x by GR_CY_1:20;
    per cases;
    suppose A14: len p = 0;
      A15: Sum p = 0 by A14,FINSEQ_1:25,GR_CY_1:22;
      A16: t = <*x*>
      proof
        p = {} by A14,FINSEQ_1:25;
        hence thesis by FINSEQ_1:47;
      end;
      A17: len t = 1 by A16,FINSEQ_1:56;
      reconsider egy = 1 as Nat;
      A18: egy <= len t by A16,FINSEQ_1:56;
      t.egy = a.egy + b.egy by A11,A18;
      hence thesis by A13,A15,A16,A17,FINSEQ_1:57;
    end;
    suppose A19: len p > 0;
      set m = len p;
      set a' = a|m;
      set b' = b|m;
      A20: m <= len a & m <= len b by A9,A10,CALCUL_1:6;
      A21: len a' = len p by A20,FINSEQ_1:80;
      A22: len b' = len p by A20,FINSEQ_1:80;
      A23: for n being Nat
            st 1 <= n & n <= len p
            holds p.n = a'.n + b'.n
      proof
        let n be Nat such that
          A24: 1 <= n and
          A25: n <= len p;
        A26: len p <= len t by CALCUL_1:6;
        A27: n <= len t by A25,A26,XXREAL_0:2;
        A28: dom p = Seg len p by FINSEQ_1:def 3;
        A29: n in dom p by A24,A25,A28,FINSEQ_1:3;
        reconsider n as Element of NAT by ORDINAL1:def 13;
        p.n = t.n by A29,FINSEQ_1:def 7
           .= a.n + b.n by A11,A24,A27
           .= a'.n + b.n by A25,FINSEQ_3:121
           .= a'.n + b'.n by A25,FINSEQ_3:121;
        hence thesis;
      end;
      A30: for n being Nat
            st 1 <= n & n < len p
            holds b'.n = -(a'.(n+1))
      proof
        let n be Nat such that
          A31: 1 <= n and
          A32: n < len p;
        reconsider n as Element of NAT by ORDINAL1:def 13;
        A33: b'.n = b.n by A32,FINSEQ_3:121;
        A34: n + 1 <= len p by A32,INT_1:20;
        A35: len p <= len t by CALCUL_1:6;
        A36: n < len t by A32,A35,XXREAL_0:2;
        a'.(n+1) = a.(n+1) by A34,FINSEQ_3:121;
        hence thesis by A12,A31,A33,A36;
      end;
      A37: Sum p = a'.1 + b'.(len p) by A8,A19,A21,A22,A23,A30;
      A38: a'.1 = a.1
      proof
        reconsider egy = 1 as Element of NAT;
        A39: 0 + 1 = 1;
        egy <= len p by A19,A39,INT_1:20;
        hence thesis by FINSEQ_3:121;
      end;
      x = -(b'.(len p)) + b.(len t)
      proof
        A40: len t = (len p) + 1
        proof
          len <*x*> = 1 by FINSEQ_1:56;
          hence thesis by FINSEQ_1:35;
        end;
        A41: 1 <= len t
        proof
          0 + 1 = 1;
          hence thesis by A40,XREAL_1:8;
        end;
        A42: a.(len t) = -(b'.(len p))
        proof
          A43: len p < len t
          proof
            0 + len p = len p;
            hence thesis by A40,XREAL_1:8;
          end;
          A44: 1 <= len p by A19,Lm1;
          A45: b.(len p) = -(a.(len p + 1)) by A12,A43,A44;
          b.(len p) = b'.(len p) by FINSEQ_3:121;
          hence thesis by A40,A45;
        end;
        x = t.(len p + 1) by FINSEQ_1:59
         .= -(b'.(len p)) + b.(len t) by A11,A40,A41,A42;
        hence thesis;
      end;
      hence thesis by A13,A37,A38;
    end;
  end;
  for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A6,A7);
  hence thesis by A1,A2,A3,A4,A5;
end;

theorem Th16:
for p,q,r being FinSequence holds
  len (p ^ q ^ r) = (len p) + (len q) + (len r)
proof
  let p,q,r be FinSequence;
  len (p ^ q ^ r) = (len (p ^ q)) + (len r) by FINSEQ_1:35
                 .= ((len p) + (len q)) + (len r) by FINSEQ_1:35;
  hence thesis;
end;

theorem Th17:
for x being set,
    p,q being FinSequence
  holds (<*x*> ^ p ^ q).1 = x
proof
  let x be set,
      p,q be FinSequence;
  <*x*> ^ p ^ q = <*x*> ^ (p ^ q) by FINSEQ_1:45;
  hence thesis by FINSEQ_1:58;
end;

theorem Th18:
for x being set,
    p,q being FinSequence
  holds (p ^ q ^ <*x*>).((len p) + (len q) + 1) = x
proof
  let x be set,
      p,q be FinSequence;
  set s = p ^ q;
  (s ^ <*x*>).((len s) + 1) = x by FINSEQ_1:59;
  hence thesis by FINSEQ_1:35;
end;

theorem Th19:
for p,q,r being FinSequence,
    k being Nat
  st len p < k & k <= len (p ^ q)
  holds (p ^ q ^ r).k = q.(k - (len p))
proof
  let p,q,r be FinSequence,
      k be Nat such that
    A1: len p < k and
    A2: k <= len (p ^ q);
  A3: len (p ^ q) <= len (p ^ (q ^ r)) by Th11;
  A4: k <= len (p ^ (q ^ r)) by A2,A3,XXREAL_0:2;
  A5: (p ^ (q ^ r)).k = (q ^ r).(k - (len p)) by A1,A4,FINSEQ_1:37;
  set n = k - (len p);
  A6: (len p) - (len p) = 0;
  A7: 0 < n by A1,A6,XREAL_1:11;
  A8: 0 + 1 = 1;
  A9: 1 <= n by A7,A8,INT_1:20;
  reconsider n as Nat by A9,Th3;
  A10: k <= (len p) + (len q) by A2,FINSEQ_1:35;
  A11: n <= len q
  proof
    ((len p) + (len q)) - (len p) = len q;
    hence thesis by A10,XREAL_1:11;
  end;
  A12: n in Seg (len q) by A9,A11,FINSEQ_1:3;
  A13: n in dom q by A12,FINSEQ_1:def 3;
  reconsider n as Element of NAT by ORDINAL1:def 13;
  (q ^ r).n = q.n by A13,FINSEQ_1:def 7;
  hence thesis by A5,FINSEQ_1:45;
end;

definition
  let a be Integer;
  redefine func
    <*a*> -> FinSequence of INT;
  coherence
  proof
    set s = <*a*>;
    A1: rng s = {a} by FINSEQ_1:55;
    A2: a in INT by INT_1:def 2;
    {a} c= INT by A2,ZFMISC_1:37;
    hence thesis by A1,FINSEQ_1:def 4;
  end;
end;

definition
  let a,b be Integer;
  redefine func
    <*a,b*> -> FinSequence of INT;
  coherence
  proof
    set s = <*a,b*>;
    A1: rng s = {a,b} by FINSEQ_2:147;
    {a,b} c= INT
    proof
      a in INT & b in INT by INT_1:def 2;
      hence thesis by ZFMISC_1:38;
    end;
    hence thesis by A1,FINSEQ_1:def 4;
  end;
end;

definition
  let a,b,c be Integer;
  redefine func
    <*a,b,c*> -> FinSequence of INT;
  coherence
  proof
    set s = <*a,b,c*>;
    A1: rng s = {a,b,c} by FINSEQ_2:148;
    {a,b,c} c= INT
    proof
      A2: a in INT by INT_1:def 2;
      A3: b in INT by INT_1:def 2;
      c in INT by INT_1:def 2;
      hence thesis by A2,A3,JORDAN16:2;
    end;
    hence thesis by A1,FINSEQ_1:def 4;
  end;
end;

definition
  let p,q be FinSequence of INT;
  redefine func
    p ^ q -> FinSequence of INT;
  coherence by FINSEQ_1:96;
end;

theorem Th20:
for p,q being FinSequence of INT
  holds Sum (p ^ q) = (Sum p) + (Sum q)
proof
  let p,q be FinSequence of INT;
  A1: rng p c= REAL by NUMBERS:15,XBOOLE_1:1;
  A2: rng q c= REAL by NUMBERS:15,XBOOLE_1:1;
  reconsider p,q as real-yielding FinSequence by A1,A2,SEQ_1:def 1;
  Sum (p ^ q) = (Sum p) + (Sum q) by RVSUM_1:105;
  hence thesis;
end;

theorem Th21:
for k being Integer,
    p being FinSequence of INT
  holds Sum (<*k*> ^ p) = k + (Sum p)
proof
  let k be Integer,
      p be FinSequence of INT;
  reconsider k as Element of INT by INT_1:def 2;
  Sum (<*k*> ^ p) = (Sum p) + (Sum <*k*>) by Th20
                 .= Sum (p ^ <*k*>) by Th20
                 .= k + (Sum p) by GR_CY_1:20;
  hence thesis;
end;

theorem Th22:
for p,q,r being FinSequence of INT
  holds Sum (p ^ q ^ r) = (Sum p) + (Sum q) + (Sum r)
proof
  let p,q,r be FinSequence of INT;
  Sum (p ^ q ^ r) = (Sum (p ^ q)) + (Sum r) by Th20
                 .= ((Sum p) + (Sum q)) + Sum r by Th20;
  hence thesis;
end;

theorem
for a being Element of Z_2
  holds Sum <*a*> = a by FINSOP_1:12;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Polyhedra and Incidence Matrices
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

:: An incidence matrix is a function that says of any two objects
:: (contained in some set) whether they are incidence to each other.
definition
  let X,Y be set;
  mode
    incidence-matrix of X,Y
  is
    Element of Funcs([:X,Y:],{0.Z_2,1.Z_2});
end;

theorem Th24:
for X,Y being set
  holds [:X,Y:] --> 1.Z_2 is incidence-matrix of X,Y
proof
  let X,Y be set;
  set f = [:X,Y:] --> 1.Z_2;
  A1: dom f = [:X,Y:] by FUNCOP_1:19;
  A2: rng f c= {1.Z_2} by FUNCOP_1:19;
  A3: {1.Z_2} c= {0.Z_2,1.Z_2} by ZFMISC_1:12;
  rng f c= {0.Z_2,1.Z_2} by A2,A3,XBOOLE_1:1;
  hence thesis by A1,FUNCT_2:def 2;
end;

:: A polyhedron (one might call it an abstract polyhedron) consists of
:: two pieces of data: a sequence of ordered sets, representing the
:: polytope sets (they are ordered for convenience's sake) and a
:: sequence of incidence matrices, which lays out the incidence
:: relation between the (k-1)-polytopes and the k-polytopes.
definition
  mode
    polyhedron
  means :Def1:
    ex F being FinSequence-yielding FinSequence,
       I being Function-yielding FinSequence st
   len I = len F - 1 &
   (for n being Nat
     st 1 <= n & n < len F
     holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
   (for n being Nat
      st 1 <= n & n <= len F
      holds F.n is non empty & F.n is one-to-one) &
   it = [F,I];
  existence
  proof
    reconsider F = <*<*{}*>*> as FinSequence-yielding FinSequence;
    reconsider I = <*>{} as Function-yielding FinSequence;
    A1: len F = 1 by FINSEQ_1:56;
    A2: len I = 1-1 by FINSEQ_1:32;
    A3: for n being Nat
          st 1 <= n & n < 1
          holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1));
    A4: for n being Nat
          st 1 <= n & n <= 1
          holds F.n is non empty & F.n is one-to-one
    proof
      let n be Nat such that
        A5: 1 <= n and
        A6: n <= 1;
      n = 1 by A5,A6,XXREAL_0:1;
      hence thesis by FINSEQ_1:def 8;
    end;
    take [F,I];
    thus thesis by A1,A2,A3,A4;
  end;
end;

reserve p for polyhedron,
        k for Integer,
        n for Nat;

:: The dimension dim(p) of a polyhedron p is just the number of
:: polytope sets that it has.
definition
  let p be polyhedron;
  func
    dim(p) -> Element of NAT
  means :Def2:
    ex F being FinSequence-yielding FinSequence,
       I being Function-yielding FinSequence
     st len I = len F - 1 &
         (for n being Nat
            st 1 <= n & n < len F
            holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
         (for n being Nat
            st 1 <= n & n <= len F
            holds F.n is non empty & F.n is one-to-one) &
         p = [F,I] &
         it = len F;
  existence
  proof
    consider F being FinSequence-yielding FinSequence,
             I being Function-yielding FinSequence such that
      A1: len I = len F - 1 and
      A2: for n being Nat
            st 1 <= n & n < len F
            holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
      A3: for n being Nat
            st 1 <= n & n <= len F
            holds F.n is non empty & F.n is one-to-one and
      A4: p = [F,I] by Def1;
    take len F;
    thus thesis by A1,A2,A3,A4;
  end;
  uniqueness by ZFMISC_1:33;
end;

:: For integers k such that 0 <= k <= dim(p), the set of k-polytopes
:: is data already given by the polyhedron.  For k = dim(p), the set
:: is the singleton {p}, which seems clear enough.  For k = -1, it is
:: convenient to define the set of k-polytopes to be {{}}.  Doing this
:: ensures that, if p is simply connected, then any two vertices are
:: connected by a system of edges.
::
:: For k < -1 and k > dim(p), the set of k-polytopes of p is empty.
definition
  let p be polyhedron,
      k be Integer;
  func
    k-polytopes(p) -> finite set
  means :Def3:
    (k < -1 implies it = {}) &
    (k = -1 implies it = {{}}) &
    (-1 < k & k < dim(p) implies
     ex F being FinSequence-yielding FinSequence,
        I being Function-yielding FinSequence
      st len I = len F - 1 &
         (for n being Nat
            st 1 <= n & n < len F
            holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
         (for n being Nat
            st 1 <= n & n <= len F
            holds F.n is non empty & F.n is one-to-one) &
         p = [F,I] &
         it = rng (F.(k+1))) &
    (k = dim(p) implies it = {p}) &
    (k > dim(p) implies it = {});
  existence
  proof
    consider F being FinSequence-yielding FinSequence,
             I being Function-yielding FinSequence such that
      A1: len I = len F - 1 and
      A2: for n being Nat
            st 1 <= n & n < len F
            holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
      A3: for n being Nat
            st 1 <= n & n <= len F
            holds F.n is non empty & F.n is one-to-one and
      A4: p = [F,I] by Def1;
    per cases by XXREAL_0:1;
    suppose A5: k < -1;
      take {};
      thus thesis by A5;
    end;
    suppose A6: k = -1;
      take {{}};
      thus thesis by A6;
    end;
    suppose A7: -1 < k & k < dim(p);
      A8: -1 + 1 = 0;
      A9: 0 <= k by A7,A8,INT_1:20;
      reconsider k as Element of NAT by A9,INT_1:16;
      set n = k + 1;
      reconsider Fn = F.n as FinSequence;
      take rng Fn;
      thus thesis by A1,A2,A3,A4,A7;
    end;
    suppose A10: k = dim(p);
      take {p};
      thus thesis by A10;
    end;
    suppose A11: k > dim(p);
      take {};
      thus thesis by A11;
    end;
  end;
  uniqueness
  proof
    let X,Y be finite set such that
      A12: k < -1 implies X = {} and
      A13: k = -1 implies X = {{}} and
      A14: (-1 < k & k < dim(p)) implies
            ex F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence
             st len I = len F - 1 &
                (for n being Nat
                   st 1 <= n & n < len F
                   holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
                (for n being Nat
                   st 1 <= n & n <= len F
                   holds F.n is non empty & F.n is one-to-one) &
                p = [F,I] &
                X = rng (F.(k+1)) and
      A15: k = dim(p) implies X = {p} and
      A16: k > dim(p) implies X = {} and
      A17: k < -1 implies Y = {} and
      A18: k = -1 implies Y = {{}} and
      A19: (-1 < k & k < dim(p)) implies
            ex F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence
             st len I = len F - 1 &
                (for n being Nat
                   st 1 <= n & n < len F
                   holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
                (for n being Nat
                   st 1 <= n & n <= len F
                   holds F.n is non empty & F.n is one-to-one) &
                p = [F,I] &
                Y = rng (F.(k+1)) and
       A20: k = dim(p) implies Y = {p} and
       A21: k > dim(p) implies Y = {};
    per cases by XXREAL_0:1;
    suppose k < -1;
      hence thesis by A12,A17;
    end;
    suppose k = -1;
      hence thesis by A13,A18;
    end;
    suppose A22: -1 < k & k < dim(p);
      consider dX being Nat,
               FX being FinSequence-yielding FinSequence,
               IX being Function-yielding FinSequence such that
        len FX = dX and
        len IX = dX - 1 and
        for n being Nat
          st 1 <= n & n < dX
          holds IX.n is incidence-matrix of rng (FX.n),rng (FX.(n+1)) and
        for n being Nat
          st 1 <= n & n <= dX
          holds FX.n is non empty & FX.n is one-to-one and
        A23: p = [FX,IX] and
        A24: X = rng (FX.(k+1)) by A14,A22;
      consider dY being Nat,
               FY being FinSequence-yielding FinSequence,
               IY being Function-yielding FinSequence such that
        len FY = dY and
        len IY = dY - 1 and
        for n being Nat
          st 1 <= n & n < dY
          holds IY.n is incidence-matrix of rng (FY.n),rng (FY.(n+1)) and
        for n being Nat
          st 1 <= n & n <= dY
          holds FY.n is non empty & FY.n is one-to-one and
        A25: p = [FY,IY] and
        A26: Y = rng (FY.(k+1)) by A19,A22;
      thus thesis by A23,A24,A25,A26,ZFMISC_1:33;
    end;
    suppose k = dim(p);
      hence thesis by A15,A20;
    end;
    suppose k > dim(p);
      hence thesis by A16,A21;
    end;
  end;
end;

theorem Th25:
-1 < k & k < dim(p)
  implies k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim(p)
proof
  assume A1: -1 < k;
  assume A2: k < dim(p);
  A3: -1 + 1 = 0;
  A4: 0 < k + 1 by A1,A3,XREAL_1:8;
  reconsider n = k + 1 as Element of NAT by A4,INT_1:16;
  A5: n is Nat;
  0 + 1 = 1;
  hence thesis by A2,A4,A5,INT_1:20;
end;

theorem Th26:
k-polytopes(p) is non empty iff (-1 <= k & k <= dim(p))
proof
  set X = k-polytopes(p);
  thus X is non empty implies -1 <= k & k <= dim(p) by Def3;
  thus -1 <= k & k <= dim(p) implies k-polytopes(p) is non empty
  proof
    assume A1: -1 <= k;
    assume A2: k <= dim(p);
    per cases by A1,A2,XXREAL_0:1;
    suppose k = -1;
      hence thesis by Def3;
    end;
    suppose A3: -1 < k & k < dim(p);
      consider F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence such that
        A4: len I = len F - 1 and
        A5: for n being Nat
              st 1 <= n & n < len F
              holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
        A6: for n being Nat
              st 1 <= n & n <= len F
              holds F.n is non empty & F.n is one-to-one and
        A7: p = [F,I] and
        A8: k-polytopes(p) = rng (F.(k+1)) by A3,Def3;
      set n = k + 1;
      A9: 1 <= n by A3,Th25;
      A10: n <= dim(p) by A3,Th25;
      A11: len F = dim(p) by A4,A5,A6,A7,Def2;
      reconsider n as Element of NAT by A9,INT_1:16;
      reconsider n as Nat;
      F.n is non empty & F.n is one-to-one by A6,A9,A10,A11;
      hence thesis by A8,RELAT_1:64;
    end;
    suppose k = dim(p);
      then k-polytopes(p) = {p} by Def3;
      hence thesis;
    end;
  end;
end;

theorem Th27:
k < dim(p) implies k - 1 < dim(p)
proof
  assume A1: k < dim(p);
  k - 1 < k by XREAL_1:148;
  hence thesis by A1,XXREAL_0:2;
end;

:: As we defined the set of k-polytopes for all integers k, we define
:: the an incidence matrix, eta(p,k), for any integer k.  Naturally,
:: for almost all k, this is the empty matrix (empty function).  The
:: two cases in which we extend the data already given by the
:: polyhedron itself is for k = 0 and k = dim(p).  For the latter, we
:: declare that the empty set (the unique -1-dimensional polytope) is
:: incident to all 0-polytopes. For the latter, we declare that every
:: (dim(p)-1)-polytope is incidence to p, the unique dim(p)-polytope
:: of p.
definition
  let p be polyhedron,
      k be Integer;
  func
    eta(p,k) -> incidence-matrix of (k-1)-polytopes(p),k-polytopes(p)
  means :Def4:
    (k < 0 implies it = {}) &
    (k = 0 implies it = [:{{}},0-polytopes(p):] --> 1.Z_2) &
    (0 < k & k < dim(p) implies
       ex F being FinSequence-yielding FinSequence,
          I being Function-yielding FinSequence
        st len I = len F - 1 &
           (for n being Nat
              st 1 <= n & n < len F
              holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
           (for n being Nat
              st 1 <= n & n <= len F
              holds F.n is non empty & F.n is one-to-one) &
           p = [F,I] &
           it = I.k) &
    (k = dim(p) implies
      it = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) &
    (k > dim(p) implies it = {});
  existence
  proof
    per cases by XXREAL_0:1;
    suppose A1: k < 0;
      A2: (k-1)-polytopes(p) = {}
      proof
        k - 1 < 0 - 1 by A1,XREAL_1:11;
        hence thesis by Th26;
      end;
      A3: [:(k-1)-polytopes(p),k-polytopes(p):] = {} by A2,ZFMISC_1:113;
      set f = {};
      reconsider f as Function;
      reconsider f as
        Function of [:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2}
          by A3,FUNCT_2:55,RELAT_1:60;
      reconsider f as
        Element of Funcs([:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2})
          by FUNCT_2:11;
      take f;
      thus thesis by A1;
    end;
    suppose A4: k > dim(p);
      A5: k-polytopes(p) = {} by A4,Th26;
      A6: [:(k-1)-polytopes(p),k-polytopes(p):] = {} by A5,ZFMISC_1:113;
      set f = {};
      reconsider f as Function;
      reconsider f as
        Function of [:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2}
          by A6,FUNCT_2:55,RELAT_1:60;
      reconsider f as
        Element of Funcs([:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2})
          by FUNCT_2:11;
      take f;
      thus thesis by A4;
    end;
    suppose A7: 0 < k & k < dim(p);
      consider F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence such that
        A8: len I = len F - 1 and
        A9: for n being Nat
              st 1 <= n & n < len F
              holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
        A10: for n being Nat
              st 1 <= n & n <= len F
              holds F.n is non empty & F.n is one-to-one and
        A11: p = [F,I] by Def1;
      A12: 0 + 1 = 1;
      A13: 1 <= k by A7,A12,INT_1:20;
      A14: 1 - 1 = 0;
      A15: -1 < k - 1 & k - 1 < dim(p) by A7,A13,A14,Th27,XREAL_1:11;
      A16: (k-1)-polytopes(p) = rng (F.((k-1)+1))
             by A8,A9,A10,A11,A15,Def3;
      A17: k-polytopes(p) = rng (F.(k+1)) by A7,A8,A9,A10,A11,Def3;
      reconsider k' = k as Nat by A13,Th3;
      len F = dim(p) by A8,A9,A10,A11,Def2;
      then reconsider Ik = I.k' as incidence-matrix of (k-1)-polytopes(p),
                                                           k-polytopes(p)
        by A7,A9,A13,A16,A17;
      take Ik;
      thus thesis by A7,A8,A9,A10,A11;
    end;
    suppose A18: k = 0;
      per cases;
      suppose A19: k = dim(p);
        A20: (k-1)-polytopes(p) = {{}} by A18,Def3;
        set f = [:{{}},{p}:] --> 1.Z_2;
        reconsider f as incidence-matrix of {{}},{p} by Th24;
        reconsider f as incidence-matrix of (k-1)-polytopes(p),
                                                k-polytopes(p) by A19,A20,Def3;
        take f;
        thus thesis by A18,A19,Def3;
      end;
      suppose A21: k <> dim(p);
        set f = [:{{}},0-polytopes(p):] --> 1.Z_2;
        reconsider f as incidence-matrix of {{}},0-polytopes(p) by Th24;
        reconsider f as incidence-matrix of (k-1)-polytopes(p),
                                                k-polytopes(p) by A18,Def3;
        take f;
        thus thesis by A18,A21;
      end;
    end;
    suppose A22: k = dim(p);
      per cases;
      suppose A23: k = 0;
        A24: (k-1)-polytopes(p) = {{}} by A23,Def3;
        set f = [:{{}},{p}:] --> 1.Z_2;
        reconsider f as incidence-matrix of {{}},{p} by Th24;
        reconsider f as incidence-matrix of (k-1)-polytopes(p),
                                                k-polytopes(p) by A22,A24,Def3;
        take f;
        thus thesis by A22,A23,Def3;
      end;
      suppose A25: k <> 0;
        set f = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2;
        reconsider f as incidence-matrix of (dim(p) - 1)-polytopes(p),{p}
          by Th24;
        reconsider f as incidence-matrix of (k-1)-polytopes(p),
                                                k-polytopes(p) by A22,Def3;
        take f;
        thus thesis by A22,A25;
      end;
    end;
  end;
  uniqueness
  proof
    let s,t be incidence-matrix of (k-1)-polytopes(p),k-polytopes(p) such that
      A26: (k < 0 implies s = {}) and
      A27: (k = 0 implies s = [:{{}},0-polytopes(p):] --> 1.Z_2) and
      A28: (0 < k & k < dim(p) implies
            ex F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence
             st len I = len F - 1 &
                (for n being Nat
                   st 1 <= n & n < len F
                   holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
                (for n being Nat
                   st 1 <= n & n <= len F
                   holds F.n is non empty & F.n is one-to-one) &
                p = [F,I] &
                s = I.k) and
      A29: (k = dim(p) implies
            s = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) and
      A30: (k > dim(p) implies s = {}) and
      A31: (k < 0 implies t = {}) and
      A32: (k = 0 implies t = [:{{}},0-polytopes(p):] --> 1.Z_2) and
      A33: (0 < k & k < dim(p) implies
            ex F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence
             st len I = len F - 1 &
                (for n being Nat
                   st 1 <= n & n < len F
                   holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
                (for n being Nat
                   st 1 <= n & n <= len F
                   holds F.n is non empty & F.n is one-to-one) &
                p = [F,I] &
                t = I.k) and
      A34: (k = dim(p) implies
            t = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) and
      A35: (k > dim(p) implies t = {});
    per cases by XXREAL_0:1;
    suppose k < 0;
      hence thesis by A26,A31;
    end;
    suppose k = 0;
      hence thesis by A27,A32;
    end;
    suppose A36: 0 < k & k < dim(p);
      consider ds being Nat,
               Fs being FinSequence-yielding FinSequence,
               Is being Function-yielding FinSequence such that
        len Fs = ds and
        len Is = ds - 1 and
        for n being Nat
              st 1 <= n & n < ds
              holds Is.n is incidence-matrix of rng (Fs.n),rng (Fs.(n+1)) and
        for n being Nat
          st 1 <= n & n <= ds
          holds Fs.n is non empty & Fs.n is one-to-one and
        A37: p = [Fs,Is] and
        A38: s = Is.k by A28,A36;
      consider dt being Nat,
               Ft being FinSequence-yielding FinSequence,
               It being Function-yielding FinSequence such that
        len Ft = dt and
        len It = dt - 1 and
        for n being Nat
          st 1 <= n & n < dt
          holds It.n is incidence-matrix of rng (Ft.n),rng (Ft.(n+1)) and
        for n being Nat
          st 1 <= n & n <= dt
          holds Ft.n is non empty & Ft.n is one-to-one and
        A39: p = [Ft,It] and
        A40: t = It.k by A33,A36;
      thus thesis by A37,A38,A39,A40,ZFMISC_1:33;
    end;
    suppose k = dim(p);
      hence thesis by A29,A34;
    end;
    suppose k > dim(p);
      hence thesis by A30,A35;
    end;
  end;
end;

definition
  let p be polyhedron,
      k be Integer;
  func
    k-polytope-seq(p) -> FinSequence
  means :Def5:
    (k < -1 implies it = <*>{}) &
    (k = -1 implies it = <*{}*>) &
    (-1 < k & k < dim(p) implies
      ex F being FinSequence-yielding FinSequence,
         I being Function-yielding FinSequence
        st len I = len F - 1 &
           (for n being Nat
              st 1 <= n & n < len F
              holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
           (for n being Nat
              st 1 <= n & n <= len F
              holds F.n is non empty & F.n is one-to-one) &
           p = [F,I] &
           it = F.(k+1)) &
    (k = dim(p) implies it = <*p*>) &
    (k > dim(p) implies it = <*>{});
  existence
  proof
    per cases by XXREAL_0:1;
    suppose A1: k < -1;
      take <*>{};
      thus thesis by A1;
    end;
    suppose A2: k = -1;
      take <*{}*>;
      thus thesis by A2;
    end;
    suppose A3: -1 < k & k < dim(p);
      consider F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence such that
        A4: len I = len F - 1 and
        A5: for n being Nat
              st 1 <= n & n < len F
              holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
        A6: for n being Nat
              st 1 <= n & n <= len F
              holds F.n is non empty & F.n is one-to-one and
        A7: p = [F,I] by Def1;
      take F.(k+1);
      thus thesis by A3,A4,A5,A6,A7;
    end;
    suppose A8: k = dim(p);
      take <*p*>;
      thus thesis by A8;
    end;
    suppose A9: k > dim(p);
      take <*>{};
      thus thesis by A9;
    end;
  end;
  uniqueness
  proof
    let s,t be FinSequence such that
      A10: (k < -1 implies s = <*>{}) and
      A11: (k = -1 implies s = <*{}*>) and
      A12: (-1 < k & k < dim(p) implies
            ex F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence
             st len I = len F - 1 &
                (for n being Nat
                   st 1 <= n & n < len F
                   holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
                (for n being Nat
                   st 1 <= n & n <= len F
                   holds F.n is non empty & F.n is one-to-one) &
                p = [F,I] &
                s = F.(k+1)) and
      A13: (k = dim(p) implies s = <*p*>) and
      A14: (k > dim(p) implies s = <*>{}) and
      A15: (k < -1 implies t = <*>{}) and
      A16: (k = -1 implies t = <*{}*>) and
      A17: (-1 < k & k < dim(p) implies
            ex F being FinSequence-yielding FinSequence,
               I being Function-yielding FinSequence
             st len I = len F - 1 &
                (for n being Nat
                   st 1 <= n & n < len F
                   holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
                (for n being Nat
                   st 1 <= n & n <= len F
                   holds F.n is non empty & F.n is one-to-one) &
                p = [F,I] &
                t = F.(k+1)) and
      A18: (k = dim(p) implies t = <*p*>) and
      A19: (k > dim(p) implies t = <*>{});
    per cases by XXREAL_0:1;
    suppose k < -1;
      hence thesis by A10,A15;
    end;
    suppose k = -1;
      hence thesis by A11,A16;
    end;
    suppose A20: -1 < k & k < dim(p);
      consider ds being Nat,
               Fs being FinSequence-yielding FinSequence,
               Is being Function-yielding FinSequence such that
        len Fs = ds and
        len Is = ds - 1 and
        for n being Nat
          st 1 <= n & n < ds
          holds Is.n is incidence-matrix of rng (Fs.n),rng (Fs.(n+1)) and
        for n being Nat
          st 1 <= n & n <= ds
          holds Fs.n is non empty & Fs.n is one-to-one and
        A21: p = [Fs,Is] and
        A22: s = Fs.(k+1) by A12,A20;
      consider dt being Nat,
               Ft being FinSequence-yielding FinSequence,
               It being Function-yielding FinSequence such that
        len Ft = dt and
        len It = dt - 1 and
        for n being Nat
          st 1 <= n & n < dt
          holds It.n is incidence-matrix of rng (Ft.n),rng (Ft.(n+1)) and
        for n being Nat
          st 1 <= n & n <= dt
          holds Ft.n is non empty & Ft.n is one-to-one and
        A23: p = [Ft,It] and
        A24: t = Ft.(k+1) by A17,A20;
      thus thesis by A21,A22,A23,A24,ZFMISC_1:33;
    end;
    suppose k = dim(p);
      hence thesis by A13,A18;
    end;
    suppose k > dim(p);
      hence thesis by A14,A19;
    end;
  end;
end;

definition
  let p be polyhedron,
      k be Integer;
  func
    num-polytopes(p,k) -> Element of NAT
  equals
    card(k-polytopes(p));
  coherence;
end;

:: It will be convenient to use these in the cases of Euler's
:: polyhedron formula that interest us.
definition
  let p be polyhedron;
  func
    num-vertices(p) -> Element of NAT
  equals
    num-polytopes(p,0);
  correctness;
  func
    num-edges(p) -> Element of NAT
  equals
    num-polytopes(p,1);
  correctness;
  func
    num-faces(p) -> Element of NAT
  equals
    num-polytopes(p,2);
  correctness;
end;

theorem Th28:
dom (k-polytope-seq(p)) = Seg (num-polytopes(p,k))
proof
  consider F being FinSequence-yielding FinSequence,
           I being Function-yielding FinSequence such that
    A1: len I = len F - 1 and
    A2: for n being Nat
          st 1 <= n & n < len F
          holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
    A3: for n being Nat
          st 1 <= n & n <= len F
          holds F.n is non empty & F.n is one-to-one and
    A4: p = [F,I] by Def1;
 per cases;
 suppose A5: k < -1;
   A6: k-polytope-seq(p) = <*>{} by A5,Def5;
   k-polytopes(p) = {} by A5,Def3;
   hence thesis by A6,FINSEQ_1:def 3;
 end;
 suppose A7: -1 <= k & k <= dim(p);
   per cases by A7,XXREAL_0:1;
   suppose A8: k = -1;
     A9: k-polytopes(p) = {{}} by A8,Def3;
     A10: k-polytope-seq(p) = <*{}*> by A8,Def5;
     A11: num-polytopes(p,k) = 1 by A9,CARD_2:60;
     len (k-polytope-seq(p)) = 1 by A10,FINSEQ_1:56;
     hence thesis by A11,FINSEQ_1:def 3;
   end;
   suppose A12: -1 < k & k < dim(p);
     A13: len F = dim(p) by A1,A2,A3,A4,Def2;
     A14: k-polytope-seq(p) = F.(k+1) by A1,A2,A3,A4,A12,Def5;
     A15: k-polytopes(p) = rng (F.(k+1)) by A1,A2,A3,A4,A12,Def3;
     set n = k + 1;
     reconsider n as Nat by A12,Th25;
     reconsider Fn = F.n as FinSequence;
     A16: 1 <= n & n <= dim(p) by A12,Th25;
     A17: Fn is one-to-one by A3,A13,A16;
     A18: num-polytopes(p,k) = card (dom Fn) by A15,A17,Th2;
     len Fn = num-polytopes(p,k) by A18,PRE_CIRC:21;
     hence thesis by A14,FINSEQ_1:def 3;
   end;
   suppose A19: k = dim(p);
     A20: k-polytopes(p) = {p} by A19,Def3;
     A21: k-polytope-seq(p) = <*p*> by A19,Def5;
     A22: num-polytopes(p,k) = 1 by A20,CARD_2:60;
     len (k-polytope-seq(p)) = 1 by A21,FINSEQ_1:56;
     hence thesis by A22,FINSEQ_1:def 3;
   end;
 end;
 suppose A23: k > dim(p);
   A24: k-polytope-seq(p) = <*>{} by A23,Def5;
   k-polytopes(p) = {} by A23,Def3;
   hence thesis by A24,FINSEQ_1:def 3;
 end;
end;

theorem Th29:
len (k-polytope-seq(p)) = num-polytopes(p,k)
proof
  dom (k-polytope-seq(p)) = Seg (num-polytopes(p,k)) by Th28;
  hence thesis by FINSEQ_1:def 3;
end;

theorem Th30:
rng (k-polytope-seq(p)) = k-polytopes(p)
proof
  consider F being FinSequence-yielding FinSequence,
           I being Function-yielding FinSequence such that
  A1: len I = len F - 1 and
  A2: for n being Nat
        st 1 <= n & n < len F
        holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
  A3: for n being Nat
        st 1 <= n & n <= len F
        holds F.n is non empty & F.n is one-to-one and
  A4: p = [F,I] by Def1;
  per cases;
  suppose A5: k < -1;
    k-polytopes(p) = {} by A5,Def3;
    hence thesis by A5,Def5,RELAT_1:60;
  end;
  suppose A6: -1 <= k & k <= dim(p);
   per cases by A6,XXREAL_0:1;
   suppose A7: k = -1;
     A8: k-polytopes(p) = {{}} by A7,Def3;
     k-polytope-seq(p) = <*{}*> by A7,Def5;
     hence thesis by A8,FINSEQ_1:55;
   end;
   suppose A9: -1 < k & k < dim(p);
     k-polytopes(p) = rng (F.(k+1)) by A1,A2,A3,A4,A9,Def3;
     hence thesis by A1,A2,A3,A4,A9,Def5;
   end;
   suppose A10: k = dim(p);
     A11: k-polytopes(p) = {p} by A10,Def3;
     k-polytope-seq(p) = <*p*> by A10,Def5;
     hence thesis by A11,FINSEQ_1:55;
   end;
  end;
  suppose A12: k > dim(p); then
    k-polytopes(p) = {} by Def3;
    hence thesis by A12,Def5,RELAT_1:60;
  end;
end;

theorem Th31:
num-polytopes(p,-1) = 1
proof
  reconsider minusone = -1 as Integer;
  minusone-polytopes(p) = {{}} by Def3;
  hence thesis by CARD_1:79;
end;

theorem Th32:
num-polytopes(p,dim(p)) = 1
proof
  dim(p)-polytopes(p) = {p} by Def3;
  hence thesis by CARD_1:79;
end;

:: The k-polytope sets aren't really sets: they're ordered sets
:: (finite sequences).
::
:: Since the k-polytope sets are empty for k < -1 and k > dim(p), we
:: have to put a condition on n and k for the definition to make
:: sense.
definition
  let p be polyhedron,
      k be Integer,
      n be Nat;
  assume A1: 1 <= n & n <= num-polytopes(p,k) & -1 <= k & k <= dim(p);
  func
    n-th-polytope(p,k) -> Element of k-polytopes(p)
  equals :Def10:
    (k-polytope-seq(p)).n;
  coherence
  proof
    A2: n in Seg num-polytopes(p,k) by A1,FINSEQ_1:3;
    A3: n in dom (k-polytope-seq(p)) by A2,Th28;
    (k-polytope-seq(p)).n in rng (k-polytope-seq(p)) by A3,FUNCT_1:12;
    hence thesis by Th30;
  end;
end;

theorem Th33:
-1 <= k & k <= dim(p)
  implies for x being Element of k-polytopes(p)
            ex n being Nat st x = n-th-polytope(p,k)
                              & 1 <= n
                              & n <= num-polytopes(p,k)
proof
  assume A1: -1 <= k & k <= dim(p);
  let x be Element of k-polytopes(p);
  per cases by A1,XXREAL_0:1;
  suppose A2: k = -1;
    A3: k-polytopes(p) = {{}} by A2,Def3;
    A4: x = {} by A3,TARSKI:def 1;
    reconsider n = 1 as Nat;
    A5: k-polytope-seq(p) = <*{}*> by A2,Def5;
    A6: (k-polytope-seq(p)).n = {} by A5,FINSEQ_1:def 8;
    A7: n <= num-polytopes(p,k) by A3,CARD_1:50;
    take n;
    thus thesis by A1,A4,A6,A7,Def10;
  end;
  suppose A8: k = dim(p);
    A9: k-polytopes(p) = {p} by A8,Def3;
    A10: x = p by A9,TARSKI:def 1;
    reconsider n = 1 as Nat;
    A11: num-polytopes(p,k) = 1 by A9,CARD_1:50;
    A12: k-polytope-seq(p) = <*p*> by A8,Def5;
    A13: (k-polytope-seq(p)).n = p by A12,FINSEQ_1:def 8;
    take n;
    thus thesis by A1,A10,A11,A13,Def10;
  end;
  suppose A14: -1 < k & k < dim(p);
    consider F being FinSequence-yielding FinSequence,
             I being Function-yielding FinSequence such that
      A15: len I = len F - 1 and
      A16: for n being Nat
            st 1 <= n & n < len F
            holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
      A17: for n being Nat
            st 1 <= n & n <= len F
            holds F.n is non empty & F.n is one-to-one and
      A18: p = [F,I] and
      A19: k-polytopes(p) = rng (F.(k+1)) by A14,Def3;
    A20: k-polytope-seq(p) = F.(k+1) by A14,A15,A16,A17,A18,Def5;
    A21: num-polytopes(p,k) = len (F.(k+1)) by A20,Th29;
    A22: len F = dim(p) by A15,A16,A17,A18,Def2;
    A23: -1 + 1 < k + 1 by A14,XREAL_1:8;
    A24: k + 1 <= dim(p) by A14,INT_1:20;
    A25: 0 + 1 <= k + 1 by A23,INT_1:20;
    reconsider k' = k + 1 as Element of NAT by A23,INT_1:16;
    A26: F.k' is non empty by A17,A22,A24,A25;
    A27: rng (F.k') is non empty by A26,RELAT_1:64;
    consider m being set such that
      A28: m in dom (F.k') and
      A29: (F.k').m = x by A19,A27,FUNCT_1:def 5;
    reconsider Fk' = F.k' as FinSequence;
    A30: dom Fk' = Seg (len Fk') by FINSEQ_1:def 3;
    now
      consider a being Nat such that
      A31: dom Fk' = Seg a by FINSEQ_1:def 2;
      thus m is Element of NAT by A28,A31;
    end;
    then reconsider m as Element of NAT;
    A32: 1 <= m & m <= len Fk' by A28,A30,FINSEQ_1:3;
    take m;
    thus thesis by A14,A20,A21,A29,A32,Def10;
  end;
end;

theorem Th34:
k-polytope-seq(p) is one-to-one
proof
  set s = k-polytope-seq(p);
  per cases by XXREAL_0:1;
  suppose k < -1;
    hence thesis by Def5;
  end;
  suppose k = -1;
    hence thesis by Def5;
  end;
  suppose A1: -1 < k & k < dim(p);
    consider F being FinSequence-yielding FinSequence,
             I being Function-yielding FinSequence such that
      A2: len I = len F - 1 and
      A3: for n being Nat
            st 1 <= n & n < len F
            holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
      A4: for n being Nat
            st 1 <= n & n <= len F
            holds F.n is non empty & F.n is one-to-one and
      A5: p = [F,I] and
      A6: s = F.(k+1) by A1,Def5;
    A7: len F = dim(p) by A2,A3,A4,A5,Def2;
    A8: -1 + 1 < k + 1 by A1,XREAL_1:8;
    reconsider m = k + 1 as Element of NAT by A8,INT_1:16;
    A9: 0 + 1 <= m by A8,INT_1:20;
    m <= dim(p) by A1,INT_1:20;
    hence thesis by A4,A6,A7,A9;
  end;
  suppose k = dim(p);
    then s = <*p*> by Def5;
    hence thesis;
  end;
  suppose k > dim(p);
    hence thesis by Def5;
  end;
end;

theorem Th35:
-1 <= k & k <= dim(p)
  implies for m,n being Nat
            st 1 <= n & n <= num-polytopes(p,k)
               & 1 <= m & m <= num-polytopes(p,k)
               & n-th-polytope(p,k) = m-th-polytope(p,k)
             holds m = n
proof
  assume A1: -1 <= k & k <= dim(p);
  let m,n be Nat such that
    A2: 1 <= n and
    A3: n <= num-polytopes(p,k) and
    A4: 1 <= m and
    A5: m <= num-polytopes(p,k) and
    A6: n-th-polytope(p,k) = m-th-polytope(p,k);
  set s = k-polytope-seq(p);
  A7: n-th-polytope(p,k) = s.n by A1,A2,A3,Def10;
  A8: m-th-polytope(p,k) = s.m by A1,A4,A5,Def10;
  A9: n in Seg (num-polytopes(p,k)) by A2,A3,FINSEQ_1:3;
  A10: n in dom s by A9,Th28;
  A11: m in Seg (num-polytopes(p,k)) by A4,A5,FINSEQ_1:3;
  A12: m in dom s by A11,Th28;
  s is one-to-one by Th34;
  hence thesis by A6,A7,A8,A10,A12,FUNCT_1:def 8;
end;

definition
  let p be polyhedron,
      k be Integer,
      x be Element of (k-1)-polytopes(p),
      y be Element of k-polytopes(p);
  assume A1: 0 <= k & k <= dim(p);
  func
    incidence-value(x,y) -> Element of Z_2
  equals :Def11:
    eta(p,k).(x,y);
  coherence
  proof
    set n = eta(p,k);
    A2: dom n = [:(k-1)-polytopes(p),k-polytopes(p):] by FUNCT_2:169;
    A3: (k-1)-polytopes(p) <> {}
    proof
      set m = k - 1;
      A4: 0 - 1 = -1;
      A5: -1 <= m by A1,A4,XREAL_1:11;
      m <= dim(p) - 0 by A1,XREAL_1:15;
      hence thesis by A5,Th26;
    end;
    A6: k-polytopes(p) <> {} by A1,Th26;
    A7: [x,y] in dom n by A2,A3,A6,ZFMISC_1:106;
    A8: rng n c= {0.Z_2,1.Z_2} by FUNCT_2:169;
    n.[x,y] in rng n by A7,FUNCT_1:12;
    hence thesis by A8,BSPACE:3,5,6;
  end;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Chain Spaces and their Subspaces.  Boundary of a k-chain.
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

::  The set of subsets of the k-polytopes naturally forms a vector
::  space over the field Z_2.  Addition is disjoint union, and scalar
::  multiplication is defined by the equations 1*x = x, 0*x = 0.
definition
  let p be polyhedron,
      k be Integer;
  func
    k-chain-space(p) -> finite-dimensional VectSp of Z_2
   equals
     bspace(k-polytopes(p));
   coherence;
end;

theorem
for x being Element of k-polytopes(p)
  holds (0.(k-chain-space(p)))@x = 0.Z_2 by BSPACE:14;

theorem Th37:
num-polytopes(p,k) = dim (k-chain-space(p))
proof
  A1: singletons(k-polytopes(p)) is Basis of k-chain-space(p) by BSPACE:41;
  set n = dim (k-chain-space(p));
  n = Card (singletons(k-polytopes(p))) by A1,VECTSP_9:def 2;
  hence thesis by BSPACE:42;
end;

:: A k-chain is a set of k-polytopes.
definition
  let p be polyhedron,
      k be Integer;
  func
    k-chains(p) -> non empty finite set
  equals
    bool (k-polytopes(p));
  coherence;
end;

definition
  let p be polyhedron,
      k be Integer,
      x be Element of (k-1)-polytopes(p),
      v be Element of k-chain-space(p);
  func
    incidence-sequence(x,v) -> FinSequence of Z_2
  means :Def14:
    ((k-1)-polytopes(p) is empty implies it = <*>{}) &
    ((k-1)-polytopes(p) is non empty implies
      len it = num-polytopes(p,k)
      & for n being Nat
          st 1 <= n & n <= num-polytopes(p,k)
          holds
            it.n =
            (v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k)));
  existence
  proof
    per cases;
    suppose A1: (k-1)-polytopes(p) is empty;
      set s = <*>{};
      A2: rng s c= the carrier of Z_2 by XBOOLE_1:2;
      reconsider s as FinSequence of Z_2 by A2,FINSEQ_1:def 4;
      take s;
      thus thesis by A1;
    end;
    suppose A3: (k-1)-polytopes(p) is non empty;
      deffunc F(Nat) =
        (v@($1-th-polytope(p,k)))*incidence-value(x,$1-th-polytope(p,k));
      consider s being FinSequence of Z_2 such that
        A4: len s = num-polytopes(p,k) and
        A5: for n being Nat
              st n in Seg num-polytopes(p,k)
              holds s.n = F(n) from FINSEQ_2:sch 1;
      A6: for n being Nat
            st 1 <= n & n <= num-polytopes(p,k)
            holds s.n =
              (v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k))
      proof
        let n be Nat such that
          A7: 1 <= n and
          A8: n <= num-polytopes(p,k);
        A9: n in Seg num-polytopes(p,k) by A7,A8,FINSEQ_1:3;
        reconsider n as Element of NAT by ORDINAL1:def 13;
        thus thesis by A5,A9;
      end;
      take s;
      thus thesis by A3,A4,A6;
    end;
  end;
  uniqueness
  proof
    let s,t be FinSequence of Z_2 such that
      A10: (k-1)-polytopes(p) is empty implies s = <*>{} and
      A11: (k-1)-polytopes(p) is non empty implies
        len(s) = num-polytopes(p,k) &
        (for n being Nat
           st 1 <= n & n <= num-polytopes(p,k)
           holds s.n =
           (v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k))) and
      A12: (k-1)-polytopes(p) is empty implies t = <*>{} and
      A13: (k-1)-polytopes(p) is non empty implies
        len(t) = num-polytopes(p,k) &
        for n being Nat
          st 1 <= n & n <= num-polytopes(p,k)
          holds t.n =
            (v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k));
    per cases;
    suppose (k-1)-polytopes(p) is empty;
      hence thesis by A10,A12;
    end;
    suppose A14: (k-1)-polytopes(p) is non empty;
      for n being Nat
        st 1 <= n & n <= len s
        holds s.n = t.n
      proof
        let n be Nat such that
          A15: 1 <= n and
          A16: n <= len s;
        reconsider n as Nat;
        s.n = (v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k))
              by A11,A14,A15,A16;
        hence thesis by A11,A13,A14,A15,A16;
      end;
      hence thesis by A11,A13,A14,FINSEQ_1:18;
    end;
  end;
end;

theorem Th38:
for c,d being Element of k-chain-space(p),
    x being Element of k-polytopes(p)
  holds (c+d)@x = (c@x) + (d@x)
proof
  let c,d be Element of k-chain-space(p),
      x be Element of k-polytopes(p);
  c+d = c \+\ d by BSPACE:def 5;
  hence thesis by BSPACE:15;
end;

theorem Th39:
for c,d being Element of k-chain-space(p),
    x being Element of (k-1)-polytopes(p)
  holds incidence-sequence(x,c+d)
        = incidence-sequence(x,c) + incidence-sequence(x,d)
proof
  let c,d be Element of k-chain-space(p),
      x be Element of (k-1)-polytopes(p);
  set n = num-polytopes(p,k);
  set l = incidence-sequence(x,c+d);
  set isc = incidence-sequence(x,c);
  set isd = incidence-sequence(x,d);
  set r = isc + isd;
  per cases;
  suppose A1: (k-1)-polytopes(p) is empty;
    A2: isc = <*>(the carrier of Z_2) by A1,Def14;
    A3: isd = <*>(the carrier of Z_2) by A1,Def14;
    reconsider isc as Element of 0-tuples_on the carrier of Z_2
      by A2,FINSEQ_2:114;
    reconsider isd as Element of 0-tuples_on the carrier of Z_2
      by A3,FINSEQ_2:114;
    A4: isc + isd is Element of 0-tuples_on the carrier of Z_2;
    r = <*>(the carrier of Z_2) by A4,FINSEQ_2:113;
    hence thesis by A1,Def14;
  end;
  suppose A5: (k-1)-polytopes(p) is non empty;
    A6: len(l) = n & len(r) = n
    proof
      A7: len isc = n by A5,Def14;
      A8: len isd = n by A5,Def14;
      reconsider isc as Element of n-tuples_on the carrier of Z_2
        by A7,FINSEQ_2:110;
      reconsider isd as Element of n-tuples_on the carrier of Z_2
        by A8,FINSEQ_2:110;
      reconsider s = isc + isd as Element of n-tuples_on the carrier of Z_2;
      len s = n by FINSEQ_2:109;
      hence thesis by A5,Def14;
    end;
    for n being Nat st 1 <= n & n <= len l
      holds l.n = r.n
    proof
      let m be Nat such that
        A9: 1 <= m and
        A10: m <= len l;
      set a = m-th-polytope(p,k);
      set iva = incidence-value(x,a);
      A11: len l = n by A5,Def14;
      A12: l.m = ((c+d)@a)*iva by A5,A9,A10,A11,Def14;
      A13: isc.m = (c@a)*iva by A5,A9,A10,A11,Def14;
      A14: isd.m = (d@a)*iva by A5,A9,A10,A11,Def14;
      A15: dom r = Seg n by A6,FINSEQ_1:def 3;
      A16: len l = n by A5,Def14;
      m in NAT by ORDINAL1:def 13;
      then
      A17: m in dom r by A9,A10,A15,A16;
      r.m = (c@a)*iva + (d@a)*iva by A13,A14,A17,FVSUM_1:21
         .= (c@a + d@a)*iva by VECTSP_1:def 12
         .= l.m by A12,Th38;
      hence thesis;
    end;
    hence thesis by A6,FINSEQ_1:18;
  end;
end;

theorem Th40:
for c,d being Element of k-chain-space(p),
    x being Element of (k-1)-polytopes(p)
  holds Sum (incidence-sequence(x,c) + incidence-sequence(x,d))
        = (Sum incidence-sequence(x,c)) + (Sum incidence-sequence(x,d))
proof
  let c,d be Element of k-chain-space(p),
      x be Element of (k-1)-polytopes(p);
  set isc = incidence-sequence(x,c);
  set isd = incidence-sequence(x,d);
  per cases;
  suppose A1: (k-1)-polytopes(p) is empty;
    A2: isc = <*>(the carrier of Z_2) by A1,Def14;
    A3: isd = <*>(the carrier of Z_2) by A1,Def14;
    reconsider isc as Element of 0-tuples_on the carrier of Z_2
      by A2,FINSEQ_2:114;
    reconsider isd as Element of 0-tuples_on the carrier of Z_2
      by A3,FINSEQ_2:114;
    A4: Sum isc = 0.Z_2 by FVSUM_1:93;
    A5: Sum isd = 0.Z_2 by FVSUM_1:93;
    reconsider s = isc + isd as Element of 0-tuples_on the carrier of Z_2;
    Sum s = 0.Z_2 by FVSUM_1:93;
    hence thesis by A4,A5,RLVECT_1:def 7;
  end;
  suppose A6: (k-1)-polytopes(p) is non empty;
    reconsider n = num-polytopes(p,k) as Element of NAT;
    A7: len isc = n by A6,Def14;
    A8: len isd = n by A6,Def14;
    reconsider isc' = isc
      as Element of n-tuples_on the carrier of Z_2 by A7,FINSEQ_2:110;
    reconsider isd' = isd
      as Element of n-tuples_on the carrier of Z_2 by A8,FINSEQ_2:110;
    Sum (isc + isd) = Sum (isc' + isd')
                   .= Sum (isc) + Sum (isd) by FVSUM_1:95;
    hence thesis;
  end;
end;

theorem Th41:
for c,d being Element of k-chain-space(p),
    x being Element of (k-1)-polytopes(p)
  holds
  Sum incidence-sequence(x,c+d)
  = (Sum incidence-sequence(x,c)) + (Sum incidence-sequence(x,d))
proof
  let c,d be Element of k-chain-space(p),
      x be Element of (k-1)-polytopes(p);
  Sum incidence-sequence(x,c+d)
  = Sum (incidence-sequence(x,c) + incidence-sequence(x,d)) by Th39
 .= (Sum incidence-sequence(x,c)) + (Sum incidence-sequence(x,d)) by Th40;
  hence thesis;
end;

theorem Th42:
for c being Element of k-chain-space(p),
    a being Element of Z_2,
    x being Element of k-polytopes(p)
  holds (a*c)@x = a*(c@x)
proof
  let c be Element of k-chain-space(p),
      a be Element of Z_2,
      x be Element of k-polytopes(p);
  per cases by BSPACE:8;
  suppose A1: a = 0.Z_2;
    A2: a*(c@x) = 0.Z_2 by A1,VECTSP_1:39;
    a*c = 0.(k-chain-space(p)) by A1,VECTSP_1:59;
    hence thesis by A2,BSPACE:14;
  end;
  suppose A3: a = 1.Z_2;
    A4: a*(c@x) = c@x by A3,VECTSP_1:def 16;
    1.Z_2 = 1_Z_2;
    hence thesis by A3,A4,VECTSP_1:def 26;
  end;
end;

theorem Th43:
for c being Element of k-chain-space(p),
    a being Element of Z_2,
    x being Element of (k-1)-polytopes(p)
  holds incidence-sequence(x,a*c) = a*incidence-sequence(x,c)
proof
  let c be Element of k-chain-space(p),
      a be Element of Z_2,
      x be Element of (k-1)-polytopes(p);
  set l = incidence-sequence(x,a*c);
  set isc = incidence-sequence(x,c);
  set r = a*isc;
  per cases;
  suppose A1: (k-1)-polytopes(p) is empty;
    A2: isc = <*>(the carrier of Z_2) by A1,Def14;
    reconsider isc as Element of 0-tuples_on the carrier of Z_2
      by A2,FINSEQ_2:114;
    A3: a*isc is Element of 0-tuples_on the carrier of Z_2;
    reconsider r as Element of 0-tuples_on the carrier of Z_2 by A3;
    r = <*>(the carrier of Z_2) by FINSEQ_2:113;
    hence thesis by A1,Def14;
  end;
  suppose A4: (k-1)-polytopes(p) is non empty;
    set n = num-polytopes(p,k);
    A5: len l = n & len r = n
    proof
      A6: len isc = n by A4,Def14;
      reconsider isc as Element of n-tuples_on the carrier of Z_2
        by A6,FINSEQ_2:110;
      set r = a*isc;
      reconsider r as Element of n-tuples_on the carrier of Z_2;
      len r = n by FINSEQ_2:109;
      hence thesis by A4,Def14;
    end;
    for m being Nat st 1 <= m & m <= len l
      holds l.m = r.m
    proof
      let m be Nat such that
        A7: 1 <= m and
        A8: m <= len l;
      set s = m-th-polytope(p,k);
      set ivs = incidence-value(x,s);
      A9: len l = n by A4,Def14;
      A10: l.m = ((a*c)@s)*ivs by A4,A7,A8,A9,Def14;
      A11: isc.m = (c@s)*ivs by A4,A7,A8,A9,Def14;
      A12: dom r = Seg n by A5,FINSEQ_1:def 3;
      A13: len l = n by A4,Def14;
      m in NAT by ORDINAL1:def 13;
      then
      A14: m in Seg n by A7,A8,A13;
      r.m = a*((c@s)*ivs) by A11,A12,A14,FVSUM_1:62
         .= (a*(c@s))*ivs by GROUP_1:def 4
         .= l.m by A10,Th42;
      hence thesis;
    end;
    hence thesis by A5,FINSEQ_1:18;
  end;
end;

theorem Th44:
for c,d being Element of k-chain-space(p)
  holds c = d iff for x being Element of k-polytopes(p) holds c@x = d@x
proof
  let c,d be Element of k-chain-space(p);
  thus c = d implies for x being Element of k-polytopes(p) holds c@x = d@x;
  thus (for x being Element of k-polytopes(p) holds c@x = d@x) implies c = d
  proof
    assume A1: for x being Element of k-polytopes(p) holds c@x = d@x;
    thus c c= d
    proof
      let x be set such that A2: x in c;
      reconsider c as Subset of k-polytopes(p);
      reconsider x as Element of k-polytopes(p) by A2;
      c@x = 1.Z_2 by A2,BSPACE:def 3;
      then d@x = 1.Z_2 by A1;
      hence thesis by BSPACE:9;
    end;
    thus d c= c
    proof
      let x be set such that A3: x in d;
      reconsider d as Subset of k-polytopes(p);
      reconsider x as Element of k-polytopes(p) by A3;
      d@x = 1.Z_2 by A3,BSPACE:def 3;
      then c@x = 1.Z_2 by A1;
      hence thesis by BSPACE:9;
    end;
  end;
end;

theorem Th45:
for c,d being Element of k-chain-space(p)
  holds c = d
          iff
        for x being Element of k-polytopes(p) holds x in c iff x in d
proof
  let c,d be Element of k-chain-space(p);
  thus c = d
         implies for x being Element of k-polytopes(p) holds x in c iff x in d;
  thus (for x being Element of k-polytopes(p) holds x in c iff x in d)
         implies c = d
  proof
    assume A1: for x being Element of k-polytopes(p) holds x in c iff x in d;
    assume A2: c <> d;
    consider x being Element of k-polytopes(p) such that
      A3: c@x <> d@x by A2,Th44;
    not (x in c iff x in d) by A3,BSPACE:13;
    hence thesis by A1;
  end;
end;

scheme
  ChainEx { p() -> polyhedron,
            k() -> Integer,
            P[Element of k()-polytopes(p())] } :
  ex c being Subset of k()-polytopes(p())
    st for x being Element of k()-polytopes(p())
         holds x in c iff (P[x] & x in k()-polytopes(p()))
proof
  set c =
    { x where x is Element of k()-polytopes(p()) :
        P[x] & x in k()-polytopes(p()) };
  c c= k()-polytopes(p())
  proof
    let x be set such that A1: x in c;
    consider y being Element of k()-polytopes(p()) such that
      A2: x = y and
      P[y] and
      A3: y in k()-polytopes(p()) by A1;
    thus thesis by A2,A3;
  end;
  then reconsider c as Subset of k()-polytopes(p());
  A4: for x being Element of k()-polytopes(p()) holds
        x in c iff (P[x] & x in k()-polytopes(p()))
  proof
    let x be Element of k()-polytopes(p());
    thus x in c implies (P[x] & x in k()-polytopes(p()))
    proof
      assume x in c;
      then consider y being Element of k()-polytopes(p()) such that
        A5: y = x and
        A6: P[y] and
        A7: y in k()-polytopes(p());
      thus thesis by A5,A6,A7;
    end;
    thus (P[x] & x in k()-polytopes(p())) implies x in c;
  end;
  take c;
  thus thesis by A4;
end;

:: The boundary of a k-chain v is the (k-1)-chain consisting of the
:: (k-1)-polytopes that are on the "perimeter" of v.  Being on the
:: perimeter amounts the sum of the incidence sequence being non-zero,
:: i.e., being equal to 1.
definition
  let p be polyhedron,
      k be Integer,
      v be Element of k-chain-space(p);
  func
    Boundary(v) -> Element of (k-1)-chain-space(p)
  means :Def15:
    ((k-1)-polytopes(p) is empty implies it = 0.((k-1)-chain-space(p))) &
    ((k-1)-polytopes(p) is non empty implies
      for x being Element of (k-1)-polytopes(p)
        holds x in it iff Sum incidence-sequence(x,v) = 1.Z_2);
  existence
  proof
    per cases;
    suppose A1: (k-1)-polytopes(p) is empty;
      take 0.((k-1)-chain-space(p));
      thus thesis by A1;
    end;
    suppose A2: (k-1)-polytopes(p) is non empty;
      defpred Q[Element of (k-1)-polytopes(p)] means
        Sum incidence-sequence($1,v) = 1.Z_2;
      consider c being Subset of (k-1)-polytopes(p) such that
        A3: for x being Element of (k-1)-polytopes(p)
              holds x in c iff (Q[x] & x in (k-1)-polytopes(p)) from ChainEx;
      reconsider c as Element of (k-1)-chain-space(p);
      take c;
      thus thesis by A2,A3;
    end;
  end;
  uniqueness
  proof
    let c,d be Element of (k-1)-chain-space(p) such that
      A4: (k-1)-polytopes(p) is empty implies c = 0.((k-1)-chain-space(p)) and
      A5: (k-1)-polytopes(p) is non empty implies
            for x being Element of (k-1)-polytopes(p)
            holds x in c iff Sum incidence-sequence(x,v) = 1.Z_2 and
      A6: (k-1)-polytopes(p) is empty implies d = 0.((k-1)-chain-space(p)) and
      A7: (k-1)-polytopes(p) is non empty implies
            for x being Element of (k-1)-polytopes(p)
            holds x in d iff Sum incidence-sequence(x,v) = 1.Z_2;
    per cases;
    suppose (k-1)-polytopes(p) is empty;
      hence thesis by A4,A6;
    end;
    suppose A8: (k-1)-polytopes(p) is non empty;
      for x being Element of (k-1)-polytopes(p)
        holds x in c iff x in d
      proof
        let x be Element of (k-1)-polytopes(p);
        thus x in c implies x in d
        proof
          assume x in c;
          then Sum incidence-sequence(x,v) = 1.Z_2 by A5;
          hence thesis by A7,A8;
        end;
        thus x in d implies x in c
        proof
          assume x in d;
          then Sum incidence-sequence(x,v) = 1.Z_2 by A7;
          hence thesis by A5,A8;
        end;
      end;
      hence thesis by Th45;
    end;
  end;
end;

theorem Th46:
for c being Element of k-chain-space(p),
    x being Element of (k-1)-polytopes(p)
  holds (Boundary(c))@x = Sum incidence-sequence(x,c)
proof
  let c be Element of k-chain-space(p),
      x be Element of (k-1)-polytopes(p);
  set b = Boundary(c);
  per cases;
  suppose A1: (k-1)-polytopes(p) is empty;
    A2: Boundary(c) = 0.((k-1)-chain-space(p)) by A1,Def15;
    set iscx = incidence-sequence(x,c);
    A3: iscx = <*>(the carrier of Z_2) by A1,Def14;
    Sum iscx = 0.Z_2 by A3,RLVECT_1:60;
    hence thesis by A2,BSPACE:14;
  end;
  suppose A4: (k-1)-polytopes(p) is non empty;
    A5: x in b iff Sum incidence-sequence(x,c) = 1.Z_2 by A4,Def15;
    per cases;
    suppose x in b;
      hence thesis by A5,BSPACE:def 3;
    end;
    suppose A6: not x in b;
      A7: Sum incidence-sequence(x,c) <> 1.Z_2 by A4,A6,Def15;
      Sum incidence-sequence(x,c) = 0.Z_2 by A7,BSPACE:8;
      hence thesis by A6,BSPACE:def 3;
    end;
  end;
end;

:: Every dimension k has its own boundary operation.
definition
  let p be polyhedron,
      k be Integer;
  func
    k-boundary(p) -> Function of k-chain-space(p),(k-1)-chain-space(p)
  means :Def16:
    for c being Element of k-chain-space(p) holds it.c = Boundary(c);
  existence
  proof
    defpred Q[set,set] means
      ex c being Element of k-chain-space(p) st $1 = c & $2 = Boundary(c);
    A1: for x being set st x in k-chains(p) holds
          ex y being set st y in (k-1)-chains(p) & Q[x,y]
    proof
      let x be set such that
        A2: x in k-chains(p);
      reconsider x as Element of k-chain-space(p) by A2;
      set b = Boundary(x);
      take b;
      thus thesis;
    end;
    consider f being Function of k-chains(p),
                             (k-1)-chains(p) such that
      A3: for x being set st x in k-chains(p) holds Q[x,f.x]
      from FUNCT_2:sch 1(A1);
    reconsider f as Function of k-chain-space(p),(k-1)-chain-space(p);
    A4: for c being Element of k-chain-space(p) holds f.c = Boundary(c)
    proof
      let c be Element of k-chain-space(p);
      Q[c,f.c] by A3;
      hence thesis;
    end;
    take f;
    thus thesis by A4;
  end;
  uniqueness
  proof
    let f,g be Function of k-chain-space(p),(k-1)-chain-space(p) such that
      A5: for c being Element of k-chain-space(p) holds f.c = Boundary(c) and
      A6: for c being Element of k-chain-space(p) holds g.c = Boundary(c);
    A7: dom f = [#](k-chain-space(p)) by FUNCT_2:def 1;
    A8: dom f = dom g by A7,FUNCT_2:def 1;
    for x being set st x in dom f holds f.x = g.x
    proof
      let x be set such that A9: x in dom f;
      reconsider x as Element of k-chain-space(p) by A9;
      f.x = Boundary(x) by A5;
      hence thesis by A6;
    end;
    hence thesis by A8,FUNCT_1:9;
  end;
end;

theorem Th47:
for c,d being Element of k-chain-space(p)
  holds Boundary(c+d) = Boundary(c) + Boundary(d)
proof
  let c,d be Element of k-chain-space(p);
  set bc = Boundary(c);
  set bd = Boundary(d);
  set s = c+d;
  set l = Boundary(s);
  set r = bc+bd;
  for x being Element of (k-1)-polytopes(p) holds l@x = r@x
  proof
    let x be Element of (k-1)-polytopes(p);
    A1: l@x = Sum incidence-sequence(x,s) by Th46;
    set a = bc@x;
    set b = bd@x;
    A2: r@x = a+b by Th38;
    A3: a = Sum incidence-sequence(x,c) by Th46;
    b = Sum incidence-sequence(x,d) by Th46;
    hence thesis by A1,A2,A3,Th41;
  end;
  hence thesis by Th44;
end;

theorem Th48:
for a being Element of Z_2,
    c being Element of k-chain-space(p)
  holds Boundary(a*c) = a*(Boundary(c))
proof
  let a be Element of Z_2,
      c be Element of k-chain-space(p);
  set lsm = a*c;
  set l = Boundary(lsm);
  set rb = Boundary(c);
  set r = a*rb;
  for x being Element of (k-1)-polytopes(p) holds l@x = r@x
  proof
    let x be Element of (k-1)-polytopes(p);
    A1: l@x = Sum incidence-sequence(x,lsm) by Th46;
    A2: rb@x = Sum incidence-sequence(x,c) by Th46;
    set b = rb@x;
    A3: r@x = a*b by Th42;
    incidence-sequence(x,lsm) = a*incidence-sequence(x,c) by Th43;
    hence thesis by A1,A2,A3,FVSUM_1:92;
  end;
  hence thesis by Th44;
end;

:: As defined, the k-boundary operator gives rise to a linear
:: transformation.
theorem Th49:
k-boundary(p) is
  linear-transformation of k-chain-space(p),(k-1)-chain-space(p)
proof
  set V = k-chain-space(p);
  set b = k-boundary(p);
  A1: for x,y being Element of V holds b.(x+y) = (b.x) + (b.y)
  proof
    let x,y be Element of V;
    b.(x+y) = Boundary(x+y) by Def16
           .= Boundary(x) + Boundary(y) by Th47
           .= (b.x) + Boundary(y) by Def16
           .= (b.x) + (b.y) by Def16;
    hence thesis;
  end;
  for a being Element of Z_2,
      x being Element of V
    holds b.(a*x) = a*(b.x)
  proof
    let a be Element of Z_2,
        x be Element of V;
     b.(a*x) = Boundary(a*x) by Def16
            .= a*(Boundary(x)) by Th48
            .= a*(b.x) by Def16;
     hence thesis;
  end;
  hence thesis by A1,MOD_2:def 5;
end;

definition
  let p be polyhedron,
      k be Integer;
  redefine func
    k-boundary(p) -> linear-transformation of k-chain-space(p),
                                          (k-1)-chain-space(p);
  coherence by Th49;
end;

:: The term "circuit" is used in Lakatos.  (A more customary term is
:: "cycle".)
definition
  let p be polyhedron,
      k be Integer;
  func
    k-circuit-space(p) -> Subspace of k-chain-space(p)
  equals
    ker (k-boundary(p));
  coherence;
end;

definition
  let p be polyhedron,
      k be Integer;
  func
    k-circuits(p) -> non empty Subset of k-chains(p)
  equals
    [#](k-circuit-space(p));
  coherence by VECTSP_4:def 2;
end;

definition
  let p be polyhedron,
      k be Integer;
  func
    k-bounding-chain-space(p) -> Subspace of k-chain-space(p)
  equals
    im ((k+1)-boundary(p));
  coherence;
end;

definition
  let p be polyhedron,
      k be Integer;
  func
    k-bounding-chains(p) -> non empty Subset of k-chains(p)
  equals
    [#](k-bounding-chain-space(p));
  coherence by VECTSP_4:def 2;
end;

definition
  let p be polyhedron,
      k be Integer;
  func
    k-bounding-circuit-space(p) -> Subspace of k-chain-space(p)
  equals
    (k-bounding-chain-space(p)) /\ (k-circuit-space(p));
  coherence;
end;

definition
  let p be polyhedron,
      k be Integer;
  func
    k-bounding-circuits(p) -> non empty Subset of k-chains(p)
  equals
    [#](k-bounding-circuit-space(p));
  coherence by VECTSP_4:def 2;
end;

theorem
dim (k-chain-space(p))
  = rank (k-boundary(p)) + nullity (k-boundary(p)) by RANKNULL:44;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Simply Connected and Eulerian Polyhedra
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

:: The property of being simply connected is that circuits are
:: bounding, and vice versa (any bounding chain is a circuit).
definition
  let p be polyhedron;
  attr
    p is simply-connected
  means :Def23:
    for k being Integer holds k-circuits(p) = k-bounding-chains(p);
end;

theorem Th51:
p is simply-connected
  iff for n being Integer
        holds n-circuit-space(p)
              = n-bounding-chain-space(p)
proof
  defpred Q[polyhedron] means
    for n being Integer
      holds n-circuit-space($1)
            = n-bounding-chain-space($1);

  thus p is simply-connected implies Q[p]
  proof
    assume A1: p is simply-connected;
    let n be Integer;
    n-circuits(p) = n-bounding-chains(p) by A1,Def23;
    hence thesis by VECTSP_4:37;
  end;
  thus Q[p] implies p is simply-connected
  proof
    assume A2: Q[p];
    let n be Integer;
    thus thesis by A2;
  end;
end;

definition
  let p be polyhedron;
  func
    alternating-f-vector(p) -> FinSequence of INT
  means :Def24:
    len(it) = dim(p) + 2
    & (for k being Nat st 1 <= k & k <= dim(p) + 2
         holds it.k = ((-1)|^k)*num-polytopes(p,k-2));
  existence
  proof
    deffunc F(Nat) = ((-1)|^$1)*num-polytopes(p,$1-2);
    consider s being FinSequence of INT such that
      A1: len s = dim(p) + 2 and
      A2: for j being Nat
            st j in Seg (dim(p) + 2)
            holds s.j = F(j) from FINSEQ_2:sch 1;
    A3: for j being Nat
          st 1 <= j & j <= dim(p) + 2
          holds s.j = ((-1)|^j)*num-polytopes(p,j-2)
    proof
      let j be Nat such that
        A4: 1 <= j and
        A5: j <= dim(p) + 2;
      A6: j in Seg (dim(p) + 2) by A4,A5,FINSEQ_1:3;
      reconsider j as Element of NAT by ORDINAL1:def 13;
      thus thesis by A2,A6;
    end;
    take s;
    thus thesis by A1,A3;
  end;
  uniqueness
  proof
    let s,t be FinSequence of INT such that
      A7: len(s) = dim(p) + 2 and
      A8: for k being Nat
            st 1 <= k & k <= dim(p) + 2
            holds s.k = ((-1)|^k)*num-polytopes(p,k-2) and
      A9: len(t) = dim(p) + 2 and
      A10: for k being Nat
            st 1 <= k & k <= dim(p) + 2
            holds t.k = ((-1)|^k)*num-polytopes(p,k-2);
    for k being Nat st 1 <= k & k <= len s
      holds s.k = t.k
    proof
      let k be Nat such that
        A11: 1 <= k and
        A12: k <= len s;
      reconsider k as Nat;
      s.k = ((-1)|^k)*num-polytopes(p,k-2) by A7,A8,A11,A12;
      hence thesis by A7,A10,A11,A12;
    end;
    hence thesis by A7,A9,FINSEQ_1:18;
  end;
end;

definition
  let p be polyhedron;
  func
    alternating-proper-f-vector(p) -> FinSequence of INT
  means :Def25:
    len(it) = dim(p)
    & (for k being Nat st 1 <= k & k <= dim(p)
         holds it.k = ((-1)|^(k+1))*num-polytopes(p,k-1));
  existence
  proof
    deffunc F(Nat) =
      ((-1)|^($1+1))*num-polytopes(p,$1-1);
    consider s being FinSequence of INT such that
      A1: len s = dim(p) and
      A2: for j being Nat
            st j in Seg dim(p)
            holds s.j = F(j) from FINSEQ_2:sch 1;
    A3: for j being Nat
          st 1 <= j & j <= dim(p)
          holds s.j = ((-1)|^(j+1))*num-polytopes(p,j-1)
    proof
      let j be Nat such that
        A4: 1 <= j and
        A5: j <= dim(p);
      A6: j in Seg dim(p) by A4,A5,FINSEQ_1:3;
      reconsider j as Element of NAT by ORDINAL1:def 13;
      thus thesis by A2,A6;
    end;
    take s;
    thus thesis by A1,A3;
  end;
  uniqueness
  proof
    let s,t be FinSequence of INT such that
      A7: len(s) = dim(p) and
      A8: for k being Nat
            st 1 <= k & k <= dim(p)
            holds s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) and
      A9: len(t) = dim(p) and
      A10: for k being Nat
            st 1 <= k & k <= dim(p)
            holds t.k = ((-1)|^(k+1))*num-polytopes(p,k-1);
    for k being Nat
      st 1 <= k & k <= len s
      holds s.k = t.k
    proof
      let k be Nat such that
        A11: 1 <= k and
        A12: k <= len s;
      reconsider k as Nat;
      s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) by A7,A8,A11,A12;
      hence thesis by A7,A10,A11,A12;
    end;
    hence thesis by A7,A9,FINSEQ_1:18;
  end;
end;

definition
  let p be polyhedron;
  func
    alternating-semi-proper-f-vector(p) -> FinSequence of INT
  means :Def26:
    len(it) = dim(p) + 1
    & (for k being Nat st 1 <= k & k <= dim(p) + 1
         holds it.k = ((-1)|^(k+1))*num-polytopes(p,k-1));
  existence
  proof
    deffunc F(Nat) =
      ((-1)|^($1+1))*num-polytopes(p,$1-1);
    consider s being FinSequence of INT such that
      A1: len s = dim(p) + 1 and
      A2: for j being Nat
            st j in Seg (dim(p) + 1)
            holds s.j = F(j) from FINSEQ_2:sch 1;
    A3: for j being Nat
          st 1 <= j & j <= dim(p) + 1
          holds s.j = ((-1)|^(j+1))*num-polytopes(p,j-1)
    proof
      let j be Nat such that
        A4: 1 <= j and
        A5: j <= dim(p) + 1;
      A6: j in Seg (dim(p) + 1) by A4,A5,FINSEQ_1:3;
      reconsider j as Element of NAT by ORDINAL1:def 13;
      thus thesis by A2,A6;
    end;
    take s;
    thus thesis by A1,A3;
  end;
  uniqueness
  proof
    let s,t be FinSequence of INT such that
      A7: len(s) = dim(p) + 1 and
      A8: for k being Nat
            st 1 <= k & k <= dim(p) + 1
            holds s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) and
      A9: len(t) = dim(p) + 1 and
      A10: for k being Nat
            st 1 <= k & k <= dim(p) + 1
            holds t.k = ((-1)|^(k+1))*num-polytopes(p,k-1);
    for k being Nat
      st 1 <= k & k <= len s
      holds s.k = t.k
    proof
      let k be Nat such that
        A11: 1 <= k and
        A12: k <= len s;
      reconsider k as Nat;
      s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) by A7,A8,A11,A12;
      hence thesis by A7,A10,A11,A12;
    end;
    hence thesis by A7,A9,FINSEQ_1:18;
  end;
end;

theorem Th52:
1 <= n & n <= len (alternating-proper-f-vector(p))
  implies (alternating-proper-f-vector(p)).n
          =  ((-1)|^(n+1))*(dim ((n-2)-bounding-chain-space(p)))
             + ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p)))
proof
  set apcs = alternating-proper-f-vector(p);
  assume A1: 1 <= n;
  assume A2: n <= len apcs;
  A3: n <= dim(p) by A2,Def25;
  set a = (-1)|^(n+1);
  apcs.n = a*num-polytopes(p,n-1) by A1,A3,Def25
        .= a*(dim ((n-1)-chain-space(p))) by Th37
        .= a*(rank ((n-1)-boundary p) + nullity ((n-1)-boundary p))
            by RANKNULL:44
        .= (a*dim ((n-2)-bounding-chain-space(p)))
           + (a*dim ((n-1)-circuit-space(p)));
  hence thesis;
end;

:: The term "eulerian" comes from Lakatos.
definition
  let p be polyhedron;
  attr
    p is eulerian
  means :Def27:
    Sum (alternating-proper-f-vector(p)) = 1 + (-1)|^(dim(p)+1);
end;

theorem Th53:
alternating-semi-proper-f-vector(p)
  = alternating-proper-f-vector(p) ^ <*(-1)|^(dim(p))*>
proof
  set d = dim(p);
  set aspcs = alternating-semi-proper-f-vector(p);
  set apcs = alternating-proper-f-vector(p);
  set r = apcs ^ <*(-1)|^(dim(p))*>;
  A1: len aspcs = d + 1 by Def26;
  A2: len r = (len apcs) + (len <*(-1)|^(dim(p))*>) by FINSEQ_1:35
           .= d + (len <*(-1)|^(dim(p))*>) by Def25
           .= d + 1 by FINSEQ_1:57;
  A3: len aspcs = len r by A2,Def26;
  for n being Nat st 1 <= n & n <= len aspcs
    holds aspcs.n = r.n
  proof
    let n be Nat such that
      A4: 1 <= n and
      A5: n <= len aspcs;
    per cases by A1,A5,NAT_1:8;
    suppose A6: n <= d;
      A7: len apcs = d by Def25;
      A8: dom apcs = Seg (len apcs) by FINSEQ_1:def 3;
      n in NAT by ORDINAL1:def 13;
      then
      A9: n in dom apcs by A4,A6,A7,A8;
      r.n = apcs.n by A9,FINSEQ_1:def 7
         .= ((-1)|^(n+1))*num-polytopes(p,n-1) by A4,A6,Def25;
      hence thesis by A1,A4,A5,Def26;
    end;
    suppose A10: n = d + 1;
      A11: aspcs.n = ((-1)|^(n+1))*num-polytopes(p,n-1) by A4,A10,Def26
                 .= ((-1)|^(n+1))*1 by A10,Th32
                 .= (-1)|^(n+1);
      A12: n = (len apcs) + 1 by A10,Def25;
      r.n = (-1)|^d by A12,FINSEQ_1:59
         .= (-1)|^(d+2) by Th14;
      hence thesis by A10,A11;
    end;
  end;
  hence thesis by A3,FINSEQ_1:18;
end;

:: Another characterization of Eulerian polyhedra
definition
  let p be polyhedron;
  redefine attr
    p is eulerian
  means :Def28:
    Sum (alternating-semi-proper-f-vector(p)) = 1;
  compatibility
  proof
    set apcs = alternating-proper-f-vector(p);
    set aspcs = alternating-semi-proper-f-vector(p);
    A1: aspcs = apcs ^ <*(-1)|^(dim(p))*> by Th53;
    A2: Sum aspcs = (Sum apcs) + (-1)|^(dim(p)) by A1,GR_CY_1:20;
    A3: p is eulerian implies Sum aspcs = 1
    proof
      assume A4: p is eulerian;
      Sum aspcs = 1 + (-1)|^(dim(p)+1) + (-1)|^(dim(p)) by A2,A4,Def27
               .= 1 + (-1)*((-1)|^(dim(p))) + (-1)|^(dim(p)) by NEWTON:11
               .= 1;
      hence thesis;
    end;
    Sum aspcs = 1 implies p is eulerian
    proof
      assume A5: Sum aspcs = 1;
      Sum apcs = 1 + (-1)*((-1)|^(dim(p))) by A2,A5
              .= 1 + (-1)|^(dim(p)+1) by NEWTON:11;
      hence thesis by Def27;
    end;
    hence thesis by A3;
  end;
end;

theorem Th54:
alternating-f-vector(p)
  = <*-1*> ^ alternating-semi-proper-f-vector(p)
proof
  set acs = alternating-f-vector(p);
  set aspcs = alternating-semi-proper-f-vector(p);
  set d = dim(p);
  set r = <*-1*> ^ aspcs;
  A1: len r = (len <*-1*>) + (len aspcs) by FINSEQ_1:35
           .= (len <*-1*>) + (d + 1)  by Def26
           .= 1 + (d + 1) by FINSEQ_1:57
           .= d + 2;
  A2: len acs = len r by A1,Def24;
  for n being Nat st 1 <= n & n <= len acs
    holds acs.n = r.n
  proof
    let n be Nat such that
      A3: 1 <= n and
      A4: n <= len acs;
    A5: n <= d + 2 by A4,Def24;
    per cases by A3,XXREAL_0:1;
    suppose A6: n = 1;
      acs.n = ((-1)|^1)*num-polytopes(p,1-2) by A5,A6,Def24
               .= (-1)*num-polytopes(p,-1) by NEWTON:10
               .= (-1)*1 by Th31
               .= -1;
      hence thesis by A6,FINSEQ_1:58;
    end;
    suppose A7: n > 1;
      A8: 1 - 1 < n - 1 by A7,XREAL_1:11;
      reconsider m = n - 1 as Element of NAT by A8,INT_1:16;
      A9: 0 < 0 + m by A8;
      A10: 1 <= m by A9,NAT_1:19;
      A11: n - 1 <= (d + 2) - 1 by A5,XREAL_1:11;
      A12: m <= d + 1 by A11;
      A13: r.n = aspcs.(n-1)
      proof
        len <*-1*> = 1 by FINSEQ_1:56;
        hence thesis by A1,A5,A7,FINSEQ_1:37;
      end;
      aspcs.m = ((-1)|^(m+1))*num-polytopes(p,m-1) by A10,A12,Def26
             .= ((-1)|^n)*(num-polytopes(p,n-2));
      hence thesis by A3,A5,A13,Def24;
    end;
  end;
  hence thesis by A2,FINSEQ_1:18;
end;

:: Yet another characterization of eulerian polyhedra
definition
  let p be polyhedron;
  redefine attr
    p is eulerian
  means :Def29:
    Sum (alternating-f-vector(p)) = 0;
  compatibility
  proof
    set acs = alternating-f-vector(p);
    set aspcs = alternating-semi-proper-f-vector(p);
    A1: acs = <*-1*> ^ aspcs by Th54;
    A2: Sum acs = -1 + (Sum aspcs) by A1,Th21;
    p is eulerian implies Sum acs = 0
    proof
      assume A3: p is eulerian;
      Sum acs = -1 + 1 by A2,A3,Def28
             .= 0;
      hence thesis;
    end;
    hence thesis by A2,Def28;
  end;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Extremal Chain Spaces
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

theorem Th55:
0-polytopes(p) is non empty
proof
  set d = dim(p);
  per cases;
  suppose d = 0;
    then 0-polytopes(p) = {p} by Def3;
    hence thesis;
  end;
  suppose d > 0;
    hence thesis by Th26;
  end;
end;

theorem Th56:
Card [#]((-1)-chain-space(p)) = 2
proof
  A1: (-1)-polytopes(p) = {{}} by Def3;
  A2: Card ((-1)-polytopes(p)) = 1 by A1,CARD_1:50;
  Card [#]((-1)-chain-space(p)) = exp(2,1) by A2,BSPACE:43
                               .= 2 by CARD_2:40;
  hence thesis;
end;

theorem Th57:
[#]((-1)-chain-space(p)) = { {}, {{}} }
proof
  (-1)-polytopes(p) = {{}} by Def3;
  hence thesis by ZFMISC_1:30;
end;

theorem Th58:
for x being Element of k-polytopes(p),
    e being Element of (k-1)-polytopes(p)
  st k = 0 & e = {}
  holds incidence-value(e,x) = 1.Z_2
proof
  let x be Element of k-polytopes(p),
      e be Element of (k-1)-polytopes(p) such that
    A1: k = 0 and
    A2: e = {};
  A3: 0 <= k & k <= dim(p) by A1;
  A4: eta(p,k) = [:{{}},0-polytopes(p):] --> 1.Z_2 by A1,Def4;
  A5: {} in {{}} by TARSKI:def 1;
  A6: 0-polytopes(p) is non empty by A3,Th26;
  A7: [{},x] in [:{{}},0-polytopes(p):] by A1,A5,A6,ZFMISC_1:106;
  incidence-value(e,x) = eta(p,k).(e,x) by A3,Def11
                      .= 1.Z_2 by A2,A4,A7,FUNCOP_1:13;
  hence thesis;
end;

theorem Th59:
for k being Integer,
    x being Element of k-polytopes(p),
    v being Element of k-chain-space(p),
    e being Element of (k-1)-polytopes(p),
    n being Nat
  st k = 0 & v = {x} & e = {} & x = n-th-polytope(p,k)
     & 1 <= n & n <= num-polytopes(p,k)
  holds incidence-sequence(e,v).n = 1.Z_2
proof
  let k be Integer,
      x be Element of k-polytopes(p),
      v be Element of k-chain-space(p),
      e be Element of (k-1)-polytopes(p),
      n be Nat such that
    A1: k = 0 and
    A2: v = {x} and
    A3: e = {} and
    A4: x = n-th-polytope(p,k) and
    A5: 1 <= n and
    A6: n <= num-polytopes(p,k);
  set iseq = incidence-sequence(e,v);
  A7: (k-1)-polytopes(p) is non empty by A1,Def3;
  A8: x in v by A2,TARSKI:def 1;
  iseq.n = (v@x)*incidence-value(e,x) by A4,A5,A6,A7,Def14
        .= (1.Z_2)*incidence-value(e,x) by A8,BSPACE:def 3
        .= (1.Z_2)*(1.Z_2) by A1,A3,Th58
        .= 1.Z_2 by VECTSP_1:def 16;
  hence thesis;
end;

theorem Th60:
for k being Integer,
    x being Element of k-polytopes(p),
    e being Element of (k-1)-polytopes(p),
    v being Element of k-chain-space(p),
    m,n being Nat
  st k = 0 &
     v = {x} &
     x = n-th-polytope(p,k) &
     1 <= m &
     m <= num-polytopes(p,k) &
     1 <= n &
     n <= num-polytopes(p,k) &
     m <> n
  holds incidence-sequence(e,v).m = 0.Z_2
proof
  let k be Integer,
      x be Element of k-polytopes(p),
      e be Element of (k-1)-polytopes(p),
      v be Element of k-chain-space(p),
      m,n be Nat such that
    A1: k = 0 and
    A2: v = {x} and
    A3: x = n-th-polytope(p,k) and
    A4: 1 <= m and
    A5: m <= num-polytopes(p,k) and
    A6: 1 <= n and
    A7: n <= num-polytopes(p,k) and
    A8: m <> n;
  set iseq = incidence-sequence(e,v);
  -1 <= k & k <= dim(p) by A1;
  then A9: m-th-polytope(p,k) <> x by A3,A4,A5,A6,A7,A8,Th35;
  now
    assume v@(m-th-polytope(p,k)) = 1.Z_2;
    then m-th-polytope(p,k) in {x} by A2,BSPACE:9;
    hence contradiction by A9,TARSKI:def 1;
  end;
  then A10: v@(m-th-polytope(p,k)) = 0.Z_2 by BSPACE:11;
  A11: (k-1)-polytopes(p) is non empty by A1,Def3;
  iseq.m = (0.Z_2)*(incidence-value(e,m-th-polytope(p,k)))
              by A4,A5,A10,A11,Def14
        .= 0.Z_2 by VECTSP_1:39;
  hence thesis;
end;

theorem Th61:
for k being Integer,
    x being Element of k-polytopes(p),
    v being Element of k-chain-space(p),
    e being Element of (k-1)-polytopes(p)
  st k = 0 & v = {x} & e = {}
  holds Sum incidence-sequence(e,v) = 1.Z_2
proof
  let k be Integer,
      x be Element of k-polytopes(p),
      v be Element of k-chain-space(p),
      e be Element of (k-1)-polytopes(p) such that
    A1: k = 0 and
    A2: v = {x} and
    A3: e = {};
  set iseq = incidence-sequence(e,v);
  A4: -1 <= k & k <= dim(p) by A1;
  consider n being Nat such that
    A5: x = n-th-polytope(p,k) and
    A6: 1 <= n and
    A7: n <= num-polytopes(p,k) by A4,Th33;
  A8: (k-1)-polytopes(p) is non empty by A1,Def3;
  A9: len iseq = num-polytopes(p,k) by A8,Def14;
  A10: dom iseq = Seg (len iseq) by FINSEQ_1:def 3;
  A11: n in dom iseq by A6,A7,A9,A10,FINSEQ_1:3;
  A12: iseq.n = 1.Z_2 by A1,A2,A3,A5,A6,A7,Th59;
  for m being Nat st m in dom iseq & m <> n holds iseq.m = 0.Z_2
  proof
    let m be Nat such that
      A13: m in dom iseq and
      A14: m <> n;
    A15: m in Seg (len iseq) by A13,FINSEQ_1:def 3;
    1 <= m & m <= len iseq by A15,FINSEQ_1:3;
    hence thesis by A1,A2,A5,A6,A7,A9,A14,Th60;
  end;
  hence thesis by A11,A12,MATRIX_3:14;
end;

theorem Th62:
for x being Element of 0-polytopes(p)
  holds (0-boundary(p)).({x}) = {{}}
proof
  let x be Element of 0-polytopes(p);
  set T = 0-boundary(p);
  reconsider minusone = 0 - 1 as Integer;
  A1: 0-polytopes(p) is non empty by Th55;
  reconsider v = {x} as Subset of 0-polytopes(p) by A1,ZFMISC_1:37;
  reconsider v as Element of 0-chain-space(p);
  A2: T.v = Boundary(v) by Def16;
  reconsider bv = Boundary(v) as Element of minusone-chain-space(p);
  A3: minusone-polytopes(p) is non empty by Def3;
  (0-1)-polytopes(p) = {{}} by Def3;
  then reconsider null = {} as Element of (0-1)-polytopes(p) by TARSKI:def 1;
  A4: null in bv iff Sum incidence-sequence(null,v) = 1.Z_2 by A3,Def15;
  A5: {null} c= bv by A4,Th61,ZFMISC_1:37;
  bv c= {null}
  proof
    let y be set such that A6: y in bv;
    A7: [#](minusone-chain-space(p)) = { {}, {{}} } by Th57;
    per cases by A7,TARSKI:def 2;
    suppose bv = {};
      hence thesis by A6;
    end;
    suppose bv = {{}};
      hence thesis by A6;
    end;
  end;
  hence thesis by A2,A5,XBOOLE_0:def 10;
end;

theorem Th63:
k = -1 implies dim(k-bounding-chain-space(p)) = 1
proof
  assume A1: k = -1;
  set T = 0-boundary(p);
  set V = k-bounding-chain-space(p);
  Card [#]V = 2
  proof
    A2: T.(0.(0-chain-space(p))) = 0.(k-chain-space(p)) by A1,RANKNULL:9
                                .= {};
    A3: 0-polytopes(p) <> {} by Th55;
    consider x being set such that
      A4: x in 0-polytopes(p) by A3,XBOOLE_0:def 1;
    reconsider x as Element of 0-polytopes(p) by A4;
    set v = {x};
    A5: T.v = {{}} by Th62;
    A6: dom T = [#](0-chain-space(p)) by RANKNULL:7;
    reconsider v as Subset of 0-polytopes(p) by A4,ZFMISC_1:37;
    reconsider v as Element of 0-chain-space(p);
    A7: v in dom T by A6;
    A8: {} in rng T by A2,A6,FUNCT_1:12;
    A9: {{}} in rng T by A5,A7,FUNCT_1:12;
    A10: {{},{{}}} c= rng T by A8,A9,ZFMISC_1:38;
    A11: Card {{},{{}}} = 2 by CARD_2:76;
    A12: 2 <=` Card rng T by A10,A11,CARD_1:27;
    A13: Card rng T = Card (T .: [#](0-chain-space(p))) by FUNCT_2:45
                   .= Card [#]V by A1,RANKNULL:def 2;
    A14: [#]V c= [#](k-chain-space(p)) by VECTSP_4:def 2;
    Card [#]V <=` Card [#](k-chain-space(p)) by A14,CARD_1:27; then
    Card [#]V <=` 2 by A1,Th56;
    hence thesis by A12,A13,XBOOLE_0:def 10;
  end;
  hence thesis by RANKNULL:6;
end;

theorem Th64:
Card [#](dim(p)-chain-space(p)) = 2
proof
  A1: dim(p)-polytopes(p) = {p} by Def3;
  A2: Card (dim(p)-polytopes(p)) = 1 by A1,CARD_1:50;
  Card [#]((dim(p))-chain-space(p)) = exp(2,1) by A2,BSPACE:43
                                   .= 2 by CARD_2:40;
  hence thesis;
end;

theorem Th65:
{p} is Element of dim(p)-chain-space(p)
proof
  dim(p)-polytopes(p) = {p} by Def3;
  hence thesis by ZFMISC_1:def 1;
end;

theorem Th66:
{p} in [#](dim(p)-chain-space(p))
proof
  {p} is Element of dim(p)-chain-space(p) by Th65;
  hence thesis;
end;

theorem Th67:
(dim(p) - 1)-polytopes(p) is non empty
proof
  set n = dim(p) - 1;
  A1: -1 <= n
  proof
    0 - 1 = -1;
    hence thesis by XREAL_1:11;
  end;
  n <= dim(p) by XREAL_1:148;
  hence thesis by A1,Th26;
end;

registration
  let p be polyhedron;
  cluster
    (dim(p)-1)-polytopes(p) -> non empty;
  coherence by Th67;
end;

theorem Th68:
[#](dim(p)-chain-space(p))
  = { 0.(dim(p)-chain-space(p)), {p} }
proof
  set V = dim(p)-chain-space(p);
  set X = { 0.V, {p} };
  set C = [#]V;
  A1: Card C = 2 by Th64;
  reconsider C as finite set;
  consider a,b being set such that
    A2: a <> b and
    A3: C = {a,b} by A1,CARD_2:79;
  {p} in C by Th66;
  hence thesis by A2,A3,Th1;
end;

theorem Th69:
for x being Element of dim(p)-chain-space(p)
  holds x = 0.(dim(p)-chain-space(p))
     or x = {p}
proof
  set V = dim(p)-chain-space(p);
  let x be Element of V;
  A1: x in [#]V;
  x in { 0.V, {p} } by A1,Th68;
  hence thesis by TARSKI:def 2;
end;

theorem Th70:
for x,y being Element of dim(p)-chain-space(p)
  st x <> y
  holds x = 0.(dim(p)-chain-space(p))
     or y = 0.(dim(p)-chain-space(p))
proof
  set V = dim(p)-chain-space(p);
  let x,y be Element of V such that
    A1: x <> y;
  assume A2: x <> 0.V;
  assume A3: y <> 0.V;
  x = {p} by A2,Th69;
  hence contradiction by A1,A3,Th69;
end;

theorem
dim(p)-polytope-seq(p) = <*p*> by Def5;

theorem Th72:
1-th-polytope(p,dim(p)) = p
proof
  reconsider egy = 1 as Nat;
  A1: egy <= num-polytopes(p,dim(p)) by Th32;
  set s = dim(p)-polytope-seq(p);
  A2: s = <*p*> by Def5;
  egy-th-polytope(p,dim(p)) = s.egy by A1,Def10
                           .= p by A2,FINSEQ_1:57;
  hence thesis;
end;

theorem Th73:
for c being Element of dim(p)-chain-space(p),
    x being Element of dim(p)-polytopes(p)
  st c = {p}
  holds c@x = 1.Z_2
proof
  let c be Element of dim(p)-chain-space(p),
      x be Element of dim(p)-polytopes(p) such that
    A1: c = {p};
  dim(p)-polytopes(p) = {p} by Def3;
  hence thesis by A1,BSPACE:def 3;
end;

theorem Th74:
for x being Element of (dim(p)-1)-polytopes(p),
    c being Element of dim(p)-polytopes(p)
  st c = p
  holds incidence-value(x,c) = 1.Z_2
proof
  let x be Element of (dim(p)-1)-polytopes(p),
      c be Element of dim(p)-polytopes(p) such that
    A1: c = p;
  set f = [:(dim(p)-1)-polytopes(p),{p}:] --> 1.Z_2;
  A2: eta(p,dim(p)) = f by Def4;
  A3: dom f = [:(dim(p)-1)-polytopes(p),{p}:] by FUNCOP_1:19;
  A4: c in {p} by A1,TARSKI:def 1;
  A5: [x,c] in dom f by A3,A4,ZFMISC_1:106;
  A6: f.(x,c) in rng f by A5,FUNCT_1:12;
  A7: f.(x,c) in {1.Z_2} by A6,FUNCOP_1:14;
  f.(x,c) = 1.Z_2 by A7,TARSKI:def 1;
  hence thesis by A2,Def11;
end;

theorem Th75:
for x being Element of (dim(p)-1)-polytopes(p),
    c being Element of dim(p)-chain-space(p)
  st c = {p}
  holds incidence-sequence(x,c) = <*1.Z_2*>
proof
  let x be Element of (dim(p)-1)-polytopes(p),
      c be Element of dim(p)-chain-space(p) such that
    A1: c = {p};
  set iseq = incidence-sequence(x,c);
  A2: num-polytopes(p,dim(p))= 1 by Th32;
  A3: len iseq = 1 by A2,Def14;
  iseq.1 = 1.Z_2
  proof
    reconsider egy = 1 as Nat;
    A4: egy <= num-polytopes(p,dim(p)) by Th32;
    set z = egy-th-polytope(p,dim(p));
    A5: z = p by Th72;
    A6: iseq.egy = (c@z)*(incidence-value(x,z)) by A4,Def14;
    A7: c@z = 1.Z_2 by A1,Th73;
    incidence-value(x,z) = 1.Z_2 by A5,Th74;
    hence thesis by A6,A7,VECTSP_1:def 16;
  end;
  hence thesis by A3,FINSEQ_1:57;
end;

theorem Th76:
for x being Element of (dim(p)-1)-polytopes(p),
    c being Element of dim(p)-chain-space(p)
  st c = {p}
  holds Sum incidence-sequence(x,c) = 1.Z_2
proof
  let x be Element of (dim(p)-1)-polytopes(p),
      c be Element of dim(p)-chain-space(p) such that
    A1: c = {p};
  incidence-sequence(x,c) = <*1.Z_2*> by A1,Th75;
  hence thesis by FINSOP_1:12;
end;

:: The boundary operation applied to the unique non-zero vector of the
:: dim(p)-chain space gives the "top" vector of the (dim(p)-1)-chain
:: space.  In other words, every (dim(p)-1)-polytope is incidence to
:: the whole polyhedron.
theorem Th77:
(dim(p)-boundary(p)).{p} = (dim(p)-1)-polytopes(p)
proof
  set T = dim(p)-boundary(p);
  set X = (dim(p)-1)-polytopes(p);
  reconsider c = {p} as Element of dim(p)-chain-space(p) by Th65;
  reconsider d = X as Element of (dim(p)-1)-chain-space(p) by ZFMISC_1:def 1;
  reconsider Tc = T.c as Element of (dim(p)-1)-chain-space(p);
  for x being Element of X
     holds x in Tc iff x in d
  proof
    let x be Element of X;
    thus x in Tc implies x in d;
    thus x in d implies x in Tc
    proof
      assume x in d;
      A1: Sum incidence-sequence(x,c) = 1.Z_2 by Th76;
      x in Boundary(c) by A1,Def15;
      hence thesis by Def16;
    end;
  end;
  hence thesis by SUBSET_1:8;
end;

theorem Th78:
dim(p)-boundary(p) is one-to-one
proof
  set T = dim(p)-boundary(p);
  set U = (dim(p) - 1)-chain-space(p);
  set V = dim(p)-chain-space(p);
  set A = (dim(p) - 1)-polytopes(p);
  set B = {p};
  assume A1: not T is one-to-one;
  consider x1,x2 being set such that
    A2: x1 in dom T and
    A3: x2 in dom T and
    A4: T.x1 = T.x2 and
    A5: x1 <> x2 by A1,FUNCT_1:def 8;
  reconsider x1 as Element of V by A2;
  reconsider x2 as Element of V by A3;
  per cases by A5,Th70;
  suppose A6: x1 = 0.V;
    A7: x2 = B by A5,A6,Th69;
    T.x1 = 0.U by A6,RANKNULL:9;
    hence thesis by A4,A7,Th77;
  end;
  suppose A8: x2 = 0.V;
    A9: x1 = B by A5,A8,Th69;
    T.x2 = 0.U by A8,RANKNULL:9;
    hence thesis by A4,A9,Th77;
  end;
end;

theorem Th79:
dim ((dim(p)-1)-bounding-chain-space(p)) = 1
proof
  set d = dim(p);
  set T = d-boundary(p);
  set U = d-chain-space(p);
  set V = (d-1)-bounding-chain-space(p);
  A1: T is one-to-one by Th78;
  A2: Card [#]V = Card (T .: [#]U) by RANKNULL:def 2
               .= Card (rng T) by FUNCT_2:45;
  A3: Card (dom T) = Card [#]U by RANKNULL:7
                  .= 2 by Th64;
  Card [#]V = 2 by A1,A2,A3,Th2;
  hence thesis by RANKNULL:6;
end;

theorem Th80:
p is simply-connected implies dim ((dim(p)-1)-circuit-space(p)) = 1
proof
  assume A1: p is simply-connected;
  set d = dim(p);
  set U = (d-1)-bounding-chain-space(p);
  set V = (d-1)-circuit-space(p);
  U = V by A1,Th51;
  hence thesis by Th79;
end;

theorem Th81:
1 < n & n < dim(p) + 2
  implies (alternating-f-vector(p)).n
          = (alternating-proper-f-vector(p)).(n-1)
proof
  assume A1: 1 < n;
  assume A2: n < dim(p) + 2;
  set acs = alternating-f-vector(p);
  set apcs = alternating-proper-f-vector(p);
  A3: acs.n = ((-1)|^n)*num-polytopes(p,n-2) by A1,A2,Def24;
  A4: 0 <= n - 1
  proof
    1 - 1 = 0;
    hence thesis by A1,XREAL_1:15;
  end;
  reconsider m = n - 1 as Element of NAT by A4,INT_1:16;
  reconsider m as Nat;
  A5: 1 <= m
  proof
    A6: 2 <= n
    proof
      1 + 1 = 2;
      hence thesis by A1,INT_1:20;
    end;
    2 - 1 = 1;
    hence thesis by A6,XREAL_1:15;
  end;
  A7: m <= dim(p)
  proof
    A8: n < (dim(p) + 1) + 1 by A2;
    A9: n <= dim(p) + 1 by A8,NAT_1:13;
    n - 1 <= (dim(p) + 1) - 1 by A9,XREAL_1:11;
    hence thesis;
  end;
  apcs.m = ((-1)|^(m+1))*num-polytopes(p,m-1) by A5,A7,Def25;
  hence thesis by A3;
end;

theorem Th82:
alternating-f-vector(p)
  = <*-1*> ^ alternating-proper-f-vector(p) ^ <*(-1)|^(dim(p))*>
proof
  set acs = alternating-f-vector(p);
  set apcs = alternating-proper-f-vector(p);
  set r = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*>;
  set n = dim(p);
  A1: len acs = n + 2 by Def24;
  A2: len apcs = n by Def25;
  A3: len r = (len <*-1*>) + (len apcs) + (len <*(-1)|^(dim(p))*>) by Th16;
  A4: len <*-1*> = 1 by FINSEQ_1:56;
  A5: len <*(-1)|^(dim(p))*> = 1 by FINSEQ_1:56;
  for k being Nat
    st 1 <= k & k <= len acs
    holds acs.k = r.k
  proof
    let k be Nat such that
      A6: 1 <= k and
      A7: k <= len acs;
    per cases by A1,A6,A7,XXREAL_0:1;
    suppose A8: k = 1;
      A9: 1 <= n + 2 by Th12;
      reconsider o = 1 as Nat;
      A10: o - 2 = -1;
      A11: acs.o = ((-1)|^o)*num-polytopes(p,-1) by A9,A10,Def24;
      A12: (-1)|^1 = -1 by Th4,Th9;
      num-polytopes(p,-1) = 1 by Th31;
      hence thesis by A8,A11,A12,Th17;
    end;
    suppose A13: k = n + 2;
      A14: 1 <= k by A13,Th12;
      A15: acs.k = ((-1)|^k)*num-polytopes(p,k-2) by A13,A14,Def24;
      A16: r.k = (-1)|^k
      proof
        A17: k = (len <*-1*> + len (apcs) + 1)
        proof
          len <*-1*> = 1 by FINSEQ_1:56;
          hence thesis by A2,A13;
        end;
        r.k = (-1)|^(dim(p)) by A17,Th18
           .= (-1)|^k by A13,Th14;
        hence thesis;
      end;
      num-polytopes(p,k-2) = 1 by A13,Th32;
      hence thesis by A15,A16;
    end;
    suppose A18: 1 < k & k < n + 2;
      set m = k - 1;
      A19: len <*-1*> = 1 by FINSEQ_1:56;
      A20: k <= len (<*-1*> ^ apcs)
      proof
        A21: len (<*-1*> ^ apcs) = (len <*-1*> + len apcs) by FINSEQ_1:35
                               .= n + 1 by A2,FINSEQ_1:56;
        A22: k + 1 <= n + 2 by A18,INT_1:20;
        A23: (k + 1) - 1 = k;
        (n + 2) - 1 = n + 1;
        hence thesis by A21,A22,A23,XREAL_1:11;
      end;
      r.k = apcs.m by A18,A19,A20,Th19;
      hence thesis by A18,Th81;
    end;
  end;
  hence thesis by A1,A2,A3,A4,A5,FINSEQ_1:18;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: A Generalized Euler Relation and its 1-, 2-, and 3-dimensional
:: Special Cases
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

theorem Th83:
dim(p) is odd
  implies Sum (alternating-f-vector(p))
        = Sum (alternating-proper-f-vector(p)) - 2
proof
  assume A1: dim(p) is odd;
  set acs = alternating-f-vector(p);
  set apcs = alternating-proper-f-vector(p);
  A2: acs = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*> by Th82;
  A3: (-1)|^(dim(p)) = -1 by A1,Th9;
  reconsider minusone = -1 as Integer;
  reconsider lastterm = (-1)|^(dim(p)) as Integer;
  Sum acs = (Sum <*minusone*>) + (Sum apcs) + (Sum <*lastterm*>) by A2,Th22
         .= (Sum <*minusone*>) + (Sum apcs) + (-1) by A3,RVSUM_1:103
         .= (-1) + (Sum apcs) + (-1) by RVSUM_1:103
         .= (Sum apcs) - 2;
  hence thesis;
end;

theorem Th84:
dim(p) is even
  implies Sum (alternating-f-vector(p))
        = Sum (alternating-proper-f-vector(p))
proof
  assume A1: dim(p) is even;
  set acs = alternating-f-vector(p);
  set apcs = alternating-proper-f-vector(p);
  A2: acs = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*> by Th82;
  A3: (-1)|^(dim(p)) = 1 by A1,Th8;
  reconsider minusone = -1 as Integer;
  reconsider plusone = 1 as Integer;
  reconsider lastterm = (-1)|^(dim(p)) as Integer;
  Sum acs = (Sum <*minusone*>) + (Sum apcs) + (Sum <*lastterm*>) by A2,Th22
         .= (Sum <*minusone*>) + (Sum apcs) + 1 by A3,RVSUM_1:103
         .= (-1) + (Sum apcs) + 1 by RVSUM_1:103
         .= Sum apcs;
  hence thesis;
end;

theorem Th85:
dim(p) = 1 implies
  Sum alternating-proper-f-vector(p)
  = num-polytopes(p,0)
proof
  assume A1: dim(p) = 1;
  set apcs = alternating-proper-f-vector(p);
  A2: len apcs = 1 by A1,Def25;
  reconsider egy = 1 as Nat;
  A3: apcs.egy = (-1)|^(egy+1)*num-polytopes(p,egy-1) by A1,Def25;
  A4: (-1)|^(egy+1) = 1 by Th5,Th8;
  apcs = <*num-polytopes(p,0)*> by A2,A3,A4,FINSEQ_1:57;
  hence thesis by RVSUM_1:103;
end;

theorem Th86:
dim(p) = 2 implies
  Sum alternating-proper-f-vector(p)
  = num-polytopes(p,0) - num-polytopes(p,1)
proof
  assume A1: dim(p) = 2;
  set apcs = alternating-proper-f-vector(p);
  A2: len apcs = 2 by A1,Def25;
  reconsider o = 1 as Nat;
  reconsider t = 2 as Nat;
  reconsider mo = -1 as Integer;
  A3: apcs.o = ((-1)|^(o+1))*num-polytopes(p,o-1) by A1,Def25;
  A4: apcs.t = ((-1)|^(t+1))*num-polytopes(p,t-1) by A1,Def25;
  A5: (-1)|^(o+1) = 1 by Th5,Th8;
  A6: (-1)|^(t+1) = -1 by Th6,Th9;
  reconsider apcso = apcs.o as Integer;
  reconsider apcst = apcs.t as Integer;
  A7: apcs = <*apcso,apcst*> by A2,FINSEQ_1:61;
  reconsider apcsonetwo = <*apcso,apcst*> as FinSequence of INT;
  Sum apcs = apcso + apcst by A7,RVSUM_1:107
          .= num-polytopes(p,0) - num-polytopes(p,1) by A3,A4,A5,A6;
  hence thesis;
end;

theorem Th87:
dim(p) = 3 implies
  Sum alternating-proper-f-vector(p)
  = num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2)
proof
  assume A1: dim(p) = 3;
  set apcs = alternating-proper-f-vector(p);
  A2: len apcs = 3 by A1,Def25;
  reconsider o = 1 as Nat;
  reconsider tw = 2 as Nat;
  reconsider th = 3 as Nat;
  reconsider mo = -1 as Integer;
  A3: (-1)|^(o+1) = 1 by Th5,Th8;
  A4: (-1)|^(tw+1) = -1 by Th6,Th9;
  A5: (-1)|^(th+1) = 1 by Th7,Th8;
  A6: apcs.o = o*num-polytopes(p,o-1) by A1,A3,Def25;
  A7: apcs.tw = mo*num-polytopes(p,tw-1) by A1,A4,Def25;
  A8: apcs.th = o*num-polytopes(p,th-1) by A1,A5,Def25;
  reconsider apcson = apcs.o as Integer;
  reconsider apcstw = apcs.tw as Integer;
  reconsider apcsth = apcs.th as Integer;
  A9: apcs = <*apcson,apcstw,apcsth*> by A2,FINSEQ_1:62;
  reconsider apcsonetwothree = <*apcson,apcstw,apcsth*> as FinSequence of INT;
  Sum apcs = apcson + apcstw + apcsth by A9,RVSUM_1:108
          .= num-polytopes(p,0)
             - num-polytopes(p,1)
             + num-polytopes(p,2) by A6,A7,A8;
  hence thesis;
end;

:: A trivial special case
theorem Th88:
dim(p) = 0 implies p is eulerian
proof
  set d = dim(p);
  assume A1: d = 0;
  set apcs = alternating-proper-f-vector(p);
  A2: (-1)|^(d+1) = -1 by A1,NEWTON:10;
  A3: 1 + (-1)|^(d+1) = 0 by A2;
  A4: len apcs = 0 by A1,Def25;
  apcs = <*>INT by A4,FINSEQ_1:32;
  hence thesis by A3,Def27,GR_CY_1:22;
end;

theorem Th89:
p is simply-connected implies p is eulerian
proof
  assume A1: p is simply-connected;
  set apcs = alternating-proper-f-vector(p);
  per cases;
  suppose dim(p) = 0;
    hence thesis by Th88;
  end;
  suppose A2: dim(p) > 0;
    A3: len apcs > 0 by A2,Def25;
    :: Split the alternating characteristic sequence into a sum of two
    :: sequences, a and b
    deffunc A(Nat)
      = ((-1)|^($1+1))*(dim (($1-2)-bounding-chain-space(p)));
    deffunc B(Nat)
      = ((-1)|^($1+1))*(dim (($1-1)-circuit-space(p)));
    consider a being FinSequence such that
      A4: len a = len apcs and
      A5: for n being Nat st n in Seg len apcs
            holds a.n = A(n) from FINSEQ_1:sch 2;
    consider b being FinSequence such that
      A6: len b = len apcs and
      A7: for n being Nat st n in Seg (len apcs)
            holds b.n = B(n) from FINSEQ_1:sch 2;
    A8: rng a c= INT & rng b c= INT
    proof
      thus rng a c= INT
      proof
        let y be set such that
        A9: y in rng a;
        consider x being set such that
        A10: x in dom a and
        A11: y = a.x by A9,FUNCT_1:def 5;
        A12: x in Seg (len apcs) by A4,A10,FINSEQ_1:def 3;
        reconsider x as Element of NAT by A12;
        a.x = ((-1)|^(x+1))*(dim ((x-2)-bounding-chain-space(p))) by A5,A12;
        hence thesis by A11;
      end;
      thus rng b c= INT
      proof
        let y be set such that
        A13: y in rng b;
        consider x being set such that
        A14: x in dom b and
        A15: y = b.x by A13,FUNCT_1:def 5;
        A16: x in Seg (len apcs) by A6,A14,FINSEQ_1:def 3;
        reconsider x as Element of NAT by A16;
        b.x = ((-1)|^(x+1))*(dim ((x-1)-circuit-space(p))) by A7,A16;
        hence thesis by A15;
      end;
    end;
    reconsider a,b as FinSequence of INT by A8,FINSEQ_1:def 4;
    A17: for n being Nat
    st 1 <= n & n <= len apcs
    holds apcs.n = a.n + b.n
    proof
      let n be Nat such that
        A18: 1 <= n and
        A19: n <= len apcs;
      A20: apcs.n = ((-1)|^(n+1))*(dim ((n-2)-bounding-chain-space(p)))
      + ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p))) by A18,A19,Th52;
      reconsider n' = n as Element of NAT by ORDINAL1:def 13;
      A21: n' in Seg (len apcs) by A18,A19;
      a.n' = ((-1)|^(n'+1))*(dim ((n'-2)-bounding-chain-space(p)))
        by A5,A21;
      hence thesis by A7,A20,A21;
    end;

    :: Now we want to how that the alternating characterstic sequence is
    :: a telescoping sum of the sequences a and b.  First, we establish
    :: the necessary relation among the sequences a and b.
    A22: for n being Nat
    st 1 <= n & n < len apcs
    holds b.n = -(a.(n+1))
    proof
      let n be Nat such that
      A23: 1 <= n and
      A24: n < len apcs;
      A25: n in Seg (len apcs) by A23,A24,FINSEQ_1:3;
      reconsider n as Element of NAT by ORDINAL1:def 13;
      A26: b.n = ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p))) by A7,A25;
      A27: n + 1 <= len apcs by A24,INT_1:20;
      A28: 1 <= n + 1 by NAT_1:11;
      A29: n + 1 in Seg (len apcs) by A27,A28;
      a.(n+1) = A(n+1) by A5,A29
             .= (((-1)|^(n+1))*((-1)|^1))*(dim ((n-1)-bounding-chain-space(p)))
               by NEWTON:13
             .= ((-1)|^(n+1))*(-1)*(dim ((n-1)-bounding-chain-space(p)))
               by NEWTON:10
             .= -((-1)|^(n+1))*(dim ((n-1)-bounding-chain-space(p)))
             .= -(b.n) by A1,A26,Th51;
      hence thesis;
    end;
    A30: Sum apcs = (a.1) + (b.(len apcs)) by A3,A4,A6,A17,A22,Th15;
    A31: a.1 = 1
    proof
      reconsider egy = 1 as Element of NAT;
      A32: 1 <= 0 + 1;
      A33: egy <= len apcs by A3,A32,NAT_1:13;
      A34: egy in Seg (len apcs) by A33;
      a.egy = ((-1)|^(1+1))*(dim ((egy-2)-bounding-chain-space(p))) by A5,A34
           .= 1*(dim ((egy-2)-bounding-chain-space(p))) by Th5,Th8
           .= 1 by Th63;
      hence thesis;
    end;
    b.(len apcs) = (-1)|^(dim(p)+1)
    proof
      reconsider n = len apcs as Element of NAT;
      A35: n = dim(p) by Def25;
      A36: 0 + 1 = 1;
      A37: 1 <= len apcs by A3,A36,NAT_1:13;
      A38: n in Seg (len apcs) by A37;
      b.n = B(n) by A7,A38
         .= ((-1)|^(n+1))*1 by A1,A35,Th80
         .= (-1)|^(n+1);
      hence thesis by Def25;
    end;
    hence thesis by A30,A31,Def27;
  end;
end;

:: Euler's Polyhedron Formula in One Dimension: simply-connected
:: 1-dimensional polyhedra are just line segments.
theorem
p is simply-connected & dim(p) = 1
  implies num-vertices(p) = 2
proof
  assume A1: p is simply-connected;
  assume A2: dim(p) = 1;
  set acs = alternating-f-vector(p);
  set apcs = alternating-proper-f-vector(p);
  A3: p is eulerian by A1,Th89;
  0 = Sum acs by A3,Def29
   .= Sum apcs - 2 by A2,Th4,Th83
   .= num-polytopes(p,0) - 2 by A2,Th85;
  hence thesis;
end;

:: Euler's Polyhedron Formula in Two Dimensions: polygons have exactly
:: as many vertices as edges.
theorem
p is simply-connected & dim(p) = 2
  implies num-vertices(p) = num-edges(p)
proof
  assume A1: p is simply-connected;
  assume A2: dim(p) = 2;
  A3: p is eulerian by A1,Th89;
  set s = num-polytopes(p,0) - num-polytopes(p,1);
  A4: s = Sum(alternating-proper-f-vector(p)) by A2,Th86;
  set c = alternating-f-vector(p);
  0 = Sum c by A3,Def29
   .= s by A2,A4,Th5,Th84;
  hence thesis;
end;

:: Euler's Polyhedron Formula in Three Dimensions: V - E + F = 2.
theorem
p is simply-connected & dim(p) = 3
  implies num-vertices(p) - num-edges(p) + num-faces(p) = 2
proof
  assume A1: p is simply-connected;
  assume A2: dim(p) = 3;
  A3: p is eulerian by A1,Th89;
  set s = num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2);
  A4: s = Sum(alternating-proper-f-vector(p)) by A2,Th87;
  set c = alternating-f-vector(p);
  0 = Sum c by A3,Def29
   .= s - 2 by A2,A4,Th6,Th83;
  hence thesis;
end;