:: 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, ARYTM;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_1, NUMBERS, FUNCOP_1,
      FINSET_1, XCMPLX_0, XXREAL_0, NAT_1, INT_1, CARD_2, FINSEQ_1, SEQ_1,
      FINSEQ_2, POWER, RVSUM_1, NEWTON, ABIAN, STRUCT_0, RLVECT_1, GROUP_1,
      VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_7, FVSUM_1, GR_CY_1, MATRLIN,
      VECTSP_9, RANKNULL, BSPACE;
 constructors NAT_1, VECTSP_9, BINOP_1, REALSET1, FINSOP_1, XXREAL_0, FVSUM_1,
      WELLORD2, BSPACE, REAL_1, BINOP_2, RANKNULL, VECTSP_7, VECTSP_5, NEWTON,
      GR_CY_1, ABIAN, POWER, CARD_2;
 registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1,
      SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0, FINSEQ_1, FINSEQ_2, CARD_1,
      MATRLIN, BSPACE, ORDINAL1, NEWTON, RVSUM_1, FUNCOP_1, POLYNOM1, ABIAN,
      XREAL_0, NUMBERS, JORDAN23, GOBRD13, XCMPLX_0, XXREAL_0, VALUED_0;
 requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
 definitions XBOOLE_0, BINOP_1, STRUCT_0, TARSKI, FVSUM_1, FINSEQ_1, BSPACE,
      RANKNULL, ALGSTR_0;
 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, NUMBERS, CARD_2, PRE_CIRC, FINSEQ_3, SUBSET_1, MOD_2, MATRIX_3,
      CALCUL_1, PARTFUN1, VALUED_0;
 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 1 <= k;
  then reconsider k as Element of NAT by 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 qua Nat) qua Nat)+ 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:46;
  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 a = b;
      then reconsider a as Element of NAT;
      reconsider s = a |^ n as Element of NAT by ORDINAL1:def 13;
      s in NAT;
      hence thesis by NUMBERS:17;
    end;
    suppose
A2:   a = -b;
A3:   -b = (-1)*b;
      reconsider bn = b |^ n as Element of NAT by ORDINAL1:def 13;
      (-1) |^n is Integer by Th10;
      then reconsider l = (-1) |^ n as Element of INT by INT_1:def 2;
      a |^ n = l*bn by A2,A3,NEWTON:12;
      hence thesis;
    end;
  end;
end;

Lm1: for x being Element of NAT st 0 < x holds 0 qua Nat+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 qua Nat + 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];
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;
      then
A15:  Sum p = 0 by CARD_2:59,GR_CY_1:22;
A16:  t = <*x*>
      proof
        p = {} by A14;
        hence thesis by FINSEQ_1:47;
      end;
      then
A17:  len t = 1 by FINSEQ_1:56;
      reconsider egy = 1 as Nat;
      egy <= len t by A16,FINSEQ_1:56;
      then t.egy = a.egy + b.egy by A11;
      hence thesis by A13,A15,A16,A17,FINSEQ_1:57;
    end;
    suppose
A18:  len p > 0;
      set m = len p;
      set a' = a|m;
      set b' = b|m;
A19:  m <= len a & m <= len b by A9,A10,CALCUL_1:6;
      then
A20:  len a' = len p by FINSEQ_1:80;
A21:  len b' = len p by A19,FINSEQ_1:80;
A22:  for n being Nat st 1 <= n & n <= len p holds p.n = a'.n + b'.n
      proof
        let n be Nat such that
A23:    1 <= n and
A24:    n <= len p;
        len p <= len t by CALCUL_1:6;
        then
A25:    n <= len t by A24,XXREAL_0:2;
        dom p = Seg len p by FINSEQ_1:def 3;
        then
A26:    n in dom p by A23,A24,FINSEQ_1:3;
        reconsider n as Element of NAT by ORDINAL1:def 13;
        p.n = t.n by A26,FINSEQ_1:def 7
          .= a.n + b.n by A11,A23,A25
          .= a'.n + b.n by A24,FINSEQ_3:121
          .= a'.n + b'.n by A24,FINSEQ_3:121;
        hence thesis;
      end;
      for n being Nat st 1 <= n & n < len p holds b'.n = -(a'.(n+1))
      proof
        let n be Nat such that
A27:    1 <= n and
A28:    n < len p;
        reconsider n as Element of NAT by ORDINAL1:def 13;
A29:    b'.n = b.n by A28,FINSEQ_3:121;
A30:    n + 1 <= len p by A28,INT_1:20;
        len p <= len t by CALCUL_1:6;
        then
A31:    n < len t by A28,XXREAL_0:2;
        a'.(n+1) = a.(n+1) by A30,FINSEQ_3:121;
        hence thesis by A12,A27,A29,A31;
      end;
      then
A32:  Sum p = a'.1 + b'.(len p) by A8,A18,A20,A21,A22;
A33:  a'.1 = a.1
      proof
        reconsider egy = 1 as Element of NAT;
        0 qua Nat + 1 = 1;
        then egy <= len p by A18,INT_1:20;
        hence thesis by FINSEQ_3:121;
      end;
      x = -(b'.(len p)) + b.(len t)
      proof
A34:    len t = (len p) + 1
        proof
          len <*x*> = 1 by FINSEQ_1:56;
          hence thesis by FINSEQ_1:35;
        end;
A35:    1 <= len t
        proof
          0 qua Nat + 1 = 1;
          hence thesis by A34,XREAL_1:8;
        end;
A36:    a.(len t) = -(b'.(len p))
        proof
A37:      len p < len t
          proof
            0 qua Nat + len p = len p;
            hence thesis by A34,XREAL_1:8;
          end;
          1 <= len p by A18,Lm1;
          then
A38:      b.(len p) = -(a.(len p + 1)) by A12,A37;
          b.(len p) = b'.(len p) by FINSEQ_3:121;
          hence thesis by A34,A38;
        end;
        x = t.(len p + 1) by FINSEQ_1:59
          .= -(b'.(len p)) + b.(len t) by A11,A34,A35,A36;
        hence thesis;
      end;
      hence thesis by A13,A32,A33;
    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);
  len (p ^ q) <= len (p ^ (q ^ r)) by Th11;
  then k <= len (p ^ (q ^ r)) by A2,XXREAL_0:2;
  then
A3: (p ^ (q ^ r)).k = (q ^ r).(k - (len p)) by A1,FINSEQ_1:37;
  set n = k - (len p);
  (len p) - (len p) = 0;
  then
A4: 0 < n by A1,XREAL_1:11;
  0 qua Nat + 1 = 1;
  then
A5: 1 <= n by A4,INT_1:20;
  then reconsider n as Nat by Th3;
A6: k <= (len p) + (len q) by A2,FINSEQ_1:35;
  n <= len q
  proof
    ((len p) + (len q)) - (len p) = len q;
    hence thesis by A6,XREAL_1:11;
  end;
  then n in Seg (len q) by A5,FINSEQ_1:3;
  then
A7: n in dom q by FINSEQ_1:def 3;
  reconsider n as Element of NAT by ORDINAL1:def 13;
  (q ^ r).n = q.n by A7,FINSEQ_1:def 7;
  hence thesis by A3,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;
    a in INT by INT_1:def 2;
    then {a} c= INT by 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;
  rng q c= REAL by NUMBERS:15,XBOOLE_1:1;
  then reconsider p,q as real-yielding FinSequence by A1,VALUED_0:def 3;
  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;
  {1.Z_2} c= {0.Z_2,1.Z_2} by ZFMISC_1:12;
  then rng f c= {0.Z_2,1.Z_2} by A2,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
  struct PolyhedronStr(# PolytopsF ->FinSequence-yielding FinSequence,
    IncidenceF ->Function-yielding FinSequence #);
end;

:: The following properties, `polyhedron_1', `polyhedron_2', and
:: `polyhedron_3' are admittedly a bit contrived.  However, they ensure
:: that a PolyhedronStr is a polyhedron: that there is one more polytope set
:: than incidence matrix, that the incidience matrices are incidence matrices
:: of the right sets, and that each term of the polytope sequence is an
:: enumeration of the respective polytope set.

definition
  let p be PolyhedronStr;
  attr p is polyhedron_1 means
  :Def1:
  len the IncidenceF of p = len(the PolytopsF of p) - 1;
  attr p is polyhedron_2 means
  :Def2:
  for n being Nat
  st 1 <= n & n < len the PolytopsF of p holds (the IncidenceF of p).n
  is incidence-matrix of rng ((the PolytopsF of p).n),
  rng ((the PolytopsF of p).(n+1));
  attr p is polyhedron_3 means
  :Def3:
  for n being Nat
  st 1 <= n & n <= len the PolytopsF of p
  holds (the PolytopsF of p).n is non empty &
  (the PolytopsF of p).n is one-to-one;
end;

registration
  cluster polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr;
  existence
  proof
    reconsider F = <*<*{}*>*> as FinSequence-yielding FinSequence;
    reconsider I = <*>{} as Function-yielding FinSequence;
    take p = PolyhedronStr(#F,I#);
A1: len F = 1 by FINSEQ_1:56;
    len I = 1-1;
    hence p is polyhedron_1 by A1,Def1;
    for n being Nat st 1 <= n & n < 1
    holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1));
    hence p is polyhedron_2 by A1,Def2;
    let n be Nat such that
A2: 1 <= n and
A3: n <= len the PolytopsF of p;
    n = 1 by A1,A2,A3,XXREAL_0:1;
    hence thesis by FINSEQ_1:def 8;
  end;
end;

definition
  mode polyhedron is polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr;
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 equals

  len the PolytopsF of p;
  coherence;
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
  :Def5:
  (k < -1 implies it = {}) &
  (k = -1 implies it = {{}}) & (-1 < k & k < dim(p) implies
  it = rng ((the PolytopsF of p).(k+1))) & (k = dim(p) implies it = {p}) &
  (k > dim(p) implies it = {});
  existence
  proof
    set F = the PolytopsF of p;
    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);
      -1 + 1 = 0;
      then 0 <= k by A3,INT_1:20;
      then reconsider k as Element of NAT by INT_1:16;
      set n = k + 1;
      reconsider Fn = F.n as FinSequence;
      take rng Fn;
      thus thesis by A3;
    end;
    suppose
A4:   k = dim(p);
      take {p};
      thus thesis by A4;
    end;
    suppose
A5:   k > dim(p);
      take {};
      thus thesis by A5;
    end;
  end;
  uniqueness
  proof
    set F = the PolytopsF of p;
    let X,Y be finite set such that
A6: k < -1 implies X = {} and
A7: k = -1 implies X = {{}} and
A8: (-1 < k & k < dim(p)) implies X = rng (F.(k+1)) and
A9: k = dim(p) implies X = {p} and
A10: k > dim(p) implies X = {} and
A11: k < -1 implies Y = {} and
A12: k = -1 implies Y = {{}} and
A13: (-1 < k & k < dim(p)) implies Y = rng (F.(k+1)) and
A14: k = dim(p) implies Y = {p} and
A15: k > dim(p) implies Y = {};
    per cases by XXREAL_0:1;
    suppose k < -1;
      hence thesis by A6,A11;
    end;
    suppose k = -1;
      hence thesis by A7,A12;
    end;
    suppose -1 < k & k < dim(p);
      hence thesis by A8,A13;
    end;
    suppose k = dim(p);
      hence thesis by A9,A14;
    end;
    suppose k > dim(p);
      hence thesis by A10,A15;
    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);
  -1 + 1 = 0;
  then
A3: 0 < k + 1 by A1,XREAL_1:8;
  then reconsider n = k + 1 as Element of NAT by INT_1:16;
A4: n is Nat;
  0 qua Nat + 1 = 1;
  hence thesis by A2,A3,A4,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 Def5;
  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 Def5;
    end;
    suppose
A3:   -1 < k & k < dim(p);
      set F = the PolytopsF of p;
A4:   k-polytopes(p) = rng (F.(k+1)) by A3,Def5;
      set n = k + 1;
A5:   1 <= n by A3,Th25;
A6:   n <= dim(p) by A3,Th25;
      reconsider n as Element of NAT by A5,INT_1:16;
      reconsider n as Nat;
      F.n is non empty & F.n is one-to-one by A5,A6,Def3;
      hence thesis by A4;
    end;
    suppose k = dim(p);
      then k-polytopes(p) = {p} by Def5;
      hence thesis;
    end;
  end;
end;

theorem Th27:
  k < dim(p) implies k - 1 < dim(p) by XREAL_1:148,XXREAL_0:2;

:: 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
  :Def6:
  (k < 0 implies it = {}) &
  (k = 0 implies it = [:{{}},0-polytopes(p):] --> 1.Z_2) &
  (0 < k & k < dim(p) implies it = (the IncidenceF of p).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;
      (k-1)-polytopes(p) = {}
      proof
        k - 1 < 0 qua Nat - 1 by A1,XREAL_1:11;
        hence thesis by Th26;
      end;
      then
A2:   [:(k-1)-polytopes(p),k-polytopes(p):] = {} by 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 A2,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
A3:   k > dim(p);
      then k-polytopes(p) = {} by Th26;
      then
A4:   [:(k-1)-polytopes(p),k-polytopes(p):] = {} by 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 A4,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 A3;
    end;
    suppose
A5:   0 < k & k < dim(p);
      set F = the PolytopsF of p, I = the IncidenceF of p;
      0 qua Nat + 1 = 1;
      then
A6:   1 <= k by A5,INT_1:20;
      1 - 1 = 0;
      then -1 < k - 1 & k - 1 < dim(p) by A5,A6,Th27,XREAL_1:11;
      then
A7:   (k-1)-polytopes(p) = rng (F.((k-1)+1)) by Def5;
A8:   k-polytopes(p) = rng (F.(k+1)) by A5,Def5;
      reconsider k' = k as Nat by A6,Th3;
      reconsider Ik = I.k' as incidence-matrix of (k-1)-polytopes(p),
      k-polytopes(p) by A5,A6,A7,A8,Def2;
      take Ik;
      thus thesis by A5;
    end;
    suppose
A9:   k = 0;
      per cases;
      suppose
A10:    k = dim(p);
A11:    (k-1)-polytopes(p) = {{}} by A9,Def5;
        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 A10,A11,Def5;
        take f;
        thus thesis by A9,A10,Def5;
      end;
      suppose
A12:    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 A9,Def5;
        take f;
        thus thesis by A9,A12;
      end;
    end;
    suppose
A13:  k = dim(p);
      per cases;
      suppose
A14:    k = 0;
        then
A15:    (k-1)-polytopes(p) = {{}} by Def5;
        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 A13,A15,Def5;
        take f;
        thus thesis by A13,A14,Def5;
      end;
      suppose
A16:    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 A13,Def5;
        take f;
        thus thesis by A13,A16;
      end;
    end;
  end;
  uniqueness
  proof
    set I = the IncidenceF of p;
    let s,t be incidence-matrix of (k-1)-polytopes(p),k-polytopes(p) such that
A17: (k < 0 implies s = {}) and
A18: (k = 0 implies s = [:{{}},0-polytopes(p):] --> 1.Z_2) and
A19: (0 < k & k < dim(p) implies s = I.k) and
A20: (k = dim(p) implies s = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) and
A21: (k > dim(p) implies s = {}) and
A22: (k < 0 implies t = {}) and
A23: (k = 0 implies t = [:{{}},0-polytopes(p):] --> 1.Z_2) and
A24: (0 < k & k < dim(p) implies t = I.k) and
A25: (k = dim(p) implies t = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) and
A26: (k > dim(p) implies t = {});
    per cases by XXREAL_0:1;
    suppose k < 0;
      hence thesis by A17,A22;
    end;
    suppose k = 0;
      hence thesis by A18,A23;
    end;
    suppose 0 < k & k < dim(p);
      hence thesis by A19,A24;
    end;
    suppose k = dim(p);
      hence thesis by A20,A25;
    end;
    suppose k > dim(p);
      hence thesis by A21,A26;
    end;
  end;
end;

definition
  let p be polyhedron, k be Integer;
  func k-polytope-seq(p) -> FinSequence means
  :Def7:
  (k < -1 implies it = <*>{}) & (k = -1 implies it = <*{}*>) &
  (-1 < k & k < dim(p) implies it = (the PolytopsF of p).(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);
      set F = the PolytopsF of p;
      take F.(k+1);
      thus thesis by A3;
    end;
    suppose
A4:   k = dim(p);
      take <*p*>;
      thus thesis by A4;
    end;
    suppose
A5:   k > dim(p);
      take <*>{};
      thus thesis by A5;
    end;
  end;
  uniqueness
  proof
    set F = the PolytopsF of p;
    let s,t be FinSequence such that
A6: (k < -1 implies s = <*>{}) and
A7: (k = -1 implies s = <*{}*>) and
A8: (-1 < k & k < dim(p) implies s = F.(k+1)) and
A9: (k = dim(p) implies s = <*p*>) and
A10: (k > dim(p) implies s = <*>{}) and
A11: (k < -1 implies t = <*>{}) and
A12: (k = -1 implies t = <*{}*>) and
A13: (-1 < k & k < dim(p) implies t = F.(k+1)) and
A14: (k = dim(p) implies t = <*p*>) and
A15: (k > dim(p) implies t = <*>{});
    per cases by XXREAL_0:1;
    suppose k < -1;
      hence thesis by A6,A11;
    end;
    suppose k = -1;
      hence thesis by A7,A12;
    end;
    suppose -1 < k & k < dim(p);
      hence thesis by A8,A13;
    end;
    suppose k = dim(p);
      hence thesis by A9,A14;
    end;
    suppose k > dim(p);
      hence thesis by A10,A15;
    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
  set F = the PolytopsF of p;
  per cases;
  suppose
A1: k < -1;
    then
A2: k-polytope-seq(p) = <*>{} by Def7;
    k-polytopes(p) = {} by A1,Def5;
    hence thesis by A2,FINSEQ_1:def 3;
  end;
  suppose
A3: -1 <= k & k <= dim(p);
    per cases by A3,XXREAL_0:1;
    suppose
A4:   k = -1;
      then
A5:   k-polytopes(p) = {{}} by Def5;
A6:   k-polytope-seq(p) = <*{}*> by A4,Def7;
A7:   num-polytopes(p,k) = 1 by A5,CARD_2:60;
      len (k-polytope-seq(p)) = 1 by A6,FINSEQ_1:56;
      hence thesis by A7,FINSEQ_1:def 3;
    end;
    suppose
A8:   -1 < k & k < dim(p);
      then
A9:   k-polytope-seq(p) = F.(k+1) by Def7;
A10:  k-polytopes(p) = rng (F.(k+1)) by A8,Def5;
      set n = k + 1;
      reconsider n as Nat by A8,Th25;
      reconsider Fn = F.n as FinSequence;
      1 <= n & n <= dim(p) by A8,Th25;
      then Fn is one-to-one by Def3;
      then num-polytopes(p,k) = card (dom Fn) by A10,Th2;
      then len Fn = num-polytopes(p,k) by PRE_CIRC:21;
      hence thesis by A9,FINSEQ_1:def 3;
    end;
    suppose
A11:  k = dim(p);
      then
A12:  k-polytopes(p) = {p} by Def5;
A13:  k-polytope-seq(p) = <*p*> by A11,Def7;
A14:  num-polytopes(p,k) = 1 by A12,CARD_2:60;
      len (k-polytope-seq(p)) = 1 by A13,FINSEQ_1:56;
      hence thesis by A14,FINSEQ_1:def 3;
    end;
  end;
  suppose
A15: k > dim(p);
    then
A16: k-polytope-seq(p) = <*>{} by Def7;
    k-polytopes(p) = {} by A15,Def5;
    hence thesis by A16,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
  set F = the PolytopsF of p;
  per cases;
  suppose
A1: k < -1;
    then k-polytopes(p) = {} by Def5;
    hence thesis by A1,Def7,RELAT_1:60;
  end;
  suppose
A2: -1 <= k & k <= dim(p);
    per cases by A2,XXREAL_0:1;
    suppose
A3:   k = -1;
      then
A4:   k-polytopes(p) = {{}} by Def5;
      k-polytope-seq(p) = <*{}*> by A3,Def7;
      hence thesis by A4,FINSEQ_1:55;
    end;
    suppose
A5:   -1 < k & k < dim(p);
      then k-polytopes(p) = rng (F.(k+1)) by Def5;
      hence thesis by A5,Def7;
    end;
    suppose
A6:   k = dim(p);
      then
A7:   k-polytopes(p) = {p} by Def5;
      k-polytope-seq(p) = <*p*> by A6,Def7;
      hence thesis by A7,FINSEQ_1:55;
    end;
  end;
  suppose
A8: k > dim(p);
    then k-polytopes(p) = {} by Def5;
    hence thesis by A8,Def7,RELAT_1:60;
  end;
end;

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

theorem Th32:
  num-polytopes(p,dim(p)) = 1
proof
  dim(p)-polytopes(p) = {p} by Def5;
  hence thesis by CARD_1:50;
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
  :Def12:
  (k-polytope-seq(p)).n;
  coherence
  proof
    n in Seg num-polytopes(p,k) by A1,FINSEQ_1:3;
    then n in dom (k-polytope-seq(p)) by Th28;
    then (k-polytope-seq(p)).n in rng (k-polytope-seq(p)) by 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;
    then
A3: k-polytopes(p) = {{}} by Def5;
    then
A4: x = {} by TARSKI:def 1;
    reconsider n = 1 as Nat;
    k-polytope-seq(p) = <*{}*> by A2,Def7;
    then
A5: (k-polytope-seq(p)).n = {} by FINSEQ_1:def 8;
A6: n <= num-polytopes(p,k) by A3,CARD_1:50;
    take n;
    thus thesis by A1,A4,A5,A6,Def12;
  end;
  suppose
A7: k = dim(p);
    then
A8: k-polytopes(p) = {p} by Def5;
    then
A9: x = p by TARSKI:def 1;
    reconsider n = 1 as Nat;
A10: num-polytopes(p,k) = 1 by A8,CARD_1:50;
    k-polytope-seq(p) = <*p*> by A7,Def7;
    then
A11: (k-polytope-seq(p)).n = p by FINSEQ_1:def 8;
    take n;
    thus thesis by A1,A9,A10,A11,Def12;
  end;
  suppose
A12: -1 < k & k < dim(p);
    set F = the PolytopsF of p;
A13: k-polytopes(p) = rng (F.(k+1)) by A12,Def5;
A14: k-polytope-seq(p) = F.(k+1) by A12,Def7;
    then
A15: num-polytopes(p,k) = len (F.(k+1)) by Th29;
A16: -1 + 1 < k + 1 by A12,XREAL_1:8;
A17: k + 1 <= dim(p) by A12,INT_1:20;
A18: 0 qua Nat + 1 <= k + 1 by A16,INT_1:20;
    reconsider k' = k + 1 as Element of NAT by A16,INT_1:16;
    F.k' is non empty by A17,A18,Def3;
    then rng (F.k') is non empty;
    then consider m being set such that
A19: m in dom (F.k') and
A20: (F.k').m = x by A13,FUNCT_1:def 5;
    reconsider Fk' = F.k' as FinSequence;
A21: dom Fk' = Seg (len Fk') by FINSEQ_1:def 3;
    reconsider m as Element of NAT by A19;
A22: 1 <= m & m <= len Fk' by A19,A21,FINSEQ_1:3;
    take m;
    thus thesis by A12,A14,A15,A20,A22,Def12;
  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 Def7;
  end;
  suppose k = -1;
    hence thesis by Def7;
  end;
  suppose
A1: -1 < k & k < dim(p);
    set F = the PolytopsF of p;
A2: s = F.(k+1) by A1,Def7;
A3: -1 + 1 < k + 1 by A1,XREAL_1:8;
    then reconsider m = k + 1 as Element of NAT by INT_1:16;
A4: 0 qua Nat + 1 <= m by A3,INT_1:20;
    m <= dim(p) by A1,INT_1:20;
    hence thesis by A2,A4,Def3;
  end;
  suppose k = dim(p);
    then s = <*p*> by Def7;
    hence thesis;
  end;
  suppose k > dim(p);
    hence thesis by Def7;
  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,Def12;
A8: m-th-polytope(p,k) = s.m by A1,A4,A5,Def12;
  n in Seg (num-polytopes(p,k)) by A2,A3,FINSEQ_1:3;
  then
A9: n in dom s by Th28;
  m in Seg (num-polytopes(p,k)) by A4,A5,FINSEQ_1:3;
  then
A10: m in dom s by Th28;
  s is one-to-one by Th34;
  hence thesis by A6,A7,A8,A9,A10,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
  :Def13:
  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;
      0 qua Nat - 1 = -1;
      then
A4:   -1 <= m by A1,XREAL_1:11;
      m <= dim(p) - (0 qua Nat) by A1,XREAL_1:15;
      hence thesis by A4,Th26;
    end;
    k-polytopes(p) <> {} by A1,Th26;
    then
A5: [x,y] in dom n by A2,A3,ZFMISC_1:106;
A6: rng n c= {0.Z_2,1.Z_2} by FUNCT_2:169;
    n.[x,y] in rng n by A5,FUNCT_1:12;
    hence thesis by A6,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
  :Def16:
  ((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 = <*>{};
      rng s c= the carrier of Z_2 by XBOOLE_1:2;
      then reconsider s as FinSequence of Z_2 by FINSEQ_1:def 4;
      take s;
      thus thesis by A1;
    end;
    suppose
A2:   (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
A3:   len s = num-polytopes(p,k) and
A4:   for n being Nat st n in dom s
      holds s.n = F(n) from FINSEQ_2:sch 1;
A5: dom s = Seg num-polytopes(p,k) by A3,FINSEQ_1:def 3;
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;
        thus thesis by A4,A9,A5;
      end;
      take s;
      thus thesis by A2,A3,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;
    then
A2: isc = <*>(the carrier of Z_2) by Def16;
A3: isd = <*>(the carrier of Z_2) by A1,Def16;
    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;
    isc + isd is Element of 0-tuples_on the carrier of Z_2;
    then r = <*>(the carrier of Z_2) by FINSEQ_2:113;
    hence thesis by A1,Def16;
  end;
  suppose
A4: (k-1)-polytopes(p) is non empty;
A5: len(l) = n & len(r) = n
    proof
A6:   len isc = n by A4,Def16;
A7:   len isd = n by A4,Def16;
      reconsider isc as Element of n-tuples_on the carrier of Z_2
      by A6,FINSEQ_2:110;
      reconsider isd as Element of n-tuples_on the carrier of Z_2
      by A7,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 A4,Def16;
    end;
    for n being Nat st 1 <= n & n <= len l holds l.n = r.n
    proof
      let m be Nat such that
A8:   1 <= m and
A9:   m <= len l;
      set a = m-th-polytope(p,k);
      set iva = incidence-value(x,a);
A10:  len l = n by A4,Def16;
      then
A11:  l.m = ((c+d)@a)*iva by A4,A8,A9,Def16;
A12:  isc.m = (c@a)*iva by A4,A8,A9,A10,Def16;
A13:  isd.m = (d@a)*iva by A4,A8,A9,A10,Def16;
A14:  dom r = Seg n by A5,FINSEQ_1:def 3;
A15:  len l = n by A4,Def16;
      m in NAT by ORDINAL1:def 13;
      then m in dom r by A8,A9,A14,A15;
      then r.m = (c@a)*iva + (d@a)*iva by A12,A13,FVSUM_1:21
        .= (c@a + d@a)*iva by VECTSP_1:def 12
        .= l.m by A11,Th38;
      hence thesis;
    end;
    hence thesis by A5,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;
    then
A2: isc = <*>(the carrier of Z_2) by Def16;
A3: isd = <*>(the carrier of Z_2) by A1,Def16;
    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,Def16;
A8: len isd = n by A6,Def16;
    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;
    then
A2: a*(c@x) = 0.Z_2 by 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;
    then a*(c@x) = c@x by VECTSP_1:def 16;
    hence thesis by A3,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;
    then isc = <*>(the carrier of Z_2) by Def16;
    then reconsider isc as Element of 0-tuples_on the carrier of Z_2
    by FINSEQ_2:114;
    a*isc is Element of 0-tuples_on the carrier of Z_2;
    then reconsider r as Element of 0-tuples_on the carrier of Z_2;
    r = <*>(the carrier of Z_2) by FINSEQ_2:113;
    hence thesis by A1,Def16;
  end;
  suppose
A2: (k-1)-polytopes(p) is non empty;
    set n = num-polytopes(p,k);
A3: len l = n & len r = n
    proof
      len isc = n by A2,Def16;
      then reconsider isc as Element of n-tuples_on the carrier of Z_2
      by 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 A2,Def16;
    end;
    for m being Nat st 1 <= m & m <= len l holds l.m = r.m
    proof
      let m be Nat such that
A4:   1 <= m and
A5:   m <= len l;
      set s = m-th-polytope(p,k);
      set ivs = incidence-value(x,s);
A6:   len l = n by A2,Def16;
      then
A7:   l.m = ((a*c)@s)*ivs by A2,A4,A5,Def16;
A8:   isc.m = (c@s)*ivs by A2,A4,A5,A6,Def16;
A9:   dom r = Seg n by A3,FINSEQ_1:def 3;
A10:  len l = n by A2,Def16;
      m in NAT by ORDINAL1:def 13;
      then m in Seg n by A4,A5,A10;
      then r.m = a*((c@s)*ivs) by A8,A9,FVSUM_1:62
        .= (a*(c@s))*ivs by GROUP_1:def 4
        .= l.m by A7,Th42;
      hence thesis;
    end;
    hence thesis by A3,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 c <> d;
    then consider x being Element of k-polytopes(p) such that
A2: c@x <> d@x by Th44;
    not (x in c iff x in d) by A2,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
  :Def17:
  ((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
   (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 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
 (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;
    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;
    then
A2: Boundary(c) = 0.((k-1)-chain-space(p));
    set iscx = incidence-sequence(x,c);
    iscx = <*>(the carrier of Z_2) by A1,Def16;
    then Sum iscx = 0.Z_2 by RLVECT_1:60;
    hence thesis by A2,BSPACE:14;
  end;
  suppose
A3: (k-1)-polytopes(p) is non empty;
    then
A4: x in b iff Sum incidence-sequence(x,c) = 1.Z_2 by Def17;
    per cases;
    suppose x in b;
      hence thesis by A4,BSPACE:def 3;
    end;
    suppose
A5:   not x in b;
      then Sum incidence-sequence(x,c) <> 1.Z_2 by A3,Def17;
      then Sum incidence-sequence(x,c) = 0.Z_2 by BSPACE:8;
      hence thesis by A5,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
  :Def18:
  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);
    dom f = [#](k-chain-space(p)) by FUNCT_2:def 1;
    then
A7: dom f = dom g by 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
A8:   x in dom f;
      reconsider x as Element of k-chain-space(p) by A8;
      f.x = Boundary(x) by A5;
      hence thesis by A6;
    end;
    hence thesis by A7,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 Def18
      .= Boundary(x) + Boundary(y) by Th47
      .= (b.x) + Boundary(y) by Def18
      .= (b.x) + (b.y) by Def18;
    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 Def18
      .= a*(Boundary(x)) by Th48
      .= a*(b.x) by Def18;
    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
  :Def25:
  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,Def25;
    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
  :Def26:
  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 dom s
    holds s.j = F(j) from FINSEQ_2:sch 1;
A3: dom s = Seg(dim(p) + 2)  by A1,FINSEQ_1:def 3;
A4: 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
A5:   1 <= j and
A6:   j <= dim(p) + 2;
A7:   j in Seg (dim(p) + 2) by A5,A6,FINSEQ_1:3;
      thus thesis by A2,A7,A3;
    end;
    take s;
    thus thesis by A1,A4;
  end;
  uniqueness
  proof
    let s,t be FinSequence of INT such that
A8: len(s) = dim(p) + 2 and
A9: for k being Nat st 1 <= k & k <= dim(p) + 2
    holds s.k = ((-1)|^k)*num-polytopes(p,k-2) and
A10: len(t) = dim(p) + 2 and
A11: 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
A12:  1 <= k and
A13:  k <= len s;
      reconsider k as Nat;
      s.k = ((-1)|^k)*num-polytopes(p,k-2) by A8,A9,A12,A13;
      hence thesis by A8,A11,A12,A13;
    end;
    hence thesis by A8,A10,FINSEQ_1:18;
  end;
end;

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

definition
  let p be polyhedron;
  func alternating-semi-proper-f-vector(p) -> FinSequence of INT means
  :Def28:
  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 dom s
    holds s.j = F(j) from FINSEQ_2:sch 1;
A3: dom s = Seg(dim(p) + 1)  by A1,FINSEQ_1:def 3;
A4: 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
A5:   1 <= j and
A6:   j <= dim(p) + 1;
A7:   j in Seg (dim(p) + 1) by A5,A6,FINSEQ_1:3;
      thus thesis by A2,A7,A3;
    end;
    take s;
    thus thesis by A1,A4;
  end;
  uniqueness
  proof
    let s,t be FinSequence of INT such that
A8: len(s) = dim(p) + 1 and
A9: for k being Nat st 1 <= k & k <= dim(p) + 1
    holds s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) and
A10: len(t) = dim(p) + 1 and
A11: 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
A12:  1 <= k and
A13:  k <= len s;
      reconsider k as Nat;
      s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) by A8,A9,A12,A13;
      hence thesis by A8,A11,A12,A13;
    end;
    hence thesis by A8,A10,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 n <= len apcs;
  then
A2: n <= dim(p) by Def27;
  set a = (-1)|^(n+1);
  apcs.n = a*num-polytopes(p,n-1) by A1,A2,Def27
    .= 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
  :Def29:
  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 Def28;
  len r = (len apcs) + (len <*(-1)|^(dim(p))*>) by FINSEQ_1:35
    .= d + (len <*(-1)|^(dim(p))*>) by Def27
    .= d + 1 by FINSEQ_1:57;
  then
A2: len aspcs = len r by Def28;
  for n being Nat st 1 <= n & n <= len aspcs holds aspcs.n = r.n
  proof
    let n be Nat such that
A3: 1 <= n and
A4: n <= len aspcs;
    per cases by A1,A4,NAT_1:8;
    suppose
A5:   n <= d;
A6:   len apcs = d by Def27;
A7:   dom apcs = Seg (len apcs) by FINSEQ_1:def 3;
      n in NAT by ORDINAL1:def 13;
      then n in dom apcs by A3,A5,A6,A7;
      then r.n = apcs.n by FINSEQ_1:def 7
        .= ((-1)|^(n+1))*num-polytopes(p,n-1) by A3,A5,Def27;
      hence thesis by A1,A3,A4,Def28;
    end;
    suppose
A8:   n = d + 1;
      then
A9:   aspcs.n = ((-1)|^(n+1))*num-polytopes(p,n-1) by A3,Def28
        .= ((-1)|^(n+1))*1 by A8,Th32
        .= (-1)|^(n+1);
      n = (len apcs) + 1 by A8,Def27;
      then r.n = (-1)|^d by FINSEQ_1:59
        .= (-1)|^(d+2) by Th14;
      hence thesis by A8,A9;
    end;
  end;
  hence thesis by A2,FINSEQ_1:18;
end;

:: Another characterization of Eulerian polyhedra

definition
  let p be polyhedron;
  redefine attr p is eulerian means
  :Def30:
  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);
    aspcs = apcs ^ <*(-1)|^(dim(p))*> by Th53;
    then
A1: Sum aspcs = (Sum apcs) + (-1)|^(dim(p)) by GR_CY_1:20;
A2: p is eulerian implies Sum aspcs = 1
    proof
      assume p is eulerian;
      then Sum aspcs = 1 + (-1)|^(dim(p)+1) + (-1)|^(dim(p)) by A1,Def29
        .= 1 + (-1)*((-1)|^(dim(p))) + (-1)|^(dim(p)) by NEWTON:11
        .= 1;
      hence thesis;
    end;
    Sum aspcs = 1 implies p is eulerian
    proof
      assume Sum aspcs = 1;
      then Sum apcs = 1 + (-1)*((-1)|^(dim(p))) by A1
        .= 1 + (-1)|^(dim(p)+1) by NEWTON:11;
      hence thesis by Def29;
    end;
    hence thesis by A2;
  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 Def28
    .= 1 + (d + 1) by FINSEQ_1:57
    .= d + 2;
  then
A2: len acs = len r by Def26;
  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,Def26;
    per cases by A3,XXREAL_0:1;
    suppose
A6:   n = 1;
      then acs.n = ((-1)|^1)*num-polytopes(p,1-2) by A5,Def26
        .= (-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;
      then
A8:   1 - 1 < n - 1 by XREAL_1:11;
      then reconsider m = n - 1 as Element of NAT by INT_1:16;
      0 < 0 qua Nat + m by A8;
      then
A9:   1 <= m by NAT_1:19;
      n - 1 <= (d + 2) - 1 by A5,XREAL_1:11;
      then
A10:  m <= d + 1;
A11:  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 A9,A10,Def28
        .= ((-1)|^n)*(num-polytopes(p,n-2));
      hence thesis by A3,A5,A11,Def26;
    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
  :Def31:
  Sum (alternating-f-vector(p)) = 0;
  compatibility
  proof
    set acs = alternating-f-vector(p);
    set aspcs = alternating-semi-proper-f-vector(p);
    acs = <*-1*> ^ aspcs by Th54;
    then
A1: Sum acs = -1 + (Sum aspcs) by Th21;
    p is eulerian implies Sum acs = 0
    proof
      assume p is eulerian;
      then Sum acs = -1 + 1 by A1,Def30
        .= 0;
      hence thesis;
    end;
    hence thesis by A1,Def30;
  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 Def5;
    hence thesis;
  end;
  suppose d > 0;
    hence thesis by Th26;
  end;
end;

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

theorem Th57:
  [#]((-1)-chain-space(p)) = { {}, {{}} }
proof
  (-1)-polytopes(p) = {{}} by Def5;
  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,Def6;
A5: {} in {{}} by TARSKI:def 1;
  0-polytopes(p) is non empty by A3,Th26;
  then
A6: [{},x] in [:{{}},0-polytopes(p):] by A1,A5,ZFMISC_1:106;
  incidence-value(e,x) = eta(p,k).(e,x) by A3,Def13
    .= 1.Z_2 by A2,A4,A6,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,Def5;
A8: x in v by A2,TARSKI:def 1;
  iseq.n = (v@x)*incidence-value(e,x) by A4,A5,A6,A7,Def16
    .= (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;
  (k-1)-polytopes(p) is non empty by A1,Def5;
  then iseq.m = (0.Z_2)*(incidence-value(e,m-th-polytope(p,k)))
  by A4,A5,A10,Def16
    .= 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);
  -1 <= k & k <= dim(p) by A1;
  then consider n being Nat such that
A4: x = n-th-polytope(p,k) and
A5: 1 <= n and
A6: n <= num-polytopes(p,k) by Th33;
  (k-1)-polytopes(p) is non empty by A1,Def5;
  then
A7: len iseq = num-polytopes(p,k) by Def16;
  dom iseq = Seg (len iseq) by FINSEQ_1:def 3;
  then
A8: n in dom iseq by A5,A6,A7,FINSEQ_1:3;
A9: iseq.n = 1.Z_2 by A1,A2,A3,A4,A5,A6,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
A10: m in dom iseq and
A11: m <> n;
    m in Seg (len iseq) by A10,FINSEQ_1:def 3;
    then 1 <= m & m <= len iseq by FINSEQ_1:3;
    hence thesis by A1,A2,A4,A5,A6,A7,A11,Th60;
  end;
  hence thesis by A8,A9,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 qua Nat - 1 as Integer;
  0-polytopes(p) is non empty by Th55;
  then reconsider v = {x} as Subset of 0-polytopes(p) by ZFMISC_1:37;
  reconsider v as Element of 0-chain-space(p);
A1: T.v = Boundary(v) by Def18;
  reconsider bv = Boundary(v) as Element of minusone-chain-space(p);
A2: minusone-polytopes(p) is non empty by Def5;
  (0 qua Nat-1)-polytopes(p) = {{}} by Def5;
  then reconsider null = {} as
  Element of (0 qua Nat-1)-polytopes(p) by TARSKI:def 1;
  null in bv iff Sum incidence-sequence(null,v) = 1.Z_2 by A2,Def17;
  then
A3: {null} c= bv by Th61,ZFMISC_1:37;
  bv c= {null}
  proof
    let y be set such that
A4: y in bv;
A5: [#](minusone-chain-space(p)) = { {}, {{}} } by Th57;
    per cases by A5,TARSKI:def 2;
    suppose bv = {};
      hence thesis by A4;
    end;
    suppose bv = {{}};
      hence thesis by A4;
    end;
  end;
  hence thesis by A1,A3,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
      .= {};
    0-polytopes(p) <> {} by Th55;
    then consider x being set such that
A3: x in 0-polytopes(p) by XBOOLE_0:def 1;
    reconsider x as Element of 0-polytopes(p) by A3;
    set v = {x};
A4: T.v = {{}} by Th62;
A5: dom T = [#](0-chain-space(p)) by RANKNULL:7;
    reconsider v as Subset of 0-polytopes(p) by A3,ZFMISC_1:37;
    reconsider v as Element of 0-chain-space(p);
A6: v in dom T by A5;
A7: {} in rng T by A2,A5,FUNCT_1:12;
    {{}} in rng T by A4,A6,FUNCT_1:12;
    then
A8: {{},{{}}} c= rng T by A7,ZFMISC_1:38;
    Card {{},{{}}} = 2 by CARD_2:76;
    then
A9: 2 c= Card rng T by A8,CARD_1:27;
A10: Card rng T = Card (T .: [#](0-chain-space(p))) by FUNCT_2:45
      .= Card [#]V by A1,RANKNULL:def 2;
    [#]V c= [#](k-chain-space(p)) by VECTSP_4:def 2;
    then Card [#]V c= Card [#](k-chain-space(p)) by CARD_1:27;
    then Card [#]V c= 2 by A1,Th56;
    hence thesis by A9,A10,XBOOLE_0:def 10;
  end;
  hence thesis by RANKNULL:6;
end;

theorem Th64:
  Card [#](dim(p)-chain-space(p)) = 2
proof
  dim(p)-polytopes(p) = {p} by Def5;
  then Card (dim(p)-polytopes(p)) = 1 by CARD_1:50;
  then Card [#]((dim(p))-chain-space(p)) = exp(2,1) by 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 Def5;
  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 qua Nat - 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 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;
  x in [#]V;
  then x in { 0.V, {p} } by 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 Def7;

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 Def7;
  egy-th-polytope(p,dim(p)) = s.egy by A1,Def12
    .= 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 Def5;
  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 Def6;
A3: dom f = [:(dim(p)-1)-polytopes(p),{p}:] by FUNCOP_1:19;
  c in {p} by A1,TARSKI:def 1;
  then [x,c] in dom f by A3,ZFMISC_1:106;
  then f.(x,c) in rng f by FUNCT_1:12;
  then f.(x,c) in {1.Z_2} by FUNCOP_1:14;
  then f.(x,c) = 1.Z_2 by TARSKI:def 1;
  hence thesis by A2,Def13;
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);
  num-polytopes(p,dim(p))= 1 by Th32;
  then
A2: len iseq = 1 by Def16;
  iseq.1 = 1.Z_2
  proof
    reconsider egy = 1 as Nat;
A3: egy <= num-polytopes(p,dim(p)) by Th32;
    set z = egy-th-polytope(p,dim(p));
A4: iseq.egy = (c@z)*(incidence-value(x,z)) by A3,Def16;
A5: c@z = 1.Z_2 by A1,Th73;
    incidence-value(x,z) = 1.Z_2 by Th72,Th74; :: !!!
    hence thesis by A4,A5,VECTSP_1:def 16;
  end;
  hence thesis by A2,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;
      Sum incidence-sequence(x,c) = 1.Z_2 by Th76;
      then x in Boundary(c) by Def17;
      hence thesis by Def18;
    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 B = {p};
  assume not T is one-to-one;
  then consider x1,x2 being set such that
A1: x1 in dom T and
A2: x2 in dom T and
A3: T.x1 = T.x2 and
A4: x1 <> x2 by FUNCT_1:def 8;
  reconsider x1 as Element of V by A1;
  reconsider x2 as Element of V by A2;
  per cases by A4,Th70;
  suppose
A5: x1 = 0.V;
    then
A6: x2 = B by A4,Th69;
    T.x1 = 0.U by A5,RANKNULL:9;
    hence thesis by A3,A6,Th77;
  end;
  suppose
A7: x2 = 0.V;
    then
A8: x1 = B by A4,Th69;
    T.x2 = 0.U by A7,RANKNULL:9;
    hence thesis by A3,A8,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;
  Card (dom T) = Card [#]U by RANKNULL:7
    .= 2 by Th64;
  then Card [#]V = 2 by A1,A2,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,Def26;
  0 <= n - 1
  proof
    1 - 1 = 0;
    hence thesis by A1,XREAL_1:15;
  end;
  then reconsider m = n - 1 as Element of NAT by INT_1:16;
  reconsider m as Nat;
A4: 1 <= m
  proof
A5: 2 <= n
    proof
      1 + 1 = 2;
      hence thesis by A1,INT_1:20;
    end;
    2 - 1 = 1;
    hence thesis by A5,XREAL_1:15;
  end;
  m <= dim(p)
  proof
    n < (dim(p) + 1) + 1 by A2;
    then n <= dim(p) + 1 by NAT_1:13;
    then n - 1 <= (dim(p) + 1) - 1 by XREAL_1:11;
    hence thesis;
  end;
  then apcs.m = ((-1)|^(m+1))*num-polytopes(p,m-1) by A4,Def27;
  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 Def26;
A2: len apcs = n by Def27;
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;
      o - 2 = -1;
      then
A10:  acs.o = ((-1)|^o)*num-polytopes(p,-1) by A9,Def26;
A11:  (-1)|^1 = -1 by Th4,Th9;
      num-polytopes(p,-1) = 1 by Th31;
      hence thesis by A8,A10,A11,Th17;
    end;
    suppose
A12:  k = n + 2;
      then 1 <= k by Th12;
      then
A13:  acs.k = ((-1)|^k)*num-polytopes(p,k-2) by A12,Def26;
A14:  r.k = (-1)|^k
      proof
        k = (len <*-1*> + len (apcs) + 1)
        proof
          len <*-1*> = 1 by FINSEQ_1:56;
          hence thesis by A2,A12;
        end;
        then r.k = (-1)|^(dim(p)) by Th18
          .= (-1)|^k by A12,Th14;
        hence thesis;
      end;
      num-polytopes(p,k-2) = 1 by A12,Th32;
      hence thesis by A13,A14;
    end;
    suppose
A15:  1 < k & k < n + 2;
      set m = k - 1;
A16:  len <*-1*> = 1 by FINSEQ_1:56;
      k <= len (<*-1*> ^ apcs)
      proof
A17:    len (<*-1*> ^ apcs) = (len <*-1*> + len apcs) by FINSEQ_1:35
          .= n + 1 by A2,FINSEQ_1:56;
A18:    k + 1 <= n + 2 by A15,INT_1:20;
A19:    (k + 1) - 1 = k;
        (n + 2) - 1 = n + 1;
        hence thesis by A17,A18,A19,XREAL_1:11;
      end;
      then r.k = apcs.m by A15,A16,Th19;
      hence thesis by A15,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 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,Def27;
  reconsider egy = 1 as Nat;
A3: apcs.egy = (-1)|^(egy+1)*num-polytopes(p,egy-1) by A1,Def27;
  (-1)|^(egy+1) = 1 by Th5,Th8;
  then apcs = <*num-polytopes(p,0)*> by A2,A3,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,Def27;
  reconsider o = 1 as Nat;
  reconsider t = 2 as Nat;
A3: apcs.o = ((-1)|^(o+1))*num-polytopes(p,o-1) by A1,Def27;
A4: apcs.t = ((-1)|^(t+1))*num-polytopes(p,t-1) by A1,Def27;
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;
  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,Def27;
  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,Def27;
A7: apcs.tw = mo*num-polytopes(p,tw-1) by A1,A4,Def27;
A8: apcs.th = o*num-polytopes(p,th-1) by A1,A5,Def27;
  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;
  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);
  (-1)|^(d+1) = -1 by A1,NEWTON:10;
  then
A2: 1 + (-1)|^(d+1) = 0;
  len apcs = 0 by A1,Def27;
  then apcs = <*>INT;
  hence thesis by A2,Def29,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 dim(p) > 0;
    then
A2: len apcs > 0 by Def27;

:: 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
A3: len a = len apcs and
A4: for n being Nat st n in dom a holds a.n = A(n) from FINSEQ_1:sch 2;
    consider b being FinSequence such that
A5: len b = len apcs and
A6: for n being Nat st n in dom b holds b.n = B(n) from FINSEQ_1:sch 2;
    rng a c= INT & rng b c= INT
    proof
      thus rng a c= INT
      proof
        let y be set such that
A7:     y in rng a;
        consider x being set such that
A8:     x in dom a and
A9:     y = a.x by A7,FUNCT_1:def 5;
        reconsider x as Element of NAT by A8;
        a.x = ((-1)|^(x+1))*(dim ((x-2)-bounding-chain-space(p))) by A4,A8;
        hence thesis by A9;
      end;
      thus rng b c= INT
      proof
        let y be set such that
A10:    y in rng b;
        consider x being set such that
A11:    x in dom b and
A12:    y = b.x by A10,FUNCT_1:def 5;
        reconsider x as Element of NAT by A11;
        b.x = ((-1)|^(x+1))*(dim ((x-1)-circuit-space(p))) by A6,A11;
        hence thesis by A12;
      end;
    end;
    then reconsider a,b as FinSequence of INT by FINSEQ_1:def 4;
A13: for n being Nat st 1 <= n & n <= len apcs holds apcs.n = a.n + b.n
    proof
      let n be Nat such that
A14:  1 <= n and
A15:  n <= len apcs;
A16:  apcs.n = ((-1)|^(n+1))*(dim ((n-2)-bounding-chain-space(p)))
      + ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p))) by A14,A15,Th52;
      reconsider n' = n as Element of NAT by ORDINAL1:def 13;
A17:  n' in dom b by A14,A15,FINSEQ_3:27,A5;
      n' in dom a by A14,A15,FINSEQ_3:27,A3;
      then a.n' = ((-1)|^(n'+1))*(dim ((n'-2)-bounding-chain-space(p))) by A4;
      hence thesis by A6,A16,A17;
    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.
    for n being Nat st 1 <= n & n < len apcs holds b.n = -(a.(n+1))
    proof
      let n be Nat such that
A18:  1 <= n and
A19:  n < len apcs;
A20:  n in dom b by A18,A19,FINSEQ_3:27,A5;
      reconsider n as Element of NAT by ORDINAL1:def 13;
A21:  b.n = ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p))) by A6,A20;
A22:  n + 1 <= len apcs by A19,INT_1:20;
      1 <= n + 1 by NAT_1:11;
      then n + 1 in dom a by A22,FINSEQ_3:27,A3;
      then a.(n+1) = A(n+1) by A4
        .= (((-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,A21,Th51;
      hence thesis;
    end;
    then
A23: Sum apcs = (a.1) + (b.(len apcs)) by A2,A3,A5,A13,Th15;
A24: a.1 = 1
    proof
      reconsider egy = 1 as Element of NAT;
      1 <= 0 qua Nat + 1;
      then egy <= len apcs by A2,NAT_1:13;
      then egy in dom a by FINSEQ_3:27,A3;
      then a.egy = ((-1)|^(1+1))*(dim ((egy-2)-bounding-chain-space(p))) by A4
        .= 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;
A25:  n = dim(p) by Def27;
      0 qua Nat + 1 = 1;
      then 1 <= len apcs by A2,NAT_1:13;
      then n in dom b by FINSEQ_3:27,A5;
      then b.n = B(n) by A6
        .= ((-1)|^(n+1))*1 by A1,A25,Th80
        .= (-1)|^(n+1);
      hence thesis by Def27;
    end;
    hence thesis by A23,A24,Def29;
  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);
  p is eulerian by A1,Th89;
  then 0 = Sum acs by Def31
    .= 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,Def31
    .= 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,Def31
    .= s - 2 by A2,A4,Th6,Th83;
  hence thesis;
end;