:: POLYFORM semantic presentation

begin

theorem Th1: :: POLYFORM:1
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 ; ::_thesis: ( ex a, b being set st
( a <> b & X = {a,b} ) & c in X & d in X & c <> d implies X = {c,d} )
assume 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 ; ::_thesis: X = {c,d}
consider a, b being set  such that
 a <> b and
A5: X = {a,b} by A1;
A6: X c= {c,d}
proof
A7: ( d = a or d = b ) by A3, A5, TARSKI:def_2;
A8: ( c = a or c = b ) by A2, A5, TARSKI:def_2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in {c,d} )
assume A9: x in X ; ::_thesis: x in {c,d}
percases ( x = a or x = b ) by A5, A9, TARSKI:def_2;
suppose x = a ; ::_thesis: x in {c,d}
hence  x in {c,d} by A4, A8, A7, TARSKI:def_2; ::_thesis: verum
end;
suppose x = b ; ::_thesis: x in {c,d}
hence  x in {c,d} by A4, A8, A7, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
 {c,d} c= X by A2, A3, ZFMISC_1:32;
hence  X = {c,d} by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

begin


theorem :: POLYFORM:2
canceled;

theorem Th3: :: POLYFORM:3
for k being Integer st 1 <= k holds
k is Nat
proof
let k be Integer; ::_thesis: ( 1 <= k implies k is Nat )
assume  1 <= k ; ::_thesis: k is Nat
then reconsider k = k as Element of NAT by INT_1:3;
 k is Nat ;
hence  k is Nat ; ::_thesis: verum
end;

definition
let a be Integer;
let b be Nat;
:: original: *
redefine funca * b ->  Element of INT ;
coherence
 a * b is Element of INT by INT_1:def_2;
end;

theorem Th4: :: POLYFORM:4
1 is odd
proof
 1 = (2 * 0) + 1 ;
hence  1 is odd ; ::_thesis: verum
end;

theorem Th5: :: POLYFORM:5
2 is even
proof
 2 = 2 * 1 ;
hence  2 is even ; ::_thesis: verum
end;

theorem Th6: :: POLYFORM:6
3 is odd
proof
 3 = (2 * 1) + 1 ;
hence  3 is odd ; ::_thesis: verum
end;

theorem Th7: :: POLYFORM:7
4 is even
proof
 4 = 2 * 2 ;
hence  4 is even ; ::_thesis: verum
end;

theorem Th8: :: POLYFORM:8
for n being Nat st n is even holds
(- 1) |^ n = 1
proof
let n be Nat; ::_thesis: ( n is even implies (- 1) |^ n = 1 )
assume A1: n is even ; ::_thesis: (- 1) |^ n = 1
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 (- 1) |^ n = (- 1) to_power n by POWER:41;
hence  (- 1) |^ n = 1 by A1, FIB_NUM2:3; ::_thesis: verum
end;

theorem Th9: :: POLYFORM:9
for n being Nat st n is odd holds
(- 1) |^ n = - 1
proof
let n be Nat; ::_thesis: ( n is odd implies (- 1) |^ n = - 1 )
assume A1: n is odd ; ::_thesis: (- 1) |^ n = - 1
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 (- 1) |^ n = (- 1) to_power n by POWER:41;
hence  (- 1) |^ n = - 1 by A1, FIB_NUM2:2; ::_thesis: verum
end;

theorem Th10: :: POLYFORM:10
for n being Nat holds (- 1) |^ n is Integer
proof
let n be Nat; ::_thesis: (- 1) |^ n is Integer
percases ( n is even or n is odd ) ;
suppose n is even ; ::_thesis: (- 1) |^ n is Integer
hence  (- 1) |^ n is Integer by Th8; ::_thesis: verum
end;
suppose n is odd ; ::_thesis: (- 1) |^ n is Integer
hence  (- 1) |^ n is Integer by Th9; ::_thesis: verum
end;
end;
end;

definition
let a be Integer;
let n be Nat;
:: original: |^
redefine funca |^ n ->  Element of INT ;
coherence
 a |^ n is Element of INT
proof
consider b being Element of NAT  such that
A1: ( a = b or a = - b ) by INT_1:2;
percases ( a = b or a = - b ) by A1;
suppose a = b ; ::_thesis: a |^ n is Element of INT
then reconsider a = a as Element of NAT ;
reconsider s = a |^ n as Element of NAT by ORDINAL1:def_12;
 s in NAT ;
hence  a |^ n is Element of INT by NUMBERS:17; ::_thesis: verum
end;
supposeA2: a = - b ; ::_thesis: a |^ n is Element of INT
reconsider bn = b |^ n as Element of NAT by ORDINAL1:def_12;
 (- 1) |^ n is Integer by Th10;
then reconsider l = (- 1) |^ n as Element of INT by INT_1:def_2;
 - b = (- 1) * b ;
then  a |^ n = l * bn by A2, NEWTON:7;
hence  a |^ n is Element of INT ; ::_thesis: verum
end;
end;
end;
end;

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

theorem Th11: :: POLYFORM:11
for p, q, r being FinSequence holds len (p ^ q) <= len (p ^ (q ^ r))
proof
let p, q, r be FinSequence; ::_thesis: len (p ^ q) <= len (p ^ (q ^ r))
 len ((p ^ q) ^ r) = len (p ^ (q ^ r)) by FINSEQ_1:32;
hence  len (p ^ q) <= len (p ^ (q ^ r)) by CALCUL_1:6; ::_thesis: verum
end;

theorem Th12: :: POLYFORM:12
for n being Nat holds 1 < n + 2
proof
let n be Nat; ::_thesis: 1 < n + 2
 ( 0 < n + 1 implies 1 < n + 2 )
proof
assume  0 < n + 1 ; ::_thesis: 1 < n + 2
 0 + 1 = 1 ;
hence  1 < n + 2 by XREAL_1:8; ::_thesis: verum
end;
hence  1 < n + 2 ; ::_thesis: verum
end;

theorem Th13: :: POLYFORM:13
(- 1) |^ 2 = 1
proof
(- 1) |^ 2 = (- 1) |^ (1 + 1)
.= ((- 1) |^ 1) * ((- 1) |^ 1) by NEWTON:8
.= ((- 1) |^ 1) * (- 1) by NEWTON:5
.= (- 1) * (- 1) by NEWTON:5 ;
hence  (- 1) |^ 2 = 1 ; ::_thesis: verum
end;

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

begin

theorem Th15: :: POLYFORM:15
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
defpred S1[ 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)) );
A1: for p being FinSequence of INT
for x being Element of INT st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of INT ; ::_thesis: for x being Element of INT st S1[p] holds
S1[p ^ <*x*>]
let x be Element of INT ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: S1[p] ; ::_thesis: S1[p ^ <*x*>]
set t = p ^ <*x*>;
assume  len (p ^ <*x*>) > 0 ; ::_thesis: for a, b being FinSequence of INT st len a = len (p ^ <*x*>) & len b = len (p ^ <*x*>) & ( for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ) holds
Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
let a, b be FinSequence of INT ; ::_thesis: ( len a = len (p ^ <*x*>) & len b = len (p ^ <*x*>) & ( for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ) implies Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) )
assume that
A3: len a = len (p ^ <*x*>) and
A4: len b = len (p ^ <*x*>) and
A5: for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) and
A6: for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ; ::_thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
A7: Sum (p ^ <*x*>) = (Sum p) + x by RVSUM_1:74;
percases ( len p = 0 or len p > 0 ) ;
supposeA8: len p = 0 ; ::_thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
reconsider egy = 1 as Nat ;
 p = {} by A8;
then A9: p ^ <*x*> = <*x*> by FINSEQ_1:34;
then  egy <= len (p ^ <*x*>) by FINSEQ_1:39;
then A10: (p ^ <*x*>) . egy = (a . egy) + (b . egy) by A5;
A11: p = {} by A8;
 len (p ^ <*x*>) = 1 by A9, FINSEQ_1:39;
hence  Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A7, A11, A9, A10, FINSEQ_1:40, GR_CY_1:3; ::_thesis: verum
end;
supposeA12: len p > 0 ; ::_thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
set m = len p;
set a9 = a | (len p);
A13: (a | (len p)) . 1 = a . 1
proof
reconsider egy = 1 as Element of NAT ;
 0 + 1 = 1 ;
then  egy <= len p by A12, INT_1:7;
hence  (a | (len p)) . 1 = a . 1 by FINSEQ_3:112; ::_thesis: verum
end;
set b9 = b | (len p);
A14: b . (len p) = (b | (len p)) . (len p) by FINSEQ_3:112;
A15: for n being Nat st 1 <= n & n < len p holds
(b | (len p)) . n = - ((a | (len p)) . (n + 1))
proof
let n be Nat; ::_thesis: ( 1 <= n & n < len p implies (b | (len p)) . n = - ((a | (len p)) . (n + 1)) )
assume that
A16: 1 <= n and
A17: n < len p ; ::_thesis: (b | (len p)) . n = - ((a | (len p)) . (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A18: (b | (len p)) . n = b . n by A17, FINSEQ_3:112;
 n + 1 <= len p by A17, INT_1:7;
then A19: (a | (len p)) . (n + 1) = a . (n + 1) by FINSEQ_3:112;
 len p <= len (p ^ <*x*>) by CALCUL_1:6;
then  n < len (p ^ <*x*>) by A17, XXREAL_0:2;
hence  (b | (len p)) . n = - ((a | (len p)) . (n + 1)) by A6, A16, A18, A19; ::_thesis: verum
end;
A20: for n being Nat st 1 <= n & n <= len p holds
p . n = ((a | (len p)) . n) + ((b | (len p)) . n)
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len p implies p . n = ((a | (len p)) . n) + ((b | (len p)) . n) )
assume that
A21: 1 <= n and
A22: n <= len p ; ::_thesis: p . n = ((a | (len p)) . n) + ((b | (len p)) . n)
 dom p = Seg (len p) by FINSEQ_1:def_3;
then A23: n in dom p by A21, A22, FINSEQ_1:1;
 len p <= len (p ^ <*x*>) by CALCUL_1:6;
then A24: n <= len (p ^ <*x*>) by A22, XXREAL_0:2;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
p . n = (p ^ <*x*>) . n by A23, FINSEQ_1:def_7
.= (a . n) + (b . n) by A5, A21, A24
.= ((a | (len p)) . n) + (b . n) by A22, FINSEQ_3:112
.= ((a | (len p)) . n) + ((b | (len p)) . n) by A22, FINSEQ_3:112 ;
hence  p . n = ((a | (len p)) . n) + ((b | (len p)) . n) ; ::_thesis: verum
end;
A25: 1 <= len p by A12, Lm1;
 len <*x*> = 1 by FINSEQ_1:39;
then A26: len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:22;
 0 + (len p) = len p ;
then  len p < len (p ^ <*x*>) by A26, XREAL_1:6;
then A27: b . (len p) = - (a . ((len p) + 1)) by A6, A25;
 0 + 1 = 1 ;
then A28: 1 <= len (p ^ <*x*>) by A26, XREAL_1:6;
A29: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42
.= (- ((b | (len p)) . (len p))) + (b . (len (p ^ <*x*>))) by A5, A26, A28, A27, A14 ;
 len p <= len b by A4, CALCUL_1:6;
then A30: len (b | (len p)) = len p by FINSEQ_1:59;
 len p <= len a by A3, CALCUL_1:6;
then  len (a | (len p)) = len p by FINSEQ_1:59;
then  Sum p = ((a | (len p)) . 1) + ((b | (len p)) . (len p)) by A2, A12, A30, A20, A15;
hence  Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A7, A13, A29; ::_thesis: verum
end;
end;
end;
A31: S1[ <*> INT] ;
A32: for p being FinSequence of INT holds S1[p] from FINSEQ_2:sch_2(A31, A1);
let a, b, s be FinSequence of INT ; ::_thesis: ( 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)) ) implies Sum s = (a . 1) + (b . (len s)) )
assume  ( 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)) ) ) ; ::_thesis: Sum s = (a . 1) + (b . (len s))
hence  Sum s = (a . 1) + (b . (len s)) by A32; ::_thesis: verum
end;

theorem Th16: :: POLYFORM:16
for p, q, r being FinSequence holds len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)
proof
let p, q, r be FinSequence; ::_thesis: len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)
len ((p ^ q) ^ r) = (len (p ^ q)) + (len r) by FINSEQ_1:22
.= ((len p) + (len q)) + (len r) by FINSEQ_1:22 ;
hence  len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r) ; ::_thesis: verum
end;

theorem Th17: :: POLYFORM:17
for x being set
for p, q being FinSequence holds ((<*x*> ^ p) ^ q) . 1 = x
proof
let x be set ; ::_thesis: for p, q being FinSequence holds ((<*x*> ^ p) ^ q) . 1 = x
let p, q be FinSequence; ::_thesis: ((<*x*> ^ p) ^ q) . 1 = x
 (<*x*> ^ p) ^ q = <*x*> ^ (p ^ q) by FINSEQ_1:32;
hence  ((<*x*> ^ p) ^ q) . 1 = x by FINSEQ_1:41; ::_thesis: verum
end;

theorem Th18: :: POLYFORM:18
for x being set
for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
proof
let x be set ; ::_thesis: for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
let p, q be FinSequence; ::_thesis: ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
set s = p ^ q;
 ((p ^ q) ^ <*x*>) . ((len (p ^ q)) + 1) = x by FINSEQ_1:42;
hence  ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x by FINSEQ_1:22; ::_thesis: verum
end;

theorem Th19: :: POLYFORM:19
for p, q, r being FinSequence
for 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; ::_thesis: for k being Nat st len p < k & k <= len (p ^ q) holds
((p ^ q) ^ r) . k = q . (k - (len p))
let k be Nat; ::_thesis: ( len p < k & k <= len (p ^ q) implies ((p ^ q) ^ r) . k = q . (k - (len p)) )
assume that
A1: len p < k and
A2: k <= len (p ^ q) ; ::_thesis: ((p ^ q) ^ r) . k = q . (k - (len p))
set n = k - (len p);
 (len p) - (len p) = 0 ;
then A3: 0 < k - (len p) by A1, XREAL_1:9;
 0 + 1 = 1 ;
then A4: 1 <= k - (len p) by A3, INT_1:7;
then reconsider n = k - (len p) as Nat by Th3;
A5: ((len p) + (len q)) - (len p) = len q ;
 k <= (len p) + (len q) by A2, FINSEQ_1:22;
then  n <= len q by A5, XREAL_1:9;
then  n in Seg (len q) by A4, FINSEQ_1:1;
then A6: n in dom q by FINSEQ_1:def_3;
 len (p ^ q) <= len (p ^ (q ^ r)) by Th11;
then  k <= len (p ^ (q ^ r)) by A2, XXREAL_0:2;
then A7: (p ^ (q ^ r)) . k = (q ^ r) . (k - (len p)) by A1, FINSEQ_1:24;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 (q ^ r) . n = q . n by A6, FINSEQ_1:def_7;
hence  ((p ^ q) ^ r) . k = q . (k - (len p)) by A7, FINSEQ_1:32; ::_thesis: verum
end;

definition
let a be Integer;
:: original: <*
redefine func<*a*> ->  FinSequence of INT ;
coherence
 <*a*> is FinSequence of INT
proof
set s = <*a*>;
 a in INT by INT_1:def_2;
then  ( rng <*a*> = {a} & {a} c= INT ) by FINSEQ_1:38, ZFMISC_1:31;
hence  <*a*> is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

definition
let a, b be Integer;
:: original: <*
redefine func<*a,b*> ->  FinSequence of INT ;
coherence
 <*a,b*> is FinSequence of INT
proof
set s = <*a,b*>;
 ( a in INT & b in INT ) by INT_1:def_2;
then  ( rng <*a,b*> = {a,b} & {a,b} c= INT ) by FINSEQ_2:127, ZFMISC_1:32;
hence  <*a,b*> is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

definition
let a, b, c be Integer;
:: original: <*
redefine func<*a,b,c*> ->  FinSequence of INT ;
coherence
 <*a,b,c*> is FinSequence of INT
proof
set s = <*a,b,c*>;
A1: c in INT by INT_1:def_2;
 ( a in INT & b in INT ) by INT_1:def_2;
then  ( rng <*a,b,c*> = {a,b,c} & {a,b,c} c= INT ) by A1, FINSEQ_2:128, ZFMISC_1:133;
hence  <*a,b,c*> is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

definition
let p, q be FinSequence of INT ;
:: original: ^
redefine funcp ^ q ->  FinSequence of INT ;
coherence
 p ^ q is FinSequence of INT by FINSEQ_1:75;
end;

theorem Th20: :: POLYFORM:20
for k being Integer
for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)
proof
let k be Integer; ::_thesis: for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)
let p be FinSequence of INT ; ::_thesis: Sum (<*k*> ^ p) = k + (Sum p)
reconsider k = k as Element of INT by INT_1:def_2;
Sum (<*k*> ^ p) = (Sum p) + (Sum <*k*>) by RVSUM_1:75
.= Sum (p ^ <*k*>) by RVSUM_1:75
.= k + (Sum p) by RVSUM_1:74 ;
hence  Sum (<*k*> ^ p) = k + (Sum p) ; ::_thesis: verum
end;

theorem Th21: :: POLYFORM:21
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 ; ::_thesis: Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)
Sum ((p ^ q) ^ r) = (Sum (p ^ q)) + (Sum r) by RVSUM_1:75
.= ((Sum p) + (Sum q)) + (Sum r) by RVSUM_1:75 ;
hence  Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r) ; ::_thesis: verum
end;

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

begin

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 Th23: :: POLYFORM:23
for X, Y being set holds [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y
proof
let X, Y be set ; ::_thesis: [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y
set f = [:X,Y:] --> (1. Z_2);
 ( rng ([:X,Y:] --> (1. Z_2)) c= {(1. Z_2)} & {(1. Z_2)} c= {(0. Z_2),(1. Z_2)} ) by FUNCOP_1:13, ZFMISC_1:7;
then  ( dom ([:X,Y:] --> (1. Z_2)) = [:X,Y:] & rng ([:X,Y:] --> (1. Z_2)) c= {(0. Z_2),(1. Z_2)} ) by FUNCOP_1:13, XBOOLE_1:1;
hence  [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y by FUNCT_2:def_2; ::_thesis: verum
end;

definition
attrc1 is strict ;
struct PolyhedronStr  -> ;
aggrPolyhedronStr(# PolytopsF, IncidenceF #) ->  PolyhedronStr ;
sel PolytopsF c1 ->  FinSequence-yielding FinSequence;
sel IncidenceF c1 ->  Function-yielding FinSequence;
end;

definition
let p be PolyhedronStr ;
attrp is polyhedron_1  means :Def1: :: POLYFORM:def 1
 len the IncidenceF of p = (len the PolytopsF of p) - 1;
attrp is polyhedron_2  means :Def2: :: POLYFORM:def 2
 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)));
attrp is polyhedron_3  means :Def3: :: POLYFORM:def 3
 for n being Nat st 1 <= n & n <= len the PolytopsF of p holds
( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one );
end;

:: deftheorem Def1 defines polyhedron_1 POLYFORM:def_1_:_
 for p being PolyhedronStr holds
( p is polyhedron_1 iff len the IncidenceF of p = (len the PolytopsF of p) - 1 );

:: deftheorem Def2 defines polyhedron_2 POLYFORM:def_2_:_
 for p being PolyhedronStr holds
( p is polyhedron_2 iff 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))) );

:: deftheorem Def3 defines polyhedron_3 POLYFORM:def_3_:_
 for p being PolyhedronStr holds
( p is polyhedron_3 iff for n being Nat st 1 <= n & n <= len the PolytopsF of p holds
( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) );

registration
cluster polyhedron_1 polyhedron_2 polyhedron_3 for PolyhedronStr ;
existence
 ex b1 being PolyhedronStr st
( b1 is polyhedron_1 & b1 is polyhedron_2 & b1 is polyhedron_3 )
proof
reconsider I = <*> {} as Function-yielding FinSequence ;
reconsider F = <*<*{}*>*> as FinSequence-yielding FinSequence ;
take p = PolyhedronStr(# F,I #); ::_thesis: ( p is polyhedron_1 & p is polyhedron_2 & p is polyhedron_3 )
A1: len F = 1 by FINSEQ_1:39;
 len I = 1 - 1 ;
hence  p is polyhedron_1 by A1, Def1; ::_thesis: ( p is polyhedron_2 & p is polyhedron_3 )
 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; ::_thesis: p is polyhedron_3
let n be Nat; :: according to POLYFORM:def_3 ::_thesis: ( 1 <= n & n <= len the PolytopsF of p implies ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) )
assume  ( 1 <= n & n <= len the PolytopsF of p ) ; ::_thesis: ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one )
then  n = 1 by A1, XXREAL_0:1;
hence  ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) by FINSEQ_1:def_8; ::_thesis: verum
end;
end;

definition
mode polyhedron is polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr ;
end;


definition
let p be polyhedron;
func dim p ->  Element of NAT  equals :: POLYFORM:def 4
 len the PolytopsF of p;
coherence
 len the PolytopsF of p is Element of NAT ;
end;

:: deftheorem  defines dim POLYFORM:def_4_:_
 for p being polyhedron holds dim p = len the PolytopsF of p;

definition
let p be polyhedron;
let k be Integer;
funck -polytopes p ->  finite set  means :Def5: :: POLYFORM:def 5
( ( 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
 ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
proof
set F = the PolytopsF of p;
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
supposeA1: k < - 1 ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take  {} ; ::_thesis: ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) )
thus  ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) ) by A1; ::_thesis: verum
end;
supposeA2: k = - 1 ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take  {{}} ; ::_thesis: ( ( k < - 1 implies {{}} = {} ) & ( k = - 1 implies {{}} = {{}} ) & ( - 1 < k & k < dim p implies {{}} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {{}} = {p} ) & ( k > dim p implies {{}} = {} ) )
thus  ( ( k < - 1 implies {{}} = {} ) & ( k = - 1 implies {{}} = {{}} ) & ( - 1 < k & k < dim p implies {{}} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {{}} = {p} ) & ( k > dim p implies {{}} = {} ) ) by A2; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
 (- 1) + 1 = 0 ;
then  0 <= k by A3, INT_1:7;
then reconsider k = k as Element of NAT by INT_1:3;
set n = k + 1;
reconsider Fn = the PolytopsF of p . (k + 1) as FinSequence ;
take  rng Fn ; ::_thesis: ( ( k < - 1 implies rng Fn = {} ) & ( k = - 1 implies rng Fn = {{}} ) & ( - 1 < k & k < dim p implies rng Fn = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies rng Fn = {p} ) & ( k > dim p implies rng Fn = {} ) )
thus  ( ( k < - 1 implies rng Fn = {} ) & ( k = - 1 implies rng Fn = {{}} ) & ( - 1 < k & k < dim p implies rng Fn = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies rng Fn = {p} ) & ( k > dim p implies rng Fn = {} ) ) by A3; ::_thesis: verum
end;
supposeA4: k = dim p ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take  {p} ; ::_thesis: ( ( k < - 1 implies {p} = {} ) & ( k = - 1 implies {p} = {{}} ) & ( - 1 < k & k < dim p implies {p} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {p} = {p} ) & ( k > dim p implies {p} = {} ) )
thus  ( ( k < - 1 implies {p} = {} ) & ( k = - 1 implies {p} = {{}} ) & ( - 1 < k & k < dim p implies {p} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {p} = {p} ) & ( k > dim p implies {p} = {} ) ) by A4; ::_thesis: verum
end;
supposeA5: k > dim p ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take  {} ; ::_thesis: ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) )
thus  ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) ) by A5; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being finite set st ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) & ( k < - 1 implies b2 = {} ) & ( k = - 1 implies b2 = {{}} ) & ( - 1 < k & k < dim p implies b2 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b2 = {p} ) & ( k > dim p implies b2 = {} ) holds
b1 = b2
proof
set F = the PolytopsF of p;
let X, Y be finite set ; ::_thesis: ( ( k < - 1 implies X = {} ) & ( k = - 1 implies X = {{}} ) & ( - 1 < k & k < dim p implies X = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies X = {p} ) & ( k > dim p implies X = {} ) & ( k < - 1 implies Y = {} ) & ( k = - 1 implies Y = {{}} ) & ( - 1 < k & k < dim p implies Y = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies Y = {p} ) & ( k > dim p implies Y = {} ) implies X = Y )
assume that
A6: ( k < - 1 implies X = {} ) and
A7: ( k = - 1 implies X = {{}} ) and
A8: ( - 1 < k & k < dim p implies X = rng ( the PolytopsF of p . (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 ( the PolytopsF of p . (k + 1)) ) and
A14: ( k = dim p implies Y = {p} ) and
A15: ( k > dim p implies Y = {} ) ; ::_thesis: X = Y
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < - 1 ; ::_thesis: X = Y
hence  X = Y by A6, A11; ::_thesis: verum
end;
suppose k = - 1 ; ::_thesis: X = Y
hence  X = Y by A7, A12; ::_thesis: verum
end;
suppose ( - 1 < k & k < dim p ) ; ::_thesis: X = Y
hence  X = Y by A8, A13; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: X = Y
hence  X = Y by A9, A14; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: X = Y
hence  X = Y by A10, A15; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def5 defines -polytopes POLYFORM:def_5_:_
 for p being polyhedron
for k being Integer
for b3 being finite set holds
( b3 = k -polytopes p iff ( ( k < - 1 implies b3 = {} ) & ( k = - 1 implies b3 = {{}} ) & ( - 1 < k & k < dim p implies b3 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b3 = {p} ) & ( k > dim p implies b3 = {} ) ) );

theorem Th24: :: POLYFORM:24
for p being polyhedron
for k being Integer st - 1 < k & k < dim p holds
( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
proof
let p be polyhedron; ::_thesis: for k being Integer st - 1 < k & k < dim p holds
( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
let k be Integer; ::_thesis: ( - 1 < k & k < dim p implies ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) )
A1: (- 1) + 1 = 0 ;
assume  - 1 < k ; ::_thesis: ( not k < dim p or ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) )
then A2: 0 < k + 1 by A1, XREAL_1:6;
then reconsider n = k + 1 as Element of NAT by INT_1:3;
A3: ( n is Nat & 0 + 1 = 1 ) ;
assume  k < dim p ; ::_thesis: ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
hence  ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) by A2, A3, INT_1:7; ::_thesis: verum
end;

theorem Th25: :: POLYFORM:25
for p being polyhedron
for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
proof
let p be polyhedron; ::_thesis: for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
let k be Integer; ::_thesis: ( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
set X = k -polytopes p;
thus  ( not k -polytopes p is empty implies ( - 1 <= k & k <= dim p ) ) by Def5; ::_thesis: ( - 1 <= k & k <= dim p implies not k -polytopes p is empty )
thus  ( - 1 <= k & k <= dim p implies not k -polytopes p is empty ) ::_thesis: verum
proof
assume A1: - 1 <= k ; ::_thesis: ( not k <= dim p or not k -polytopes p is empty )
assume A2: k <= dim p ; ::_thesis: not k -polytopes p is empty
percases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A1, A2, XXREAL_0:1;
suppose k = - 1 ; ::_thesis: not k -polytopes p is empty
hence  not k -polytopes p is empty by Def5; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: not k -polytopes p is empty
set F = the PolytopsF of p;
A4: k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A3, Def5;
set n = k + 1;
A5: 1 <= k + 1 by A3, Th24;
A6: k + 1 <= dim p by A3, Th24;
reconsider n = k + 1 as Element of NAT by A5, INT_1:3;
reconsider n = n as Nat ;
 not the PolytopsF of p . n is empty by A5, A6, Def3;
hence  not k -polytopes p is empty by A4; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: not k -polytopes p is empty
then  k -polytopes p = {p} by Def5;
hence  not k -polytopes p is empty ; ::_thesis: verum
end;
end;
end;
end;

theorem :: POLYFORM:26
for p being polyhedron
for k being Integer st k < dim p holds
k - 1 < dim p by XREAL_1:146, XXREAL_0:2;

definition
let p be polyhedron;
let k be Integer;
func eta (p,k) ->  incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) means :Def6: :: POLYFORM:def 6
( ( 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
 ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
proof
percases ( k < 0 or k > dim p or ( 0 < k & k < dim p ) or k = 0 or k = dim p ) by XXREAL_0:1;
supposeA1: k < 0 ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
set f = {} ;
reconsider f = {} as Function ;
 k - 1 < 0 - 1 by A1, XREAL_1:9;
then  (k - 1) -polytopes p = {} by Def5;
then  [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:90;
then reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)} by RELSET_1:12;
reconsider f = f as Element of Funcs ([:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)}) by FUNCT_2:8;
take  f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus  ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A1; ::_thesis: verum
end;
supposeA2: k > dim p ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
set f = {} ;
reconsider f = {} as Function ;
 k -polytopes p = {} by A2, Th25;
then  [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:90;
then reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)} by RELSET_1:12;
reconsider f = f as Element of Funcs ([:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)}) by FUNCT_2:8;
take  f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus  ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A2; ::_thesis: verum
end;
supposeA3: ( 0 < k & k < dim p ) ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
set F = the PolytopsF of p;
set I = the IncidenceF of p;
A4: k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A3, Def5;
A5: k - 1 < dim p by A3, XREAL_1:146, XXREAL_0:2;
 0 + 1 = 1 ;
then A6: 1 <= k by A3, INT_1:7;
then reconsider k9 = k as Nat by Th3;
 1 - 1 = 0 ;
then  - 1 < k - 1 by A6, XREAL_1:9;
then  (k - 1) -polytopes p = rng ( the PolytopsF of p . ((k - 1) + 1)) by A5, Def5;
then reconsider Ik = the IncidenceF of p . k9 as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A3, A6, A4, Def2;
take  Ik ; ::_thesis: ( ( k < 0 implies Ik = {} ) & ( k = 0 implies Ik = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies Ik = the IncidenceF of p . k ) & ( k = dim p implies Ik = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies Ik = {} ) )
thus  ( ( k < 0 implies Ik = {} ) & ( k = 0 implies Ik = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies Ik = the IncidenceF of p . k ) & ( k = dim p implies Ik = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies Ik = {} ) ) by A3; ::_thesis: verum
end;
supposeA7: k = 0 ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
percases ( k = dim p or k <> dim p ) ;
supposeA8: k = dim p ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
set f = [:{{}},{p}:] --> (1. Z_2);
reconsider f = [:{{}},{p}:] --> (1. Z_2) as incidence-matrix of {{}},{p} by Th23;
 (k - 1) -polytopes p = {{}} by A7, Def5;
then reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A8, Def5;
take  f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus  ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A7, A8, Def5; ::_thesis: verum
end;
supposeA9: k <> dim p ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
set f = [:{{}},(0 -polytopes p):] --> (1. Z_2);
reconsider f = [:{{}},(0 -polytopes p):] --> (1. Z_2) as incidence-matrix of {{}},(0 -polytopes p) by Th23;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A7, Def5;
take  f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus  ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A7, A9; ::_thesis: verum
end;
end;
end;
supposeA10: k = dim p ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
percases ( k = 0 or k <> 0 ) ;
supposeA11: k = 0 ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
set f = [:{{}},{p}:] --> (1. Z_2);
reconsider f = [:{{}},{p}:] --> (1. Z_2) as incidence-matrix of {{}},{p} by Th23;
 (k - 1) -polytopes p = {{}} by A11, Def5;
then reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A10, Def5;
take  f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus  ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A10, A11, Def5; ::_thesis: verum
end;
supposeA12: k <> 0 ; ::_thesis: ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) )
set f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2);
reconsider f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) as incidence-matrix of (((dim p) - 1) -polytopes p),{p} by Th23;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A10, Def5;
take  f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus  ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A10, A12; ::_thesis: verum
end;
end;
end;
end;
end;
uniqueness
 for b1, b2 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b1 = {} ) & ( k < 0 implies b2 = {} ) & ( k = 0 implies b2 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b2 = the IncidenceF of p . k ) & ( k = dim p implies b2 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b2 = {} ) holds
b1 = b2
proof
set I = the IncidenceF of p;
let s, t be incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p); ::_thesis: ( ( k < 0 implies s = {} ) & ( k = 0 implies s = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies s = the IncidenceF of p . k ) & ( k = dim p implies s = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies s = {} ) & ( k < 0 implies t = {} ) & ( k = 0 implies t = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies t = the IncidenceF of p . k ) & ( k = dim p implies t = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies t = {} ) implies s = t )
assume that
A13: ( k < 0 implies s = {} ) and
A14: ( k = 0 implies s = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) and
A15: ( 0 < k & k < dim p implies s = the IncidenceF of p . k ) and
A16: ( k = dim p implies s = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) and
A17: ( k > dim p implies s = {} ) and
A18: ( k < 0 implies t = {} ) and
A19: ( k = 0 implies t = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) and
A20: ( 0 < k & k < dim p implies t = the IncidenceF of p . k ) and
A21: ( k = dim p implies t = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) and
A22: ( k > dim p implies t = {} ) ; ::_thesis: s = t
percases ( k < 0 or k = 0 or ( 0 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < 0 ; ::_thesis: s = t
hence  s = t by A13, A18; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: s = t
hence  s = t by A14, A19; ::_thesis: verum
end;
suppose ( 0 < k & k < dim p ) ; ::_thesis: s = t
hence  s = t by A15, A20; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: s = t
hence  s = t by A16, A21; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: s = t
hence  s = t by A17, A22; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def6 defines eta POLYFORM:def_6_:_
 for p being polyhedron
for k being Integer
for b3 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) holds
( b3 = eta (p,k) iff ( ( k < 0 implies b3 = {} ) & ( k = 0 implies b3 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b3 = the IncidenceF of p . k ) & ( k = dim p implies b3 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b3 = {} ) ) );

definition
let p be polyhedron;
let k be Integer;
funck -polytope-seq p ->  FinSequence means :Def7: :: POLYFORM:def 7
( ( 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
 ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
proof
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
supposeA1: k < - 1 ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take  <*> {} ; ::_thesis: ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) )
thus  ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) ) by A1; ::_thesis: verum
end;
supposeA2: k = - 1 ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take  <*{}*> ; ::_thesis: ( ( k < - 1 implies <*{}*> = <*> {} ) & ( k = - 1 implies <*{}*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*{}*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*{}*> = <*p*> ) & ( k > dim p implies <*{}*> = <*> {} ) )
thus  ( ( k < - 1 implies <*{}*> = <*> {} ) & ( k = - 1 implies <*{}*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*{}*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*{}*> = <*p*> ) & ( k > dim p implies <*{}*> = <*> {} ) ) by A2; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
set F = the PolytopsF of p;
take  the PolytopsF of p . (k + 1) ; ::_thesis: ( ( k < - 1 implies the PolytopsF of p . (k + 1) = <*> {} ) & ( k = - 1 implies the PolytopsF of p . (k + 1) = <*{}*> ) & ( - 1 < k & k < dim p implies the PolytopsF of p . (k + 1) = the PolytopsF of p . (k + 1) ) & ( k = dim p implies the PolytopsF of p . (k + 1) = <*p*> ) & ( k > dim p implies the PolytopsF of p . (k + 1) = <*> {} ) )
thus  ( ( k < - 1 implies the PolytopsF of p . (k + 1) = <*> {} ) & ( k = - 1 implies the PolytopsF of p . (k + 1) = <*{}*> ) & ( - 1 < k & k < dim p implies the PolytopsF of p . (k + 1) = the PolytopsF of p . (k + 1) ) & ( k = dim p implies the PolytopsF of p . (k + 1) = <*p*> ) & ( k > dim p implies the PolytopsF of p . (k + 1) = <*> {} ) ) by A3; ::_thesis: verum
end;
supposeA4: k = dim p ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take  <*p*> ; ::_thesis: ( ( k < - 1 implies <*p*> = <*> {} ) & ( k = - 1 implies <*p*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*p*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*p*> = <*p*> ) & ( k > dim p implies <*p*> = <*> {} ) )
thus  ( ( k < - 1 implies <*p*> = <*> {} ) & ( k = - 1 implies <*p*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*p*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*p*> = <*p*> ) & ( k > dim p implies <*p*> = <*> {} ) ) by A4; ::_thesis: verum
end;
supposeA5: k > dim p ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take  <*> {} ; ::_thesis: ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) )
thus  ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) ) by A5; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being FinSequence st ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) & ( k < - 1 implies b2 = <*> {} ) & ( k = - 1 implies b2 = <*{}*> ) & ( - 1 < k & k < dim p implies b2 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b2 = <*p*> ) & ( k > dim p implies b2 = <*> {} ) holds
b1 = b2
proof
set F = the PolytopsF of p;
let s, t be FinSequence; ::_thesis: ( ( k < - 1 implies s = <*> {} ) & ( k = - 1 implies s = <*{}*> ) & ( - 1 < k & k < dim p implies s = the PolytopsF of p . (k + 1) ) & ( k = dim p implies s = <*p*> ) & ( k > dim p implies s = <*> {} ) & ( k < - 1 implies t = <*> {} ) & ( k = - 1 implies t = <*{}*> ) & ( - 1 < k & k < dim p implies t = the PolytopsF of p . (k + 1) ) & ( k = dim p implies t = <*p*> ) & ( k > dim p implies t = <*> {} ) implies s = t )
assume that
A6: ( k < - 1 implies s = <*> {} ) and
A7: ( k = - 1 implies s = <*{}*> ) and
A8: ( - 1 < k & k < dim p implies s = the PolytopsF of p . (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 = the PolytopsF of p . (k + 1) ) and
A14: ( k = dim p implies t = <*p*> ) and
A15: ( k > dim p implies t = <*> {} ) ; ::_thesis: s = t
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < - 1 ; ::_thesis: s = t
hence  s = t by A6, A11; ::_thesis: verum
end;
suppose k = - 1 ; ::_thesis: s = t
hence  s = t by A7, A12; ::_thesis: verum
end;
suppose ( - 1 < k & k < dim p ) ; ::_thesis: s = t
hence  s = t by A8, A13; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: s = t
hence  s = t by A9, A14; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: s = t
hence  s = t by A10, A15; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def7 defines -polytope-seq POLYFORM:def_7_:_
 for p being polyhedron
for k being Integer
for b3 being FinSequence holds
( b3 = k -polytope-seq p iff ( ( k < - 1 implies b3 = <*> {} ) & ( k = - 1 implies b3 = <*{}*> ) & ( - 1 < k & k < dim p implies b3 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b3 = <*p*> ) & ( k > dim p implies b3 = <*> {} ) ) );

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

:: deftheorem  defines num-polytopes POLYFORM:def_8_:_
 for p being polyhedron
for k being Integer holds num-polytopes (p,k) = card (k -polytopes p);

definition
let p be polyhedron;
func num-vertices p ->  Element of NAT  equals :: POLYFORM:def 9
 num-polytopes (p,0);
correctness
coherence
num-polytopes (p,0) is Element of NAT ;
;
func num-edges p ->  Element of NAT  equals :: POLYFORM:def 10
 num-polytopes (p,1);
correctness
coherence
num-polytopes (p,1) is Element of NAT ;
;
func num-faces p ->  Element of NAT  equals :: POLYFORM:def 11
 num-polytopes (p,2);
correctness
coherence
num-polytopes (p,2) is Element of NAT ;
;
end;

:: deftheorem  defines num-vertices POLYFORM:def_9_:_
 for p being polyhedron holds num-vertices p = num-polytopes (p,0);

:: deftheorem  defines num-edges POLYFORM:def_10_:_
 for p being polyhedron holds num-edges p = num-polytopes (p,1);

:: deftheorem  defines num-faces POLYFORM:def_11_:_
 for p being polyhedron holds num-faces p = num-polytopes (p,2);

theorem Th27: :: POLYFORM:27
for p being polyhedron
for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
proof
let p be polyhedron; ::_thesis: for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
let k be Integer; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
set F = the PolytopsF of p;
percases ( k < - 1 or ( - 1 <= k & k <= dim p ) or k > dim p ) ;
suppose k < - 1 ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then  ( k -polytope-seq p = <*> {} & k -polytopes p = {} ) by Def5, Def7;
hence  dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by FINSEQ_1:def_3; ::_thesis: verum
end;
supposeA1: ( - 1 <= k & k <= dim p ) ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
percases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A1, XXREAL_0:1;
supposeA2: k = - 1 ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then  k -polytope-seq p = <*{}*> by Def7;
then A3: len (k -polytope-seq p) = 1 by FINSEQ_1:39;
 k -polytopes p = {{}} by A2, Def5;
then  num-polytopes (p,k) = 1 by CARD_2:42;
hence  dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def_3; ::_thesis: verum
end;
supposeA4: ( - 1 < k & k < dim p ) ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
set n = k + 1;
reconsider n = k + 1 as Nat by A4, Th24;
reconsider Fn = the PolytopsF of p . n as FinSequence ;
 ( 1 <= n & n <= dim p ) by A4, Th24;
then A5: Fn is one-to-one by Def3;
 k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A4, Def5;
then  num-polytopes (p,k) = card (dom Fn) by A5, CARD_1:70;
then A6: len Fn = num-polytopes (p,k) by CARD_1:62;
 k -polytope-seq p = the PolytopsF of p . (k + 1) by A4, Def7;
hence  dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A6, FINSEQ_1:def_3; ::_thesis: verum
end;
supposeA7: k = dim p ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then  k -polytope-seq p = <*p*> by Def7;
then A8: len (k -polytope-seq p) = 1 by FINSEQ_1:39;
 k -polytopes p = {p} by A7, Def5;
then  num-polytopes (p,k) = 1 by CARD_2:42;
hence  dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A8, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;
suppose k > dim p ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then  ( k -polytope-seq p = <*> {} & k -polytopes p = {} ) by Def5, Def7;
hence  dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;

theorem Th28: :: POLYFORM:28
for p being polyhedron
for k being Integer holds len (k -polytope-seq p) = num-polytopes (p,k)
proof
let p be polyhedron; ::_thesis: for k being Integer holds len (k -polytope-seq p) = num-polytopes (p,k)
let k be Integer; ::_thesis: len (k -polytope-seq p) = num-polytopes (p,k)
 dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by Th27;
hence  len (k -polytope-seq p) = num-polytopes (p,k) by FINSEQ_1:def_3; ::_thesis: verum
end;

theorem Th29: :: POLYFORM:29
for p being polyhedron
for k being Integer holds rng (k -polytope-seq p) = k -polytopes p
proof
let p be polyhedron; ::_thesis: for k being Integer holds rng (k -polytope-seq p) = k -polytopes p
let k be Integer; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
set F = the PolytopsF of p;
percases ( k < - 1 or ( - 1 <= k & k <= dim p ) or k > dim p ) ;
supposeA1: k < - 1 ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then  k -polytopes p = {} by Def5;
hence  rng (k -polytope-seq p) = k -polytopes p by A1, Def7, RELAT_1:38; ::_thesis: verum
end;
supposeA2: ( - 1 <= k & k <= dim p ) ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
percases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A2, XXREAL_0:1;
suppose k = - 1 ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then  ( k -polytopes p = {{}} & k -polytope-seq p = <*{}*> ) by Def5, Def7;
hence  rng (k -polytope-seq p) = k -polytopes p by FINSEQ_1:38; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then  k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by Def5;
hence  rng (k -polytope-seq p) = k -polytopes p by A3, Def7; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then  ( k -polytopes p = {p} & k -polytope-seq p = <*p*> ) by Def5, Def7;
hence  rng (k -polytope-seq p) = k -polytopes p by FINSEQ_1:38; ::_thesis: verum
end;
end;
end;
supposeA4: k > dim p ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then  k -polytopes p = {} by Def5;
hence  rng (k -polytope-seq p) = k -polytopes p by A4, Def7, RELAT_1:38; ::_thesis: verum
end;
end;
end;

theorem Th30: :: POLYFORM:30
for p being polyhedron holds num-polytopes (p,(- 1)) = 1
proof
let p be polyhedron; ::_thesis: num-polytopes (p,(- 1)) = 1
reconsider minusone = - 1 as Integer ;
 minusone -polytopes p = {{}} by Def5;
hence  num-polytopes (p,(- 1)) = 1 by CARD_1:30; ::_thesis: verum
end;

theorem Th31: :: POLYFORM:31
for p being polyhedron holds num-polytopes (p,(dim p)) = 1
proof
let p be polyhedron; ::_thesis: num-polytopes (p,(dim p)) = 1
 (dim p) -polytopes p = {p} by Def5;
hence  num-polytopes (p,(dim p)) = 1 by CARD_1:30; ::_thesis: verum
end;

definition
let p be polyhedron;
let k be Integer;
let n be Nat;
assume A1: ( 1 <= n & n <= num-polytopes (p,k) ) ;
funcn -th-polytope (p,k) ->  Element of k -polytopes p equals :Def12: :: POLYFORM:def 12
(k -polytope-seq p) . n;
coherence
 (k -polytope-seq p) . n is Element of k -polytopes p
proof
 n in Seg (num-polytopes (p,k)) by A1, FINSEQ_1:1;
then  n in dom (k -polytope-seq p) by Th27;
then  (k -polytope-seq p) . n in rng (k -polytope-seq p) by FUNCT_1:3;
hence  (k -polytope-seq p) . n is Element of k -polytopes p by Th29; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines -th-polytope POLYFORM:def_12_:_
 for p being polyhedron
for k being Integer
for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
n -th-polytope (p,k) = (k -polytope-seq p) . n;

theorem Th32: :: POLYFORM:32
for p being polyhedron
for k being Integer st - 1 <= k & k <= dim p holds
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
let p be polyhedron; ::_thesis: for k being Integer st - 1 <= k & k <= dim p holds
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) )
let k be Integer; ::_thesis: ( - 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) ) )
assume A1: ( - 1 <= k & k <= dim p ) ; ::_thesis: 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) )
let x be Element of k -polytopes p; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
percases ( k = - 1 or k = dim p or ( - 1 < k & k < dim p ) ) by A1, XXREAL_0:1;
supposeA2: k = - 1 ; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
reconsider n = 1 as Nat ;
 k -polytope-seq p = <*{}*> by A2, Def7;
then A3: (k -polytope-seq p) . n = {} by FINSEQ_1:def_8;
take  n ; ::_thesis: ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
 k -polytopes p = {{}} by A2, Def5;
then  ( x = {} & n <= num-polytopes (p,k) ) by CARD_1:30, TARSKI:def_1;
hence  ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) ) by A3, Def12; ::_thesis: verum
end;
supposeA4: k = dim p ; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
reconsider n = 1 as Nat ;
 k -polytope-seq p = <*p*> by A4, Def7;
then A5: (k -polytope-seq p) . n = p by FINSEQ_1:def_8;
take  n ; ::_thesis: ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
 k -polytopes p = {p} by A4, Def5;
then  ( x = p & num-polytopes (p,k) = 1 ) by CARD_1:30, TARSKI:def_1;
hence  ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) ) by A5, Def12; ::_thesis: verum
end;
supposeA6: ( - 1 < k & k < dim p ) ; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
set F = the PolytopsF of p;
A7: k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A6, Def5;
A8: (- 1) + 1 < k + 1 by A6, XREAL_1:6;
then A9: 0 + 1 <= k + 1 by INT_1:7;
reconsider k9 = k + 1 as Element of NAT by A8, INT_1:3;
 k + 1 <= dim p by A6, INT_1:7;
then  not the PolytopsF of p . k9 is empty by A9, Def3;
then consider m being set  such that
A10: m in dom ( the PolytopsF of p . k9) and
A11: ( the PolytopsF of p . k9) . m = x by A7, FUNCT_1:def_3;
reconsider Fk9 = the PolytopsF of p . k9 as FinSequence ;
reconsider m = m as Element of NAT by A10;
 dom Fk9 = Seg (len Fk9) by FINSEQ_1:def_3;
then A12: ( 1 <= m & m <= len Fk9 ) by A10, FINSEQ_1:1;
take  m ; ::_thesis: ( x = m -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) )
A13: k -polytope-seq p = the PolytopsF of p . (k + 1) by A6, Def7;
then  num-polytopes (p,k) = len ( the PolytopsF of p . (k + 1)) by Th28;
hence  ( x = m -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) ) by A13, A11, A12, Def12; ::_thesis: verum
end;
end;
end;

theorem Th33: :: POLYFORM:33
for p being polyhedron
for k being Integer holds k -polytope-seq p is one-to-one
proof
let p be polyhedron; ::_thesis: for k being Integer holds k -polytope-seq p is one-to-one
let k be Integer; ::_thesis: k -polytope-seq p is one-to-one
set s = k -polytope-seq p;
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < - 1 ; ::_thesis: k -polytope-seq p is one-to-one
hence  k -polytope-seq p is one-to-one by Def7; ::_thesis: verum
end;
suppose k = - 1 ; ::_thesis: k -polytope-seq p is one-to-one
hence  k -polytope-seq p is one-to-one by Def7; ::_thesis: verum
end;
supposeA1: ( - 1 < k & k < dim p ) ; ::_thesis: k -polytope-seq p is one-to-one
then A2: (- 1) + 1 < k + 1 by XREAL_1:6;
then reconsider m = k + 1 as Element of NAT by INT_1:3;
set F = the PolytopsF of p;
A3: 0 + 1 <= m by A2, INT_1:7;
 ( k -polytope-seq p = the PolytopsF of p . (k + 1) & m <= dim p ) by A1, Def7, INT_1:7;
hence  k -polytope-seq p is one-to-one by A3, Def3; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: k -polytope-seq p is one-to-one
then  k -polytope-seq p = <*p*> by Def7;
hence  k -polytope-seq p is one-to-one ; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: k -polytope-seq p is one-to-one
hence  k -polytope-seq p is one-to-one by Def7; ::_thesis: verum
end;
end;
end;

theorem Th34: :: POLYFORM:34
for p being polyhedron
for k being Integer
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
let p be polyhedron; ::_thesis: for k being Integer
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
let k be Integer; ::_thesis: 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
let m, n be Nat; ::_thesis: ( 1 <= n & n <= num-polytopes (p,k) & 1 <= m & m <= num-polytopes (p,k) & n -th-polytope (p,k) = m -th-polytope (p,k) implies m = n )
assume that
A1: ( 1 <= n & n <= num-polytopes (p,k) ) and
A2: ( 1 <= m & m <= num-polytopes (p,k) ) and
A3: n -th-polytope (p,k) = m -th-polytope (p,k) ; ::_thesis: m = n
set s = k -polytope-seq p;
A4: k -polytope-seq p is one-to-one by Th33;
 m in Seg (num-polytopes (p,k)) by A2, FINSEQ_1:1;
then A5: m in dom (k -polytope-seq p) by Th27;
 n in Seg (num-polytopes (p,k)) by A1, FINSEQ_1:1;
then A6: n in dom (k -polytope-seq p) by Th27;
 ( n -th-polytope (p,k) = (k -polytope-seq p) . n & m -th-polytope (p,k) = (k -polytope-seq p) . m ) by A1, A2, Def12;
hence  m = n by A3, A6, A5, A4, FUNCT_1:def_4; ::_thesis: verum
end;

definition
let p be polyhedron;
let k be Integer;
let x be Element of (k - 1) -polytopes p;
let y be Element of k -polytopes p;
assume that
A1: 0 <= k and
A2: k <= dim p ;
func incidence-value (x,y) ->  Element of Z_2 equals :Def13: :: POLYFORM:def 13
(eta (p,k)) . (x,y);
coherence
 (eta (p,k)) . (x,y) is Element of Z_2
proof
set n = eta (p,k);
A3: (k - 1) -polytopes p <> {}
proof
set m = k - 1;
 0 - 1 = - 1 ;
then A4: - 1 <= k - 1 by A1, XREAL_1:9;
 k - 1 <= (dim p) - 0 by A2, XREAL_1:13;
hence  (k - 1) -polytopes p <> {} by A4, Th25; ::_thesis: verum
end;
 ( dom (eta (p,k)) = [:((k - 1) -polytopes p),(k -polytopes p):] & k -polytopes p <> {} ) by A1, A2, Th25, FUNCT_2:92;
then  [x,y] in dom (eta (p,k)) by A3, ZFMISC_1:87;
then  (eta (p,k)) . [x,y] in rng (eta (p,k)) by FUNCT_1:3;
hence  (eta (p,k)) . (x,y) is Element of Z_2 by BSPACE:3, BSPACE:5, BSPACE:6; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines incidence-value POLYFORM:def_13_:_
 for p being polyhedron
for k being Integer
for x being Element of (k - 1) -polytopes p
for y being Element of k -polytopes p st 0 <= k & k <= dim p holds
incidence-value (x,y) = (eta (p,k)) . (x,y);

begin

definition
let p be polyhedron;
let k be Integer;
funck -chain-space p ->  finite-dimensional VectSp of Z_2  equals :: POLYFORM:def 14
 bspace (k -polytopes p);
coherence
 bspace (k -polytopes p) is finite-dimensional VectSp of Z_2 ;
end;

:: deftheorem  defines -chain-space POLYFORM:def_14_:_
 for p being polyhedron
for k being Integer holds k -chain-space p = bspace (k -polytopes p);

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

theorem Th36: :: POLYFORM:36
for p being polyhedron
for k being Integer holds num-polytopes (p,k) = dim (k -chain-space p)
proof
let p be polyhedron; ::_thesis: for k being Integer holds num-polytopes (p,k) = dim (k -chain-space p)
let k be Integer; ::_thesis: num-polytopes (p,k) = dim (k -chain-space p)
set n = dim (k -chain-space p);
 singletons (k -polytopes p) is Basis of k -chain-space p by BSPACE:40;
then  dim (k -chain-space p) = card (singletons (k -polytopes p)) by VECTSP_9:def_1;
hence  num-polytopes (p,k) = dim (k -chain-space p) by BSPACE:41; ::_thesis: verum
end;

definition
let p be polyhedron;
let k be Integer;
funck -chains p ->  non empty finite set  equals :: POLYFORM:def 15
 bool (k -polytopes p);
coherence
 bool (k -polytopes p) is non empty finite set ;
end;

:: deftheorem  defines -chains POLYFORM:def_15_:_
 for p being polyhedron
for k being Integer holds k -chains p = bool (k -polytopes p);

definition
let p be polyhedron;
let k be Integer;
let x be Element of (k - 1) -polytopes p;
let v be Element of (k -chain-space p);
func incidence-sequence (x,v) ->  FinSequence of Z_2 means :Def16: :: POLYFORM:def 16
( ( (k - 1) -polytopes p is empty implies it = <*> {} ) & ( not (k - 1) -polytopes p is 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
 ex b1 being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
proof
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: ex b1 being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
set s = <*> {};
 rng (<*> {}) 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 ; ::_thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is 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)))) ) ) ) )
thus  ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is 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)))) ) ) ) ) by A1; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: ex b1 being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
deffunc H1( Nat) ->  Element of the carrier of Z_2 = (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 = H1(n) from FINSEQ_2:sch_1();
take  s ; ::_thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is 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)))) ) ) ) )
A5: dom s = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def_3;
 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; ::_thesis: ( 1 <= n & n <= num-polytopes (p,k) implies s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) )
assume  ( 1 <= n & n <= num-polytopes (p,k) ) ; ::_thesis: s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k))))
then  n in Seg (num-polytopes (p,k)) by FINSEQ_1:1;
hence  s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) by A4, A5; ::_thesis: verum
end;
hence  ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is 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)))) ) ) ) ) by A2, A3; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being FinSequence of Z_2 st ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) & ( (k - 1) -polytopes p is empty implies b2 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b2 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b2 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) holds
b1 = b2
proof
let s, t be FinSequence of Z_2; ::_thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is 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)))) ) ) ) & ( (k - 1) -polytopes p is empty implies t = <*> {} ) & ( not (k - 1) -polytopes p is 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)))) ) ) ) implies s = t )
assume that
A6: ( (k - 1) -polytopes p is empty implies s = <*> {} ) and
A7: ( not (k - 1) -polytopes p is 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
A8: ( (k - 1) -polytopes p is empty implies t = <*> {} ) and
A9: ( not (k - 1) -polytopes p is 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)))) ) ) ) ; ::_thesis: s = t
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
suppose (k - 1) -polytopes p is empty ; ::_thesis: s = t
hence  s = t by A6, A8; ::_thesis: verum
end;
supposeA10: not (k - 1) -polytopes p is empty ; ::_thesis: s = t
 for n being Nat st 1 <= n & n <= len s holds
s . n = t . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len s implies s . n = t . n )
assume A11: ( 1 <= n & n <= len s ) ; ::_thesis: s . n = t . n
reconsider n = n as Nat ;
 s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) by A7, A10, A11;
hence  s . n = t . n by A7, A9, A10, A11; ::_thesis: verum
end;
hence  s = t by A7, A9, A10, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def16 defines incidence-sequence POLYFORM:def_16_:_
 for p being polyhedron
for k being Integer
for x being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for b5 being FinSequence of Z_2 holds
( b5 = incidence-sequence (x,v) iff ( ( (k - 1) -polytopes p is empty implies b5 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b5 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b5 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) );

theorem Th37: :: POLYFORM:37
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
proof
let p be polyhedron; ::_thesis: for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
let k be Integer; ::_thesis: for c, d being Element of (k -chain-space p)
for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
let c, d be Element of (k -chain-space p); ::_thesis: for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
let x be Element of k -polytopes p; ::_thesis: (c + d) @ x = (c @ x) + (d @ x)
 c + d = c \+\ d by BSPACE:def_5;
hence  (c + d) @ x = (c @ x) + (d @ x) by BSPACE:15; ::_thesis: verum
end;

theorem Th38: :: POLYFORM:38
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
proof
let p be polyhedron; ::_thesis: for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
let k be Integer; ::_thesis: for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
let c, d be Element of (k -chain-space p); ::_thesis: for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
let x be Element of (k - 1) -polytopes p; ::_thesis: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
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 = (incidence-sequence (x,c)) + (incidence-sequence (x,d));
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
then  incidence-sequence (x,d) is Tuple of 0 , the carrier of Z_2 by Def16;
then reconsider isd = incidence-sequence (x,d) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
 incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
 isc + isd is Element of 0 -tuples_on the carrier of Z_2 ;
hence  incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d)) by A1, Def16; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
A3: ( len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) & len ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = num-polytopes (p,k) )
proof
 len (incidence-sequence (x,d)) = num-polytopes (p,k) by A2, Def16;
then reconsider isd = incidence-sequence (x,d) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
 len (incidence-sequence (x,c)) = num-polytopes (p,k) by A2, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
reconsider s = isc + isd as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 ;
 len s = num-polytopes (p,k) by CARD_1:def_7;
hence  ( len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) & len ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = num-polytopes (p,k) ) by A2, Def16; ::_thesis: verum
end;
 for n being Nat st 1 <= n & n <= len (incidence-sequence (x,(c + d))) holds
(incidence-sequence (x,(c + d))) . n = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . n
proof
A4: ( dom ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = Seg (num-polytopes (p,k)) & len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) ) by A3, FINSEQ_1:def_3;
let m be Nat; ::_thesis: ( 1 <= m & m <= len (incidence-sequence (x,(c + d))) implies (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m )
assume A5: ( 1 <= m & m <= len (incidence-sequence (x,(c + d))) ) ; ::_thesis: (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m
set a = m -th-polytope (p,k);
set iva = incidence-value (x,(m -th-polytope (p,k)));
A6: len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) by A2, Def16;
then A7: (incidence-sequence (x,(c + d))) . m = ((c + d) @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) by A2, A5, Def16;
 m in NAT by ORDINAL1:def_12;
then A8: m in dom ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) by A4, A5;
 ( (incidence-sequence (x,c)) . m = (c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) & (incidence-sequence (x,d)) . m = (d @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) ) by A2, A5, A6, Def16;
then ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m = ((c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) + ((d @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) by A8, FVSUM_1:17
.= ((c @ (m -th-polytope (p,k))) + (d @ (m -th-polytope (p,k)))) * (incidence-value (x,(m -th-polytope (p,k)))) by VECTSP_1:def_3
.= (incidence-sequence (x,(c + d))) . m by A7, Th37 ;
hence  (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m ; ::_thesis: verum
end;
hence  incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d)) by A3, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;

theorem Th39: :: POLYFORM:39
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for 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 p be polyhedron; ::_thesis: for k being Integer
for c, d being Element of (k -chain-space p)
for 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)))
let k be Integer; ::_thesis: for c, d being Element of (k -chain-space p)
for 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)))
let c, d be Element of (k -chain-space p); ::_thesis: for 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)))
let x be Element of (k - 1) -polytopes p; ::_thesis: Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
set isc = incidence-sequence (x,c);
set isd = incidence-sequence (x,d);
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
then  incidence-sequence (x,d) = <*> the carrier of Z_2 by Def16;
then reconsider isd = incidence-sequence (x,d) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
 incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
reconsider s = isc + isd as Element of 0 -tuples_on the carrier of Z_2 ;
 Sum s = 0. Z_2 by FVSUM_1:74;
hence  Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) by RLVECT_1:def_4; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
reconsider n = num-polytopes (p,k) as Element of NAT ;
 len (incidence-sequence (x,d)) = n by A2, Def16;
then reconsider isd9 = incidence-sequence (x,d) as Element of n -tuples_on the carrier of Z_2 by FINSEQ_2:92;
 len (incidence-sequence (x,c)) = n by A2, Def16;
then reconsider isc9 = incidence-sequence (x,c) as Element of n -tuples_on the carrier of Z_2 by FINSEQ_2:92;
Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = Sum (isc9 + isd9)
.= (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) by FVSUM_1:76 ;
hence  Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) ; ::_thesis: verum
end;
end;
end;

theorem Th40: :: POLYFORM:40
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for 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 p be polyhedron; ::_thesis: for k being Integer
for c, d being Element of (k -chain-space p)
for 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)))
let k be Integer; ::_thesis: for c, d being Element of (k -chain-space p)
for 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)))
let c, d be Element of (k -chain-space p); ::_thesis: for 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)))
let x be Element of (k - 1) -polytopes p; ::_thesis: Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
Sum (incidence-sequence (x,(c + d))) = Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) by Th38
.= (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) by Th39 ;
hence  Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) ; ::_thesis: verum
end;

theorem Th41: :: POLYFORM:41
for p being polyhedron
for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
proof
let p be polyhedron; ::_thesis: for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let k be Integer; ::_thesis: for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let c be Element of (k -chain-space p); ::_thesis: for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let a be Element of Z_2; ::_thesis: for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let x be Element of k -polytopes p; ::_thesis: (a * c) @ x = a * (c @ x)
percases ( a = 0. Z_2 or a = 1. Z_2 ) by BSPACE:8;
suppose a = 0. Z_2 ; ::_thesis: (a * c) @ x = a * (c @ x)
then  ( a * (c @ x) = 0. Z_2 & a * c = 0. (k -chain-space p) ) by VECTSP_1:7, VECTSP_1:14;
hence  (a * c) @ x = a * (c @ x) by BSPACE:14; ::_thesis: verum
end;
supposeA1: a = 1. Z_2 ; ::_thesis: (a * c) @ x = a * (c @ x)
then  a * (c @ x) = c @ x by VECTSP_1:def_6;
hence  (a * c) @ x = a * (c @ x) by A1, VECTSP_1:def_17; ::_thesis: verum
end;
end;
end;

theorem Th42: :: POLYFORM:42
for p being polyhedron
for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
proof
let p be polyhedron; ::_thesis: for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
let k be Integer; ::_thesis: for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
let c be Element of (k -chain-space p); ::_thesis: for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
let a be Element of Z_2; ::_thesis: for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
let x be Element of (k - 1) -polytopes p; ::_thesis: incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
set l = incidence-sequence (x,(a * c));
set isc = incidence-sequence (x,c);
set r = a * (incidence-sequence (x,c));
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
then  incidence-sequence (x,c) = <*> the carrier of Z_2 by Def16;
then reconsider isc = incidence-sequence (x,c) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
 a * isc is Element of 0 -tuples_on the carrier of Z_2 ;
then reconsider r = a * (incidence-sequence (x,c)) as Element of 0 -tuples_on the carrier of Z_2 ;
 r = <*> the carrier of Z_2 ;
hence  incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c)) by A1, Def16; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
set n = num-polytopes (p,k);
A3: ( len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) & len (a * (incidence-sequence (x,c))) = num-polytopes (p,k) )
proof
 len (incidence-sequence (x,c)) = num-polytopes (p,k) by A2, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
set r = a * isc;
reconsider r = a * isc as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 ;
 len r = num-polytopes (p,k) by CARD_1:def_7;
hence  ( len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) & len (a * (incidence-sequence (x,c))) = num-polytopes (p,k) ) by A2, Def16; ::_thesis: verum
end;
 for m being Nat st 1 <= m & m <= len (incidence-sequence (x,(a * c))) holds
(incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m
proof
A4: dom (a * (incidence-sequence (x,c))) = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def_3;
let m be Nat; ::_thesis: ( 1 <= m & m <= len (incidence-sequence (x,(a * c))) implies (incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m )
assume A5: ( 1 <= m & m <= len (incidence-sequence (x,(a * c))) ) ; ::_thesis: (incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m
set s = m -th-polytope (p,k);
set ivs = incidence-value (x,(m -th-polytope (p,k)));
A6: len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) by A2, Def16;
then A7: (incidence-sequence (x,(a * c))) . m = ((a * c) @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) by A2, A5, Def16;
 ( len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) & m in NAT ) by A2, Def16, ORDINAL1:def_12;
then A8: m in Seg (num-polytopes (p,k)) by A5;
 (incidence-sequence (x,c)) . m = (c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) by A2, A5, A6, Def16;
then (a * (incidence-sequence (x,c))) . m = a * ((c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) by A4, A8, FVSUM_1:50
.= (a * (c @ (m -th-polytope (p,k)))) * (incidence-value (x,(m -th-polytope (p,k)))) by GROUP_1:def_3
.= (incidence-sequence (x,(a * c))) . m by A7, Th41 ;
hence  (incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m ; ::_thesis: verum
end;
hence  incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c)) by A3, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;

theorem Th43: :: POLYFORM:43
for p being polyhedron
for k being Integer
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 p be polyhedron; ::_thesis: for k being Integer
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 )
let k be Integer; ::_thesis: 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 )
let c, d be Element of (k -chain-space p); ::_thesis: ( c = d iff for x being Element of k -polytopes p holds c @ x = d @ x )
thus  ( c = d implies for x being Element of k -polytopes p holds c @ x = d @ x ) ; ::_thesis: ( ( for x being Element of k -polytopes p holds c @ x = d @ x ) implies c = d )
thus  ( ( for x being Element of k -polytopes p holds c @ x = d @ x ) implies c = d ) ::_thesis: verum
proof
assume A1: for x being Element of k -polytopes p holds c @ x = d @ x ; ::_thesis: c = d
thus  c c= d :: according to XBOOLE_0:def_10 ::_thesis: d c= c
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c or x in d )
assume A2: x in c ; ::_thesis: x in d
reconsider x = x as Element of k -polytopes p by A2;
reconsider c = c as Subset of (k -polytopes p) ;
 c @ x = 1. Z_2 by A2, BSPACE:def_3;
then  d @ x = 1. Z_2 by A1;
hence  x in d by BSPACE:9; ::_thesis: verum
end;
thus  d c= c ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in d or x in c )
assume A3: x in d ; ::_thesis: x in c
reconsider x = x as Element of k -polytopes p by A3;
reconsider d = d as Subset of (k -polytopes p) ;
 d @ x = 1. Z_2 by A3, BSPACE:def_3;
then  c @ x = 1. Z_2 by A1;
hence  x in c by BSPACE:9; ::_thesis: verum
end;
end;
end;

theorem Th44: :: POLYFORM:44
for p being polyhedron
for k being Integer
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 p be polyhedron; ::_thesis: for k being Integer
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 ) )
let k be Integer; ::_thesis: 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 ) )
let c, d be Element of (k -chain-space p); ::_thesis: ( c = d iff for x being Element of k -polytopes p holds
( x in c iff x in d ) )
thus  ( c = d implies for x being Element of k -polytopes p holds
( x in c iff x in d ) ) ; ::_thesis: ( ( for x being Element of k -polytopes p holds
( x in c iff x in d ) ) implies c = d )
thus  ( ( for x being Element of k -polytopes p holds
( x in c iff x in d ) ) implies c = d ) ::_thesis: verum
proof
assume A1: for x being Element of k -polytopes p holds
( x in c iff x in d ) ; ::_thesis: c = d
assume  c <> d ; ::_thesis: contradiction
then consider x being Element of k -polytopes p such that
A2: c @ x <> d @ x by Th43;
 ( ( x in c & not x in d ) or ( x in d & not x in c ) ) by A2, BSPACE:13;
hence  contradiction by A1; ::_thesis: verum
end;
end;

scheme :: POLYFORM:sch 1
ChainEx{ F1() ->  polyhedron, F2() ->  Integer, P1[ Element of F2() -polytopes F1()] } :
 ex c being Subset of (F2() -polytopes F1()) st
for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
proof
set c =  {  x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() )  }  ;
  {  x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() )  }  c= F2() -polytopes F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() )  }  or x in F2() -polytopes F1() )
assume  x in  {  x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() )  }  ; ::_thesis: x in F2() -polytopes F1()
then  ex y being Element of F2() -polytopes F1() st
( x = y & P1[y] & y in F2() -polytopes F1() ) ;
hence  x in F2() -polytopes F1() ; ::_thesis: verum
end;
then reconsider c =  {  x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() )  }  as Subset of (F2() -polytopes F1()) ;
take  c ; ::_thesis: for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
 for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
proof
let x be Element of F2() -polytopes F1(); ::_thesis: ( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
thus  ( x in c implies ( P1[x] & x in F2() -polytopes F1() ) ) ::_thesis: ( P1[x] & x in F2() -polytopes F1() implies x in c )
proof
assume  x in c ; ::_thesis: ( P1[x] & x in F2() -polytopes F1() )
then  ex y being Element of F2() -polytopes F1() st
( y = x & P1[y] & y in F2() -polytopes F1() ) ;
hence  ( P1[x] & x in F2() -polytopes F1() ) ; ::_thesis: verum
end;
thus  ( P1[x] & x in F2() -polytopes F1() implies x in c ) ; ::_thesis: verum
end;
hence  for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) ) ; ::_thesis: verum
end;

definition
let p be polyhedron;
let k be Integer;
let v be Element of (k -chain-space p);
func Boundary v ->  Element of ((k - 1) -chain-space p) means :Def17: :: POLYFORM:def 17
( ( (k - 1) -polytopes p is empty implies it = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is 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
 ex b1 being Element of ((k - 1) -chain-space p) st
( ( (k - 1) -polytopes p is empty implies b1 = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b1 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) )
proof
defpred S1[ 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
A1: for x being Element of (k - 1) -polytopes p holds
( x in c iff ( S1[x] & x in (k - 1) -polytopes p ) ) from POLYFORM:sch_1();
reconsider c = c as Element of ((k - 1) -chain-space p) ;
take  c ; ::_thesis: ( ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) )
thus  ( ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of ((k - 1) -chain-space p) st ( (k - 1) -polytopes p is empty implies b1 = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b1 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) & ( (k - 1) -polytopes p is empty implies b2 = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b2 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) holds
b1 = b2
proof
let c, d be Element of ((k - 1) -chain-space p); ::_thesis: ( ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) & ( (k - 1) -polytopes p is empty implies d = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in d iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) implies c = d )
assume that
A2: ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) and
A3: ( not (k - 1) -polytopes p is 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
A4: ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in d iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ; ::_thesis: c = d
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
suppose (k - 1) -polytopes p is empty ; ::_thesis: c = d
hence  c = d by A2; ::_thesis: verum
end;
supposeA5: not (k - 1) -polytopes p is empty ; ::_thesis: c = d
 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; ::_thesis: ( x in c iff x in d )
thus  ( x in c implies x in d ) ::_thesis: ( x in d implies x in c )
proof
assume  x in c ; ::_thesis: x in d
then  Sum (incidence-sequence (x,v)) = 1. Z_2 by A3;
hence  x in d by A4, A5; ::_thesis: verum
end;
thus  ( x in d implies x in c ) ::_thesis: verum
proof
assume  x in d ; ::_thesis: x in c
then  Sum (incidence-sequence (x,v)) = 1. Z_2 by A4;
hence  x in c by A3, A5; ::_thesis: verum
end;
end;
hence  c = d by Th44; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def17 defines Boundary POLYFORM:def_17_:_
 for p being polyhedron
for k being Integer
for v being Element of (k -chain-space p)
for b4 being Element of ((k - 1) -chain-space p) holds
( b4 = Boundary v iff ( ( (k - 1) -polytopes p is empty implies b4 = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b4 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ) );

theorem Th45: :: POLYFORM:45
for p being polyhedron
for k being Integer
for c being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
proof
let p be polyhedron; ::_thesis: for k being Integer
for c being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
let k be Integer; ::_thesis: for c being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
let c be Element of (k -chain-space p); ::_thesis: for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
let x be Element of (k - 1) -polytopes p; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
set b = Boundary c;
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
set iscx = incidence-sequence (x,c);
 incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then A2: Sum (incidence-sequence (x,c)) = 0. Z_2 by RLVECT_1:43;
 Boundary c = 0. ((k - 1) -chain-space p) by A1;
hence  (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A2, BSPACE:14; ::_thesis: verum
end;
supposeA3: not (k - 1) -polytopes p is empty ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
then A4: ( x in Boundary c iff Sum (incidence-sequence (x,c)) = 1. Z_2 ) by Def17;
percases ( x in Boundary c or not x in Boundary c ) ;
suppose x in Boundary c ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
hence  (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A4, BSPACE:def_3; ::_thesis: verum
end;
supposeA5: not x in Boundary c ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
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  (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A5, BSPACE:def_3; ::_thesis: verum
end;
end;
end;
end;
end;

definition
let p be polyhedron;
let k be Integer;
funck -boundary p ->  Function of (k -chain-space p),((k - 1) -chain-space p) means :Def18: :: POLYFORM:def 18
 for c being Element of (k -chain-space p) holds it . c = Boundary c;
existence
 ex b1 being Function of (k -chain-space p),((k - 1) -chain-space p) st
for c being Element of (k -chain-space p) holds b1 . c = Boundary c
proof
defpred S1[ 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 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in k -chains p implies ex y being set st
( y in (k - 1) -chains p & S1[x,y] ) )
assume  x in k -chains p ; ::_thesis: ex y being set st
( y in (k - 1) -chains p & S1[x,y] )
then reconsider x = x as Element of (k -chain-space p) ;
set b = Boundary x;
take  Boundary x ; ::_thesis: ( Boundary x in (k - 1) -chains p & S1[x, Boundary x] )
thus  ( Boundary x in (k - 1) -chains p & S1[x, Boundary x] ) ; ::_thesis: verum
end;
consider f being Function of (k -chains p),((k - 1) -chains p) such that
A2: for x being set st x in k -chains p holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
reconsider f = f as Function of (k -chain-space p),((k - 1) -chain-space p) ;
take  f ; ::_thesis: for c being Element of (k -chain-space p) holds f . c = Boundary c
 for c being Element of (k -chain-space p) holds f . c = Boundary c
proof
let c be Element of (k -chain-space p); ::_thesis: f . c = Boundary c
 S1[c,f . c] by A2;
hence  f . c = Boundary c ; ::_thesis: verum
end;
hence  for c being Element of (k -chain-space p) holds f . c = Boundary c ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (k -chain-space p),((k - 1) -chain-space p) st ( for c being Element of (k -chain-space p) holds b1 . c = Boundary c ) & ( for c being Element of (k -chain-space p) holds b2 . c = Boundary c ) holds
b1 = b2
proof
let f, g be Function of (k -chain-space p),((k - 1) -chain-space p); ::_thesis: ( ( for c being Element of (k -chain-space p) holds f . c = Boundary c ) & ( for c being Element of (k -chain-space p) holds g . c = Boundary c ) implies f = g )
assume that
A3: for c being Element of (k -chain-space p) holds f . c = Boundary c and
A4: for c being Element of (k -chain-space p) holds g . c = Boundary c ; ::_thesis: f = g
A5: for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume  x in dom f ; ::_thesis: f . x = g . x
then reconsider x = x as Element of (k -chain-space p) ;
 f . x = Boundary x by A3;
hence  f . x = g . x by A4; ::_thesis: verum
end;
 dom f = [#] (k -chain-space p) by FUNCT_2:def_1;
then  dom f = dom g by FUNCT_2:def_1;
hence  f = g by A5, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def18 defines -boundary POLYFORM:def_18_:_
 for p being polyhedron
for k being Integer
for b3 being Function of (k -chain-space p),((k - 1) -chain-space p) holds
( b3 = k -boundary p iff for c being Element of (k -chain-space p) holds b3 . c = Boundary c );

theorem Th46: :: POLYFORM:46
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
proof
let p be polyhedron; ::_thesis: for k being Integer
for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
let k be Integer; ::_thesis: for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
let c, d be Element of (k -chain-space p); ::_thesis: Boundary (c + d) = (Boundary c) + (Boundary d)
set bc = Boundary c;
set bd = Boundary d;
set s = c + d;
set l = Boundary (c + d);
set r = (Boundary c) + (Boundary d);
 for x being Element of (k - 1) -polytopes p holds (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x
proof
let x be Element of (k - 1) -polytopes p; ::_thesis: (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x
set a = (Boundary c) @ x;
set b = (Boundary d) @ x;
A1: ( (Boundary c) @ x = Sum (incidence-sequence (x,c)) & (Boundary d) @ x = Sum (incidence-sequence (x,d)) ) by Th45;
 ( (Boundary (c + d)) @ x = Sum (incidence-sequence (x,(c + d))) & ((Boundary c) + (Boundary d)) @ x = ((Boundary c) @ x) + ((Boundary d) @ x) ) by Th37, Th45;
hence  (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x by A1, Th40; ::_thesis: verum
end;
hence  Boundary (c + d) = (Boundary c) + (Boundary d) by Th43; ::_thesis: verum
end;

theorem Th47: :: POLYFORM:47
for p being polyhedron
for k being Integer
for a being Element of Z_2
for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
proof
let p be polyhedron; ::_thesis: for k being Integer
for a being Element of Z_2
for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let k be Integer; ::_thesis: for a being Element of Z_2
for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let a be Element of Z_2; ::_thesis: for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let c be Element of (k -chain-space p); ::_thesis: Boundary (a * c) = a * (Boundary c)
set lsm = a * c;
set l = Boundary (a * c);
set rb = Boundary c;
set r = a * (Boundary c);
 for x being Element of (k - 1) -polytopes p holds (Boundary (a * c)) @ x = (a * (Boundary c)) @ x
proof
let x be Element of (k - 1) -polytopes p; ::_thesis: (Boundary (a * c)) @ x = (a * (Boundary c)) @ x
set b = (Boundary c) @ x;
A1: ( (Boundary (a * c)) @ x = Sum (incidence-sequence (x,(a * c))) & (Boundary c) @ x = Sum (incidence-sequence (x,c)) ) by Th45;
 ( (a * (Boundary c)) @ x = a * ((Boundary c) @ x) & incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c)) ) by Th41, Th42;
hence  (Boundary (a * c)) @ x = (a * (Boundary c)) @ x by A1, FVSUM_1:73; ::_thesis: verum
end;
hence  Boundary (a * c) = a * (Boundary c) by Th43; ::_thesis: verum
end;

theorem Th48: :: POLYFORM:48
for p being polyhedron
for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
proof
let p be polyhedron; ::_thesis: for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
let k be Integer; ::_thesis: k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
set V = k -chain-space p;
set b = k -boundary p;
A1: for a being Element of Z_2
for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
proof
let a be Element of Z_2; ::_thesis: for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
let x be Element of (k -chain-space p); ::_thesis: (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
(k -boundary p) . (a * x) = Boundary (a * x) by Def18
.= a * (Boundary x) by Th47
.= a * ((k -boundary p) . x) by Def18 ;
hence  (k -boundary p) . (a * x) = a * ((k -boundary p) . x) ; ::_thesis: verum
end;
 for x, y being Element of (k -chain-space p) holds (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)
proof
let x, y be Element of (k -chain-space p); ::_thesis: (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)
(k -boundary p) . (x + y) = Boundary (x + y) by Def18
.= (Boundary x) + (Boundary y) by Th46
.= ((k -boundary p) . x) + (Boundary y) by Def18
.= ((k -boundary p) . x) + ((k -boundary p) . y) by Def18 ;
hence  (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y) ; ::_thesis: verum
end;
then  ( k -boundary p is additive & k -boundary p is homogeneous ) by A1, VECTSP_1:def_20, MOD_2:def_2;
hence  k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p) ; ::_thesis: verum
end;

registration
let p be polyhedron;
let k be Integer;
clusterk -boundary p ->  additive homogeneous ;
coherence
 ( k -boundary p is homogeneous & k -boundary p is additive ) by Th48;
end;

definition
let p be polyhedron;
let k be Integer;
funck -circuit-space p ->  Subspace of k -chain-space p equals :: POLYFORM:def 19
 ker (k -boundary p);
coherence
 ker (k -boundary p) is Subspace of k -chain-space p ;
end;

:: deftheorem  defines -circuit-space POLYFORM:def_19_:_
 for p being polyhedron
for k being Integer holds k -circuit-space p = ker (k -boundary p);

definition
let p be polyhedron;
let k be Integer;
funck -circuits p ->  non empty Subset of (k -chains p) equals :: POLYFORM:def 20
 [#] (k -circuit-space p);
coherence
 [#] (k -circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def_2;
end;

:: deftheorem  defines -circuits POLYFORM:def_20_:_
 for p being polyhedron
for k being Integer holds k -circuits p = [#] (k -circuit-space p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-chain-space p ->  Subspace of k -chain-space p equals :: POLYFORM:def 21
 im ((k + 1) -boundary p);
coherence
 im ((k + 1) -boundary p) is Subspace of k -chain-space p ;
end;

:: deftheorem  defines -bounding-chain-space POLYFORM:def_21_:_
 for p being polyhedron
for k being Integer holds k -bounding-chain-space p = im ((k + 1) -boundary p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-chains p ->  non empty Subset of (k -chains p) equals :: POLYFORM:def 22
 [#] (k -bounding-chain-space p);
coherence
 [#] (k -bounding-chain-space p) is non empty Subset of (k -chains p) by VECTSP_4:def_2;
end;

:: deftheorem  defines -bounding-chains POLYFORM:def_22_:_
 for p being polyhedron
for k being Integer holds k -bounding-chains p = [#] (k -bounding-chain-space p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-circuit-space p ->  Subspace of k -chain-space p equals :: POLYFORM:def 23
(k -bounding-chain-space p) /\ (k -circuit-space p);
coherence
 (k -bounding-chain-space p) /\ (k -circuit-space p) is Subspace of k -chain-space p ;
end;

:: deftheorem  defines -bounding-circuit-space POLYFORM:def_23_:_
 for p being polyhedron
for k being Integer holds k -bounding-circuit-space p = (k -bounding-chain-space p) /\ (k -circuit-space p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-circuits p ->  non empty Subset of (k -chains p) equals :: POLYFORM:def 24
 [#] (k -bounding-circuit-space p);
coherence
 [#] (k -bounding-circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def_2;
end;

:: deftheorem  defines -bounding-circuits POLYFORM:def_24_:_
 for p being polyhedron
for k being Integer holds k -bounding-circuits p = [#] (k -bounding-circuit-space p);

theorem :: POLYFORM:49
for p being polyhedron
for k being Integer holds dim (k -chain-space p) = (rank (k -boundary p)) + (nullity (k -boundary p)) by RANKNULL:44;

begin

definition
let p be polyhedron;
attrp is simply-connected  means :Def25: :: POLYFORM:def 25
 for k being Integer holds k -circuits p = k -bounding-chains p;
end;

:: deftheorem Def25 defines simply-connected POLYFORM:def_25_:_
 for p being polyhedron holds
( p is simply-connected iff for k being Integer holds k -circuits p = k -bounding-chains p );

theorem Th50: :: POLYFORM:50
for p being polyhedron holds
( p is simply-connected iff for n being Integer holds n -circuit-space p = n -bounding-chain-space p )
proof
let p be polyhedron; ::_thesis: ( p is simply-connected iff for n being Integer holds n -circuit-space p = n -bounding-chain-space p )
defpred S1[ polyhedron] means  for n being Integer holds n -circuit-space $1 = n -bounding-chain-space $1;
thus  ( p is simply-connected implies S1[p] ) ::_thesis: ( ( for n being Integer holds n -circuit-space p = n -bounding-chain-space p ) implies p is simply-connected )
proof
assume A1: p is simply-connected ; ::_thesis: S1[p]
let n be Integer; ::_thesis: n -circuit-space p = n -bounding-chain-space p
 n -circuits p = n -bounding-chains p by A1, Def25;
hence  n -circuit-space p = n -bounding-chain-space p by VECTSP_4:29; ::_thesis: verum
end;
thus  ( S1[p] implies p is simply-connected ) ::_thesis: verum
proof
assume A2: S1[p] ; ::_thesis: p is simply-connected
let n be Integer; :: according to POLYFORM:def_25 ::_thesis: n -circuits p = n -bounding-chains p
thus  n -circuits p = n -bounding-chains p by A2; ::_thesis: verum
end;
end;

definition
let p be polyhedron;
func alternating-f-vector p ->  FinSequence of INT  means :Def26: :: POLYFORM:def 26
( 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
 ex b1 being FinSequence of INT st
( len b1 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b1 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )
proof
deffunc H1( Nat) ->  Element of INT = ((- 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 = H1(j) from FINSEQ_2:sch_1();
take  s ; ::_thesis: ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )
A3: dom s = Seg ((dim p) + 2) by A1, FINSEQ_1:def_3;
 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; ::_thesis: ( 1 <= j & j <= (dim p) + 2 implies s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2))) )
assume  ( 1 <= j & j <= (dim p) + 2 ) ; ::_thesis: s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2)))
then  j in Seg ((dim p) + 2) by FINSEQ_1:1;
hence  s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2))) by A2, A3; ::_thesis: verum
end;
hence  ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of INT st len b1 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b1 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) & len b2 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b2 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) holds
b1 = b2
proof
let s, t be FinSequence of INT ; ::_thesis: ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) & len t = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
t . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) implies s = t )
assume that
A4: len s = (dim p) + 2 and
A5: for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) and
A6: len t = (dim p) + 2 and
A7: for k being Nat st 1 <= k & k <= (dim p) + 2 holds
t . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ; ::_thesis: s = t
 for k being Nat st 1 <= k & k <= len s holds
s . k = t . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = t . k )
assume A8: ( 1 <= k & k <= len s ) ; ::_thesis: s . k = t . k
reconsider k = k as Nat ;
 s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) by A4, A5, A8;
hence  s . k = t . k by A4, A7, A8; ::_thesis: verum
end;
hence  s = t by A4, A6, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def26 defines alternating-f-vector POLYFORM:def_26_:_
 for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-f-vector p iff ( len b2 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b2 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) ) );

definition
let p be polyhedron;
func alternating-proper-f-vector p ->  FinSequence of INT  means :Def27: :: POLYFORM:def 27
( 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
 ex b1 being FinSequence of INT st
( len b1 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
proof
deffunc H1( Nat) ->  Element of INT = ((- 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 = H1(j) from FINSEQ_2:sch_1();
take  s ; ::_thesis: ( len s = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
A3: dom s = Seg (dim p) by A1, FINSEQ_1:def_3;
 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; ::_thesis: ( 1 <= j & j <= dim p implies s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) )
assume  ( 1 <= j & j <= dim p ) ; ::_thesis: s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1)))
then  j in Seg (dim p) by FINSEQ_1:1;
hence  s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) by A2, A3; ::_thesis: verum
end;
hence  ( len s = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of INT st len b1 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b2 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b1 = b2
proof
let s, t be FinSequence of INT ; ::_thesis: ( len s = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len t = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) implies s = t )
assume that
A4: len s = dim p and
A5: for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) and
A6: len t = dim p and
A7: for k being Nat st 1 <= k & k <= dim p holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ; ::_thesis: s = t
 for k being Nat st 1 <= k & k <= len s holds
s . k = t . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = t . k )
assume A8: ( 1 <= k & k <= len s ) ; ::_thesis: s . k = t . k
reconsider k = k as Nat ;
 s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) by A4, A5, A8;
hence  s . k = t . k by A4, A7, A8; ::_thesis: verum
end;
hence  s = t by A4, A6, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def27 defines alternating-proper-f-vector POLYFORM:def_27_:_
 for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-proper-f-vector p iff ( len b2 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) );

definition
let p be polyhedron;
func alternating-semi-proper-f-vector p ->  FinSequence of INT  means :Def28: :: POLYFORM:def 28
( 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
 ex b1 being FinSequence of INT st
( len b1 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
proof
deffunc H1( Nat) ->  Element of INT = ((- 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 = H1(j) from FINSEQ_2:sch_1();
take  s ; ::_thesis: ( len s = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
A3: dom s = Seg ((dim p) + 1) by A1, FINSEQ_1:def_3;
 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; ::_thesis: ( 1 <= j & j <= (dim p) + 1 implies s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) )
assume  ( 1 <= j & j <= (dim p) + 1 ) ; ::_thesis: s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1)))
then  j in Seg ((dim p) + 1) by FINSEQ_1:1;
hence  s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) by A2, A3; ::_thesis: verum
end;
hence  ( len s = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of INT st len b1 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b2 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b1 = b2
proof
let s, t be FinSequence of INT ; ::_thesis: ( len s = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len t = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) implies s = t )
assume that
A4: len s = (dim p) + 1 and
A5: for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) and
A6: len t = (dim p) + 1 and
A7: for k being Nat st 1 <= k & k <= (dim p) + 1 holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ; ::_thesis: s = t
 for k being Nat st 1 <= k & k <= len s holds
s . k = t . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = t . k )
assume A8: ( 1 <= k & k <= len s ) ; ::_thesis: s . k = t . k
reconsider k = k as Nat ;
 s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) by A4, A5, A8;
hence  s . k = t . k by A4, A7, A8; ::_thesis: verum
end;
hence  s = t by A4, A6, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def28 defines alternating-semi-proper-f-vector POLYFORM:def_28_:_
 for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-semi-proper-f-vector p iff ( len b2 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) );

theorem Th51: :: POLYFORM:51
for p being polyhedron
for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds
(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
let p be polyhedron; ::_thesis: for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds
(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)))
let n be Nat; ::_thesis: ( 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))) )
set apcs = alternating-proper-f-vector p;
assume A1: 1 <= n ; ::_thesis: ( not n <= len (alternating-proper-f-vector p) or (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))) )
set a = (- 1) |^ (n + 1);
assume  n <= len (alternating-proper-f-vector p) ; ::_thesis: (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)))
then  n <= dim p by Def27;
then (alternating-proper-f-vector p) . n = ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A1, Def27
.= ((- 1) |^ (n + 1)) * (dim ((n - 1) -chain-space p)) by Th36
.= ((- 1) |^ (n + 1)) * ((rank ((n - 1) -boundary p)) + (nullity ((n - 1) -boundary p))) by RANKNULL:44
.= (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p))) ;
hence  (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))) ; ::_thesis: verum
end;

definition
let p be polyhedron;
attrp is eulerian  means :Def29: :: POLYFORM:def 29
 Sum (alternating-proper-f-vector p) = 1 + ((- 1) |^ ((dim p) + 1));
end;

:: deftheorem Def29 defines eulerian POLYFORM:def_29_:_
 for p being polyhedron holds
( p is eulerian iff Sum (alternating-proper-f-vector p) = 1 + ((- 1) |^ ((dim p) + 1)) );

theorem Th52: :: POLYFORM:52
for p being polyhedron holds alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>
proof
let p be polyhedron; ::_thesis: alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>
set d = dim p;
set aspcs = alternating-semi-proper-f-vector p;
set apcs = alternating-proper-f-vector p;
set r = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>;
A1: len (alternating-semi-proper-f-vector p) = (dim p) + 1 by Def28;
A2: for n being Nat st 1 <= n & n <= len (alternating-semi-proper-f-vector p) holds
(alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len (alternating-semi-proper-f-vector p) implies (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n )
assume that
A3: 1 <= n and
A4: n <= len (alternating-semi-proper-f-vector p) ; ::_thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
percases ( n <= dim p or n = (dim p) + 1 ) by A1, A4, NAT_1:8;
supposeA5: n <= dim p ; ::_thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
A6: n in NAT by ORDINAL1:def_12;
 ( len (alternating-proper-f-vector p) = dim p & dom (alternating-proper-f-vector p) = Seg (len (alternating-proper-f-vector p)) ) by Def27, FINSEQ_1:def_3;
then  n in dom (alternating-proper-f-vector p) by A3, A5, A6;
then ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n = (alternating-proper-f-vector p) . n by FINSEQ_1:def_7
.= ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A3, A5, Def27 ;
hence  (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n by A1, A3, A4, Def28; ::_thesis: verum
end;
supposeA7: n = (dim p) + 1 ; ::_thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
then  n = (len (alternating-proper-f-vector p)) + 1 by Def27;
then A8: ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n = (- 1) |^ (dim p) by FINSEQ_1:42
.= (- 1) |^ ((dim p) + 2) by Th14 ;
(alternating-semi-proper-f-vector p) . n = ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A3, A7, Def28
.= ((- 1) |^ (n + 1)) * 1 by A7, Th31
.= (- 1) |^ (n + 1) ;
hence  (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n by A7, A8; ::_thesis: verum
end;
end;
end;
len ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) = (len (alternating-proper-f-vector p)) + (len <*((- 1) |^ (dim p))*>) by FINSEQ_1:22
.= (dim p) + (len <*((- 1) |^ (dim p))*>) by Def27
.= (dim p) + 1 by FINSEQ_1:40 ;
then  len (alternating-semi-proper-f-vector p) = len ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) by Def28;
hence  alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*> by A2, FINSEQ_1:14; ::_thesis: verum
end;

definition
let p be polyhedron;
redefine attr p is eulerian  means :Def30: :: POLYFORM:def 30
 Sum (alternating-semi-proper-f-vector p) = 1;
compatibility
 ( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 )
proof
set aspcs = alternating-semi-proper-f-vector p;
set apcs = alternating-proper-f-vector p;
 alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*> by Th52;
then A1: Sum (alternating-semi-proper-f-vector p) = (Sum (alternating-proper-f-vector p)) + ((- 1) |^ (dim p)) by RVSUM_1:74;
A2: ( Sum (alternating-semi-proper-f-vector p) = 1 implies p is eulerian )
proof
assume  Sum (alternating-semi-proper-f-vector p) = 1 ; ::_thesis: p is eulerian
then  Sum (alternating-proper-f-vector p) = 1 + ((- 1) * ((- 1) |^ (dim p))) by A1
.= 1 + ((- 1) |^ ((dim p) + 1)) by NEWTON:6 ;
hence  p is eulerian by Def29; ::_thesis: verum
end;
 ( p is eulerian implies Sum (alternating-semi-proper-f-vector p) = 1 )
proof
assume  p is eulerian ; ::_thesis: Sum (alternating-semi-proper-f-vector p) = 1
then  Sum (alternating-semi-proper-f-vector p) = (1 + ((- 1) |^ ((dim p) + 1))) + ((- 1) |^ (dim p)) by A1, Def29
.= (1 + ((- 1) * ((- 1) |^ (dim p)))) + ((- 1) |^ (dim p)) by NEWTON:6
.= 1 ;
hence  Sum (alternating-semi-proper-f-vector p) = 1 ; ::_thesis: verum
end;
hence  ( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 ) by A2; ::_thesis: verum
end;
end;

:: deftheorem Def30 defines eulerian POLYFORM:def_30_:_
 for p being polyhedron holds
( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 );

theorem Th53: :: POLYFORM:53
for p being polyhedron holds alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p)
proof
let p be polyhedron; ::_thesis: alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p)
set acs = alternating-f-vector p;
set aspcs = alternating-semi-proper-f-vector p;
set d = dim p;
set r = <*(- 1)*> ^ (alternating-semi-proper-f-vector p);
A1: len (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) = (len <*(- 1)*>) + (len (alternating-semi-proper-f-vector p)) by FINSEQ_1:22
.= (len <*(- 1)*>) + ((dim p) + 1) by Def28
.= 1 + ((dim p) + 1) by FINSEQ_1:40
.= (dim p) + 2 ;
A2: for n being Nat st 1 <= n & n <= len (alternating-f-vector p) holds
(alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len (alternating-f-vector p) implies (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n )
assume that
A3: 1 <= n and
A4: n <= len (alternating-f-vector p) ; ::_thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
A5: n <= (dim p) + 2 by A4, Def26;
percases ( n = 1 or n > 1 ) by A3, XXREAL_0:1;
supposeA6: n = 1 ; ::_thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
then (alternating-f-vector p) . n = ((- 1) |^ 1) * (num-polytopes (p,(1 - 2))) by A5, Def26
.= (- 1) * (num-polytopes (p,(- 1))) by NEWTON:5
.= (- 1) * 1 by Th30
.= - 1 ;
hence  (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n by A6, FINSEQ_1:41; ::_thesis: verum
end;
supposeA7: n > 1 ; ::_thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
then A8: 1 - 1 < n - 1 by XREAL_1:9;
then reconsider m = n - 1 as Element of NAT by INT_1:3;
 n - 1 <= ((dim p) + 2) - 1 by A5, XREAL_1:9;
then A9: m <= (dim p) + 1 ;
 len <*(- 1)*> = 1 by FINSEQ_1:39;
then A10: (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n = (alternating-semi-proper-f-vector p) . (n - 1) by A1, A5, A7, FINSEQ_1:24;
 0 < 0 + m by A8;
then  1 <= m by NAT_1:19;
then (alternating-semi-proper-f-vector p) . m = ((- 1) |^ (m + 1)) * (num-polytopes (p,(m - 1))) by A9, Def28
.= ((- 1) |^ n) * (num-polytopes (p,(n - 2))) ;
hence  (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n by A3, A5, A10, Def26; ::_thesis: verum
end;
end;
end;
 len (alternating-f-vector p) = len (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) by A1, Def26;
hence  alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p) by A2, FINSEQ_1:14; ::_thesis: verum
end;

definition
let p be polyhedron;
redefine attr p is eulerian  means :Def31: :: POLYFORM:def 31
 Sum (alternating-f-vector p) = 0 ;
compatibility
 ( p is eulerian iff Sum (alternating-f-vector p) = 0 )
proof
set aspcs = alternating-semi-proper-f-vector p;
set acs = alternating-f-vector p;
 alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p) by Th53;
then A1: Sum (alternating-f-vector p) = (- 1) + (Sum (alternating-semi-proper-f-vector p)) by Th20;
 ( p is eulerian implies Sum (alternating-f-vector p) = 0 )
proof
assume  p is eulerian ; ::_thesis: Sum (alternating-f-vector p) = 0
then  Sum (alternating-f-vector p) = (- 1) + 1 by A1, Def30
.= 0 ;
hence  Sum (alternating-f-vector p) = 0 ; ::_thesis: verum
end;
hence  ( p is eulerian iff Sum (alternating-f-vector p) = 0 ) by A1, Def30; ::_thesis: verum
end;
end;

:: deftheorem Def31 defines eulerian POLYFORM:def_31_:_
 for p being polyhedron holds
( p is eulerian iff Sum (alternating-f-vector p) = 0 );

begin

theorem Th54: :: POLYFORM:54
for p being polyhedron holds not 0 -polytopes p is empty
proof
let p be polyhedron; ::_thesis: not 0 -polytopes p is empty
set d = dim p;
percases ( dim p = 0 or dim p > 0 ) ;
suppose dim p = 0 ; ::_thesis: not 0 -polytopes p is empty
then  0 -polytopes p = {p} by Def5;
hence  not 0 -polytopes p is empty ; ::_thesis: verum
end;
suppose dim p > 0 ; ::_thesis: not 0 -polytopes p is empty
hence  not 0 -polytopes p is empty by Th25; ::_thesis: verum
end;
end;
end;

theorem Th55: :: POLYFORM:55
for p being polyhedron holds card ([#] ((- 1) -chain-space p)) = 2
proof
let p be polyhedron; ::_thesis: card ([#] ((- 1) -chain-space p)) = 2
 (- 1) -polytopes p = {{}} by Def5;
then  card ((- 1) -polytopes p) = 1 by CARD_1:30;
then  card ([#] ((- 1) -chain-space p)) = exp (2,1) by BSPACE:42
.= 2 by CARD_2:27 ;
hence  card ([#] ((- 1) -chain-space p)) = 2 ; ::_thesis: verum
end;

theorem Th56: :: POLYFORM:56
for p being polyhedron holds [#] ((- 1) -chain-space p) = {{},{{}}}
proof
let p be polyhedron; ::_thesis: [#] ((- 1) -chain-space p) = {{},{{}}}
 (- 1) -polytopes p = {{}} by Def5;
hence  [#] ((- 1) -chain-space p) = {{},{{}}} by ZFMISC_1:24; ::_thesis: verum
end;

theorem Th57: :: POLYFORM:57
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
proof
let p be polyhedron; ::_thesis: for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
let k be Integer; ::_thesis: for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
let x be Element of k -polytopes p; ::_thesis: for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
let e be Element of (k - 1) -polytopes p; ::_thesis: ( k = 0 & e = {} implies incidence-value (e,x) = 1. Z_2 )
assume that
A1: k = 0 and
A2: e = {} ; ::_thesis: incidence-value (e,x) = 1. Z_2
A3: eta (p,k) = [:{{}},(0 -polytopes p):] --> (1. Z_2) by A1, Def6;
A4: k <= dim p by A1;
then  ( {} in {{}} & not 0 -polytopes p is empty ) by Th25, TARSKI:def_1;
then A5: [{},x] in [:{{}},(0 -polytopes p):] by A1, ZFMISC_1:87;
incidence-value (e,x) = (eta (p,k)) . (e,x) by A1, A4, Def13
.= 1. Z_2 by A2, A3, A5, FUNCOP_1:7 ;
hence  incidence-value (e,x) = 1. Z_2 ; ::_thesis: verum
end;

theorem Th58: :: POLYFORM:58
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p
for 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 p be polyhedron; ::_thesis: for k being Integer
for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p
for 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
let k be Integer; ::_thesis: for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p
for 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
let x be Element of k -polytopes p; ::_thesis: for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p
for 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
let v be Element of (k -chain-space p); ::_thesis: for e being Element of (k - 1) -polytopes p
for 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
let e be Element of (k - 1) -polytopes p; ::_thesis: for 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
let n be Nat; ::_thesis: ( k = 0 & v = {x} & e = {} & x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) implies (incidence-sequence (e,v)) . n = 1. Z_2 )
assume that
A1: k = 0 and
A2: v = {x} and
A3: e = {} and
A4: ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) ) ; ::_thesis: (incidence-sequence (e,v)) . n = 1. Z_2
set iseq = incidence-sequence (e,v);
A5: x in v by A2, TARSKI:def_1;
 not (k - 1) -polytopes p is empty by A1, Def5;
then (incidence-sequence (e,v)) . n = (v @ x) * (incidence-value (e,x)) by A4, Def16
.= (1. Z_2) * (incidence-value (e,x)) by A5, BSPACE:def_3
.= (1. Z_2) * (1. Z_2) by A1, A3, Th57
.= 1. Z_2 by VECTSP_1:def_6 ;
hence  (incidence-sequence (e,v)) . n = 1. Z_2 ; ::_thesis: verum
end;

theorem Th59: :: POLYFORM:59
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for 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 p be polyhedron; ::_thesis: for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for 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
let k be Integer; ::_thesis: for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for 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
let x be Element of k -polytopes p; ::_thesis: for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for 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
let e be Element of (k - 1) -polytopes p; ::_thesis: for v being Element of (k -chain-space p)
for 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
let v be Element of (k -chain-space p); ::_thesis: for 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
let m, n be Nat; ::_thesis: ( 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 implies (incidence-sequence (e,v)) . m = 0. Z_2 )
assume that
A1: k = 0 and
A2: v = {x} and
A3: x = n -th-polytope (p,k) and
A4: ( 1 <= m & m <= num-polytopes (p,k) ) and
A5: ( 1 <= n & n <= num-polytopes (p,k) & m <> n ) ; ::_thesis: (incidence-sequence (e,v)) . m = 0. Z_2
A6: m -th-polytope (p,k) <> x by A3, A4, A5, Th34;
now__::_thesis:_not_v_@_(m_-th-polytope_(p,k))_=_1._Z_2
assume  v @ (m -th-polytope (p,k)) = 1. Z_2 ; ::_thesis: contradiction
then  m -th-polytope (p,k) in {x} by A2, BSPACE:9;
hence  contradiction by A6, TARSKI:def_1; ::_thesis: verum
end;
then A7: v @ (m -th-polytope (p,k)) = 0. Z_2 by BSPACE:11;
set iseq = incidence-sequence (e,v);
 not (k - 1) -polytopes p is empty by A1, Def5;
then (incidence-sequence (e,v)) . m = (0. Z_2) * (incidence-value (e,(m -th-polytope (p,k)))) by A4, A7, Def16
.= 0. Z_2 by VECTSP_1:7 ;
hence  (incidence-sequence (e,v)) . m = 0. Z_2 ; ::_thesis: verum
end;

theorem Th60: :: POLYFORM:60
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for 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 p be polyhedron; ::_thesis: for k being Integer
for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p st k = 0 & v = {x} & e = {} holds
Sum (incidence-sequence (e,v)) = 1. Z_2
let k be Integer; ::_thesis: for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p st k = 0 & v = {x} & e = {} holds
Sum (incidence-sequence (e,v)) = 1. Z_2
let x be Element of k -polytopes p; ::_thesis: for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p st k = 0 & v = {x} & e = {} holds
Sum (incidence-sequence (e,v)) = 1. Z_2
let v be Element of (k -chain-space p); ::_thesis: for e being Element of (k - 1) -polytopes p st k = 0 & v = {x} & e = {} holds
Sum (incidence-sequence (e,v)) = 1. Z_2
let e be Element of (k - 1) -polytopes p; ::_thesis: ( k = 0 & v = {x} & e = {} implies Sum (incidence-sequence (e,v)) = 1. Z_2 )
assume that
A1: k = 0 and
A2: v = {x} and
A3: e = {} ; ::_thesis: Sum (incidence-sequence (e,v)) = 1. Z_2
set iseq = incidence-sequence (e,v);
 k <= dim p by A1;
then consider n being Nat such that
A4: x = n -th-polytope (p,k) and
A5: ( 1 <= n & n <= num-polytopes (p,k) ) by A1, Th32;
 not (k - 1) -polytopes p is empty by A1, Def5;
then A6: len (incidence-sequence (e,v)) = num-polytopes (p,k) by Def16;
A7: for m being Nat st m in dom (incidence-sequence (e,v)) & m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
proof
let m be Nat; ::_thesis: ( m in dom (incidence-sequence (e,v)) & m <> n implies (incidence-sequence (e,v)) . m = 0. Z_2 )
assume that
A8: m in dom (incidence-sequence (e,v)) and
A9: m <> n ; ::_thesis: (incidence-sequence (e,v)) . m = 0. Z_2
 m in Seg (len (incidence-sequence (e,v))) by A8, FINSEQ_1:def_3;
then  ( 1 <= m & m <= len (incidence-sequence (e,v)) ) by FINSEQ_1:1;
hence  (incidence-sequence (e,v)) . m = 0. Z_2 by A1, A2, A4, A5, A6, A9, Th59; ::_thesis: verum
end;
 dom (incidence-sequence (e,v)) = Seg (len (incidence-sequence (e,v))) by FINSEQ_1:def_3;
then A10: n in dom (incidence-sequence (e,v)) by A5, A6, FINSEQ_1:1;
 (incidence-sequence (e,v)) . n = 1. Z_2 by A1, A2, A3, A4, A5, Th58;
hence  Sum (incidence-sequence (e,v)) = 1. Z_2 by A10, A7, MATRIX_3:12; ::_thesis: verum
end;

theorem Th61: :: POLYFORM:61
for p being polyhedron
for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{}}
proof
let p be polyhedron; ::_thesis: for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{}}
reconsider minusone = 0 - 1 as Integer ;
let x be Element of 0 -polytopes p; ::_thesis: (0 -boundary p) . {x} = {{}}
set T = 0 -boundary p;
 not 0 -polytopes p is empty by Th54;
then reconsider v = {x} as Subset of (0 -polytopes p) by ZFMISC_1:31;
 (0 - 1) -polytopes p = {{}} by Def5;
then reconsider null = {} as Element of (0 - 1) -polytopes p by TARSKI:def_1;
reconsider v = v as Element of (0 -chain-space p) ;
reconsider bv = Boundary v as Element of (minusone -chain-space p) ;
A1: bv c= {null}
proof
A2: [#] (minusone -chain-space p) = {{},{{}}} by Th56;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in bv or y in {null} )
assume A3: y in bv ; ::_thesis: y in {null}
percases ( bv = {} or bv = {{}} ) by A2, TARSKI:def_2;
suppose bv = {} ; ::_thesis: y in {null}
hence  y in {null} by A3; ::_thesis: verum
end;
suppose bv = {{}} ; ::_thesis: y in {null}
hence  y in {null} by A3; ::_thesis: verum
end;
end;
end;
 not minusone -polytopes p is empty by Def5;
then  ( null in bv iff Sum (incidence-sequence (null,v)) = 1. Z_2 ) by Def17;
then A4: {null} c= bv by Th60, ZFMISC_1:31;
 (0 -boundary p) . v = Boundary v by Def18;
hence  (0 -boundary p) . {x} = {{}} by A4, A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th62: :: POLYFORM:62
for p being polyhedron
for k being Integer st k = - 1 holds
dim (k -bounding-chain-space p) = 1
proof
let p be polyhedron; ::_thesis: for k being Integer st k = - 1 holds
dim (k -bounding-chain-space p) = 1
let k be Integer; ::_thesis: ( k = - 1 implies dim (k -bounding-chain-space p) = 1 )
set T = 0 -boundary p;
set V = k -bounding-chain-space p;
assume A1: k = - 1 ; ::_thesis: dim (k -bounding-chain-space p) = 1
 card ([#] (k -bounding-chain-space p)) = 2
proof
 [#] (k -bounding-chain-space p) c= [#] (k -chain-space p) by VECTSP_4:def_2;
then  card ([#] (k -bounding-chain-space p)) c= card ([#] (k -chain-space p)) by CARD_1:11;
then A2: card ([#] (k -bounding-chain-space p)) c= 2 by A1, Th55;
 0 -polytopes p <> {} by Th54;
then consider x being set  such that
A3: x in 0 -polytopes p by XBOOLE_0:def_1;
reconsider x = x as Element of 0 -polytopes p by A3;
set v = {x};
A4: (0 -boundary p) . {x} = {{}} by Th61;
reconsider v = {x} as Subset of (0 -polytopes p) by A3, ZFMISC_1:31;
reconsider v = v as Element of (0 -chain-space p) ;
A5: dom (0 -boundary p) = [#] (0 -chain-space p) by RANKNULL:7;
then  v in dom (0 -boundary p) ;
then A6: {{}} in rng (0 -boundary p) by A4, FUNCT_1:3;
(0 -boundary p) . (0. (0 -chain-space p)) = 0. (k -chain-space p) by A1, RANKNULL:9
.= {} ;
then  {} in rng (0 -boundary p) by A5, FUNCT_1:3;
then A7: {{},{{}}} c= rng (0 -boundary p) by A6, ZFMISC_1:32;
 card {{},{{}}} = 2 by CARD_2:57;
then A8: 2 c= card (rng (0 -boundary p)) by A7, CARD_1:11;
card (rng (0 -boundary p)) = card ((0 -boundary p) .: ([#] (0 -chain-space p))) by RELSET_1:22
.= card ([#] (k -bounding-chain-space p)) by A1, RANKNULL:def_2 ;
hence  card ([#] (k -bounding-chain-space p)) = 2 by A8, A2, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  dim (k -bounding-chain-space p) = 1 by RANKNULL:6; ::_thesis: verum
end;

theorem Th63: :: POLYFORM:63
for p being polyhedron holds card ([#] ((dim p) -chain-space p)) = 2
proof
let p be polyhedron; ::_thesis: card ([#] ((dim p) -chain-space p)) = 2
 (dim p) -polytopes p = {p} by Def5;
then  card ((dim p) -polytopes p) = 1 by CARD_1:30;
then  card ([#] ((dim p) -chain-space p)) = exp (2,1) by BSPACE:42
.= 2 by CARD_2:27 ;
hence  card ([#] ((dim p) -chain-space p)) = 2 ; ::_thesis: verum
end;

theorem Th64: :: POLYFORM:64
for p being polyhedron holds {p} is Element of ((dim p) -chain-space p)
proof
let p be polyhedron; ::_thesis: {p} is Element of ((dim p) -chain-space p)
 (dim p) -polytopes p = {p} by Def5;
hence  {p} is Element of ((dim p) -chain-space p) by ZFMISC_1:def_1; ::_thesis: verum
end;

theorem Th65: :: POLYFORM:65
for p being polyhedron holds {p} in [#] ((dim p) -chain-space p)
proof
let p be polyhedron; ::_thesis: {p} in [#] ((dim p) -chain-space p)
 {p} is Element of ((dim p) -chain-space p) by Th64;
hence  {p} in [#] ((dim p) -chain-space p) ; ::_thesis: verum
end;

theorem Th66: :: POLYFORM:66
for p being polyhedron holds not ((dim p) - 1) -polytopes p is empty
proof
let p be polyhedron; ::_thesis: not ((dim p) - 1) -polytopes p is empty
set n = (dim p) - 1;
 0 - 1 = - 1 ;
then A1: - 1 <= (dim p) - 1 by XREAL_1:9;
 (dim p) - 1 <= dim p by XREAL_1:146;
hence  not ((dim p) - 1) -polytopes p is empty by A1, Th25; ::_thesis: verum
end;

registration
let p be polyhedron;
cluster((dim p) - 1) -polytopes p ->  non empty finite ;
coherence
 not ((dim p) - 1) -polytopes p is empty by Th66;
end;

theorem Th67: :: POLYFORM:67
for p being polyhedron holds [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}}
proof
let p be polyhedron; ::_thesis: [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}}
set V = (dim p) -chain-space p;
set C = [#] ((dim p) -chain-space p);
A1: card ([#] ((dim p) -chain-space p)) = 2 by Th63;
reconsider C = [#] ((dim p) -chain-space p) as finite set ;
A2: {p} in C by Th65;
 ex a, b being set st
( a <> b & C = {a,b} ) by A1, CARD_2:60;
hence  [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}} by A2, Th1; ::_thesis: verum
end;

theorem Th68: :: POLYFORM:68
for p being polyhedron
for x being Element of ((dim p) -chain-space p) holds
( x = 0. ((dim p) -chain-space p) or x = {p} )
proof
let p be polyhedron; ::_thesis: for x being Element of ((dim p) -chain-space p) holds
( x = 0. ((dim p) -chain-space p) or x = {p} )
set V = (dim p) -chain-space p;
let x be Element of ((dim p) -chain-space p); ::_thesis: ( x = 0. ((dim p) -chain-space p) or x = {p} )
 x in [#] ((dim p) -chain-space p) ;
then  x in {(0. ((dim p) -chain-space p)),{p}} by Th67;
hence  ( x = 0. ((dim p) -chain-space p) or x = {p} ) by TARSKI:def_2; ::_thesis: verum
end;

theorem Th69: :: POLYFORM:69
for p being polyhedron
for x, y being Element of ((dim p) -chain-space p) holds
( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
proof
let p be polyhedron; ::_thesis: for x, y being Element of ((dim p) -chain-space p) holds
( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
set V = (dim p) -chain-space p;
let x, y be Element of ((dim p) -chain-space p); ::_thesis: ( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
assume A1: x <> y ; ::_thesis: ( x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
assume  x <> 0. ((dim p) -chain-space p) ; ::_thesis: y = 0. ((dim p) -chain-space p)
then A2: x = {p} by Th68;
assume  y <> 0. ((dim p) -chain-space p) ; ::_thesis: contradiction
hence  contradiction by A1, A2, Th68; ::_thesis: verum
end;

theorem :: POLYFORM:70
for p being polyhedron holds (dim p) -polytope-seq p = <*p*> by Def7;

theorem Th71: :: POLYFORM:71
for p being polyhedron holds 1 -th-polytope (p,(dim p)) = p
proof
let p be polyhedron; ::_thesis: 1 -th-polytope (p,(dim p)) = p
reconsider egy = 1 as Nat ;
set s = (dim p) -polytope-seq p;
A1: (dim p) -polytope-seq p = <*p*> by Def7;
 egy <= num-polytopes (p,(dim p)) by Th31;
then egy -th-polytope (p,(dim p)) = ((dim p) -polytope-seq p) . egy by Def12
.= p by A1, FINSEQ_1:40 ;
hence  1 -th-polytope (p,(dim p)) = p ; ::_thesis: verum
end;

theorem Th72: :: POLYFORM:72
for p being polyhedron
for c being Element of ((dim p) -chain-space p)
for x being Element of (dim p) -polytopes p st c = {p} holds
c @ x = 1. Z_2
proof
let p be polyhedron; ::_thesis: for c being Element of ((dim p) -chain-space p)
for x being Element of (dim p) -polytopes p st c = {p} holds
c @ x = 1. Z_2
A1: (dim p) -polytopes p = {p} by Def5;
let c be Element of ((dim p) -chain-space p); ::_thesis: for x being Element of (dim p) -polytopes p st c = {p} holds
c @ x = 1. Z_2
let x be Element of (dim p) -polytopes p; ::_thesis: ( c = {p} implies c @ x = 1. Z_2 )
assume  c = {p} ; ::_thesis: c @ x = 1. Z_2
hence  c @ x = 1. Z_2 by A1, BSPACE:def_3; ::_thesis: verum
end;

theorem Th73: :: POLYFORM:73
for p being polyhedron
for x being Element of ((dim p) - 1) -polytopes p
for c being Element of (dim p) -polytopes p st c = p holds
incidence-value (x,c) = 1. Z_2
proof
let p be polyhedron; ::_thesis: for x being Element of ((dim p) - 1) -polytopes p
for c being Element of (dim p) -polytopes p st c = p holds
incidence-value (x,c) = 1. Z_2
set f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2);
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: for c being Element of (dim p) -polytopes p st c = p holds
incidence-value (x,c) = 1. Z_2
let c be Element of (dim p) -polytopes p; ::_thesis: ( c = p implies incidence-value (x,c) = 1. Z_2 )
assume  c = p ; ::_thesis: incidence-value (x,c) = 1. Z_2
then  ( dom ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) = [:(((dim p) - 1) -polytopes p),{p}:] & c in {p} ) by FUNCOP_1:13, TARSKI:def_1;
then  [x,c] in dom ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) by ZFMISC_1:87;
then  ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) . (x,c) in rng ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) by FUNCT_1:3;
then  ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) . (x,c) in {(1. Z_2)} by FUNCOP_1:8;
then A1: ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) . (x,c) = 1. Z_2 by TARSKI:def_1;
 eta (p,(dim p)) = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) by Def6;
hence  incidence-value (x,c) = 1. Z_2 by A1, Def13; ::_thesis: verum
end;

theorem Th74: :: POLYFORM:74
for p being polyhedron
for x being Element of ((dim p) - 1) -polytopes p
for c being Element of ((dim p) -chain-space p) st c = {p} holds
incidence-sequence (x,c) = <*(1. Z_2)*>
proof
let p be polyhedron; ::_thesis: for x being Element of ((dim p) - 1) -polytopes p
for c being Element of ((dim p) -chain-space p) st c = {p} holds
incidence-sequence (x,c) = <*(1. Z_2)*>
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: for c being Element of ((dim p) -chain-space p) st c = {p} holds
incidence-sequence (x,c) = <*(1. Z_2)*>
let c be Element of ((dim p) -chain-space p); ::_thesis: ( c = {p} implies incidence-sequence (x,c) = <*(1. Z_2)*> )
assume A1: c = {p} ; ::_thesis: incidence-sequence (x,c) = <*(1. Z_2)*>
set iseq = incidence-sequence (x,c);
A2: (incidence-sequence (x,c)) . 1 = 1. Z_2
proof
reconsider egy = 1 as Nat ;
set z = egy -th-polytope (p,(dim p));
 egy <= num-polytopes (p,(dim p)) by Th31;
then A3: (incidence-sequence (x,c)) . egy = (c @ (egy -th-polytope (p,(dim p)))) * (incidence-value (x,(egy -th-polytope (p,(dim p))))) by Def16;
 ( c @ (egy -th-polytope (p,(dim p))) = 1. Z_2 & incidence-value (x,(egy -th-polytope (p,(dim p)))) = 1. Z_2 ) by A1, Th71, Th72, Th73;
hence  (incidence-sequence (x,c)) . 1 = 1. Z_2 by A3, VECTSP_1:def_6; ::_thesis: verum
end;
 num-polytopes (p,(dim p)) = 1 by Th31;
then  len (incidence-sequence (x,c)) = 1 by Def16;
hence  incidence-sequence (x,c) = <*(1. Z_2)*> by A2, FINSEQ_1:40; ::_thesis: verum
end;

theorem Th75: :: POLYFORM:75
for p being polyhedron
for x being Element of ((dim p) - 1) -polytopes p
for c being Element of ((dim p) -chain-space p) st c = {p} holds
Sum (incidence-sequence (x,c)) = 1. Z_2
proof
let p be polyhedron; ::_thesis: for x being Element of ((dim p) - 1) -polytopes p
for c being Element of ((dim p) -chain-space p) st c = {p} holds
Sum (incidence-sequence (x,c)) = 1. Z_2
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: for c being Element of ((dim p) -chain-space p) st c = {p} holds
Sum (incidence-sequence (x,c)) = 1. Z_2
let c be Element of ((dim p) -chain-space p); ::_thesis: ( c = {p} implies Sum (incidence-sequence (x,c)) = 1. Z_2 )
assume  c = {p} ; ::_thesis: Sum (incidence-sequence (x,c)) = 1. Z_2
then  incidence-sequence (x,c) = <*(1. Z_2)*> by Th74;
hence  Sum (incidence-sequence (x,c)) = 1. Z_2 by FINSOP_1:11; ::_thesis: verum
end;

theorem Th76: :: POLYFORM:76
for p being polyhedron holds ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p
proof
let p be polyhedron; ::_thesis: ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p
reconsider c = {p} as Element of ((dim p) -chain-space p) by Th64;
set T = (dim p) -boundary p;
set X = ((dim p) - 1) -polytopes p;
reconsider d = ((dim p) - 1) -polytopes p as Element of (((dim p) - 1) -chain-space p) by ZFMISC_1:def_1;
reconsider Tc = ((dim p) -boundary p) . c as Element of (((dim p) - 1) -chain-space p) ;
 for x being Element of ((dim p) - 1) -polytopes p holds
( x in Tc iff x in d )
proof
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: ( x in Tc iff x in d )
thus  ( x in Tc implies x in d ) ; ::_thesis: ( x in d implies x in Tc )
thus  ( x in d implies x in Tc ) ::_thesis: verum
proof
assume  x in d ; ::_thesis: x in Tc
 Sum (incidence-sequence (x,c)) = 1. Z_2 by Th75;
then  x in Boundary c by Def17;
hence  x in Tc by Def18; ::_thesis: verum
end;
end;
hence  ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p by SUBSET_1:3; ::_thesis: verum
end;

theorem Th77: :: POLYFORM:77
for p being polyhedron holds (dim p) -boundary p is one-to-one
proof
let p be polyhedron; ::_thesis: (dim p) -boundary p is one-to-one
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 (dim p) -boundary p is one-to-one ; ::_thesis: contradiction
then consider x1, x2 being set  such that
A1: x1 in dom ((dim p) -boundary p) and
A2: x2 in dom ((dim p) -boundary p) and
A3: ((dim p) -boundary p) . x1 = ((dim p) -boundary p) . x2 and
A4: x1 <> x2 by FUNCT_1:def_4;
reconsider x2 = x2 as Element of ((dim p) -chain-space p) by A2;
reconsider x1 = x1 as Element of ((dim p) -chain-space p) by A1;
percases ( x1 = 0. ((dim p) -chain-space p) or x2 = 0. ((dim p) -chain-space p) ) by A4, Th69;
suppose x1 = 0. ((dim p) -chain-space p) ; ::_thesis: contradiction
then  ( x2 = {p} & ((dim p) -boundary p) . x1 = 0. (((dim p) - 1) -chain-space p) ) by A4, Th68, RANKNULL:9;
hence  contradiction by A3, Th76; ::_thesis: verum
end;
suppose x2 = 0. ((dim p) -chain-space p) ; ::_thesis: contradiction
then  ( x1 = {p} & ((dim p) -boundary p) . x2 = 0. (((dim p) - 1) -chain-space p) ) by A4, Th68, RANKNULL:9;
hence  contradiction by A3, Th76; ::_thesis: verum
end;
end;
end;

theorem Th78: :: POLYFORM:78
for p being polyhedron holds dim (((dim p) - 1) -bounding-chain-space p) = 1
proof
let p be polyhedron; ::_thesis: dim (((dim p) - 1) -bounding-chain-space p) = 1
set d = dim p;
set T = (dim p) -boundary p;
set U = (dim p) -chain-space p;
set V = ((dim p) - 1) -bounding-chain-space p;
A1: card ([#] (((dim p) - 1) -bounding-chain-space p)) = card (((dim p) -boundary p) .: ([#] ((dim p) -chain-space p))) by RANKNULL:def_2
.= card (rng ((dim p) -boundary p)) by RELSET_1:22 ;
A2: card (dom ((dim p) -boundary p)) = card ([#] ((dim p) -chain-space p)) by RANKNULL:7
.= 2 by Th63 ;
 (dim p) -boundary p is one-to-one by Th77;
then  card ([#] (((dim p) - 1) -bounding-chain-space p)) = 2 by A1, A2, CARD_1:70;
hence  dim (((dim p) - 1) -bounding-chain-space p) = 1 by RANKNULL:6; ::_thesis: verum
end;

theorem Th79: :: POLYFORM:79
for p being polyhedron st p is simply-connected holds
dim (((dim p) - 1) -circuit-space p) = 1
proof
let p be polyhedron; ::_thesis: ( p is simply-connected implies dim (((dim p) - 1) -circuit-space p) = 1 )
set d = dim p;
set U = ((dim p) - 1) -bounding-chain-space p;
set V = ((dim p) - 1) -circuit-space p;
assume  p is simply-connected ; ::_thesis: dim (((dim p) - 1) -circuit-space p) = 1
then  ((dim p) - 1) -bounding-chain-space p = ((dim p) - 1) -circuit-space p by Th50;
hence  dim (((dim p) - 1) -circuit-space p) = 1 by Th78; ::_thesis: verum
end;

theorem Th80: :: POLYFORM:80
for p being polyhedron
for n being Nat st 1 < n & n < (dim p) + 2 holds
(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
proof
let p be polyhedron; ::_thesis: for n being Nat st 1 < n & n < (dim p) + 2 holds
(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
let n be Nat; ::_thesis: ( 1 < n & n < (dim p) + 2 implies (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) )
assume A1: 1 < n ; ::_thesis: ( not n < (dim p) + 2 or (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) )
 1 - 1 = 0 ;
then reconsider m = n - 1 as Element of NAT by A1, INT_1:3, XREAL_1:13;
reconsider m = m as Nat ;
set apcs = alternating-proper-f-vector p;
set acs = alternating-f-vector p;
A2: 2 - 1 = 1 ;
 1 + 1 = 2 ;
then  2 <= n by A1, INT_1:7;
then A3: 1 <= m by A2, XREAL_1:13;
assume A4: n < (dim p) + 2 ; ::_thesis: (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
then  n < ((dim p) + 1) + 1 ;
then  n <= (dim p) + 1 by NAT_1:13;
then  n - 1 <= ((dim p) + 1) - 1 by XREAL_1:9;
then A5: (alternating-proper-f-vector p) . m = ((- 1) |^ (m + 1)) * (num-polytopes (p,(m - 1))) by A3, Def27;
 (alternating-f-vector p) . n = ((- 1) |^ n) * (num-polytopes (p,(n - 2))) by A1, A4, Def26;
hence  (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) by A5; ::_thesis: verum
end;

theorem Th81: :: POLYFORM:81
for p being polyhedron holds alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>
proof
let p be polyhedron; ::_thesis: alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
set r = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>;
set n = dim p;
A1: len <*((- 1) |^ (dim p))*> = 1 by FINSEQ_1:39;
A2: len (alternating-proper-f-vector p) = dim p by Def27;
A3: len (alternating-f-vector p) = (dim p) + 2 by Def26;
A4: for k being Nat st 1 <= k & k <= len (alternating-f-vector p) holds
(alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len (alternating-f-vector p) implies (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k )
assume A5: ( 1 <= k & k <= len (alternating-f-vector p) ) ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
percases ( k = 1 or k = (dim p) + 2 or ( 1 < k & k < (dim p) + 2 ) ) by A3, A5, XXREAL_0:1;
supposeA6: k = 1 ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
reconsider o = 1 as Nat ;
 ( 1 <= (dim p) + 2 & o - 2 = - 1 ) by Th12;
then A7: (alternating-f-vector p) . o = ((- 1) |^ o) * (num-polytopes (p,(- 1))) by Def26;
 ( (- 1) |^ 1 = - 1 & num-polytopes (p,(- 1)) = 1 ) by Th4, Th9, Th30;
hence  (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A6, A7, Th17; ::_thesis: verum
end;
supposeA8: k = (dim p) + 2 ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
 len <*(- 1)*> = 1 by FINSEQ_1:39;
then  k = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + 1 by A2, A8;
then A9: ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (- 1) |^ (dim p) by Th18
.= (- 1) |^ k by A8, Th14 ;
 1 <= k by A8, Th12;
then A10: (alternating-f-vector p) . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) by A8, Def26;
 num-polytopes (p,(k - 2)) = 1 by A8, Th31;
hence  (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A10, A9; ::_thesis: verum
end;
supposeA11: ( 1 < k & k < (dim p) + 2 ) ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
set m = k - 1;
A12: ( (k + 1) - 1 = k & ((dim p) + 2) - 1 = (dim p) + 1 ) ;
A13: k + 1 <= (dim p) + 2 by A11, INT_1:7;
len (<*(- 1)*> ^ (alternating-proper-f-vector p)) = (len <*(- 1)*>) + (len (alternating-proper-f-vector p)) by FINSEQ_1:22
.= (dim p) + 1 by A2, FINSEQ_1:39 ;
then  ( len <*(- 1)*> = 1 & k <= len (<*(- 1)*> ^ (alternating-proper-f-vector p)) ) by A13, A12, FINSEQ_1:39, XREAL_1:9;
then  ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (alternating-proper-f-vector p) . (k - 1) by A11, Th19;
hence  (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A11, Th80; ::_thesis: verum
end;
end;
end;
 ( len ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + (len <*((- 1) |^ (dim p))*>) & len <*(- 1)*> = 1 ) by Th16, FINSEQ_1:39;
hence  alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by A3, A2, A1, A4, FINSEQ_1:14; ::_thesis: verum
end;

begin

theorem Th82: :: POLYFORM:82
for p being polyhedron st dim p is odd holds
Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2
proof
let p be polyhedron; ::_thesis: ( dim p is odd implies Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2 )
reconsider minusone = - 1 as Integer ;
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
reconsider lastterm = (- 1) |^ (dim p) as Integer ;
assume  dim p is odd ; ::_thesis: Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2
then A1: (- 1) |^ (dim p) = - 1 by Th9;
 alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by Th81;
then  Sum (alternating-f-vector p) = ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (Sum <*lastterm*>) by Th21
.= ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (- 1) by A1, RVSUM_1:73
.= ((- 1) + (Sum (alternating-proper-f-vector p))) + (- 1) by RVSUM_1:73
.= (Sum (alternating-proper-f-vector p)) - 2 ;
hence  Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2 ; ::_thesis: verum
end;

theorem Th83: :: POLYFORM:83
for p being polyhedron st dim p is even holds
Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)
proof
let p be polyhedron; ::_thesis: ( dim p is even implies Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) )
reconsider minusone = - 1 as Integer ;
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
reconsider lastterm = (- 1) |^ (dim p) as Integer ;
assume  dim p is even ; ::_thesis: Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)
then A1: (- 1) |^ (dim p) = 1 by Th8;
 alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by Th81;
then  Sum (alternating-f-vector p) = ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (Sum <*lastterm*>) by Th21
.= ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + 1 by A1, RVSUM_1:73
.= ((- 1) + (Sum (alternating-proper-f-vector p))) + 1 by RVSUM_1:73
.= Sum (alternating-proper-f-vector p) ;
hence  Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) ; ::_thesis: verum
end;

theorem Th84: :: POLYFORM:84
for p being polyhedron st dim p = 1 holds
Sum (alternating-proper-f-vector p) = num-polytopes (p,0)
proof
let p be polyhedron; ::_thesis: ( dim p = 1 implies Sum (alternating-proper-f-vector p) = num-polytopes (p,0) )
reconsider egy = 1 as Nat ;
set apcs = alternating-proper-f-vector p;
assume  dim p = 1 ; ::_thesis: Sum (alternating-proper-f-vector p) = num-polytopes (p,0)
then A1: ( len (alternating-proper-f-vector p) = 1 & (alternating-proper-f-vector p) . egy = ((- 1) |^ (egy + 1)) * (num-polytopes (p,(egy - 1))) ) by Def27;
 (- 1) |^ (egy + 1) = 1 by Th5, Th8;
then  alternating-proper-f-vector p = <*(num-polytopes (p,0))*> by A1, FINSEQ_1:40;
hence  Sum (alternating-proper-f-vector p) = num-polytopes (p,0) by RVSUM_1:73; ::_thesis: verum
end;

theorem Th85: :: POLYFORM:85
for p being polyhedron st dim p = 2 holds
Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))
proof
let p be polyhedron; ::_thesis: ( dim p = 2 implies Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1)) )
reconsider t = 2 as Nat ;
reconsider o = 1 as Nat ;
set apcs = alternating-proper-f-vector p;
reconsider apcso = (alternating-proper-f-vector p) . o as Integer ;
reconsider apcst = (alternating-proper-f-vector p) . t as Integer ;
assume A1: dim p = 2 ; ::_thesis: Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))
then A2: ( (alternating-proper-f-vector p) . o = ((- 1) |^ (o + 1)) * (num-polytopes (p,(o - 1))) & (alternating-proper-f-vector p) . t = ((- 1) |^ (t + 1)) * (num-polytopes (p,(t - 1))) ) by Def27;
A3: ( (- 1) |^ (o + 1) = 1 & (- 1) |^ (t + 1) = - 1 ) by Th5, Th8, Th9;
 len (alternating-proper-f-vector p) = 2 by A1, Def27;
then  alternating-proper-f-vector p = <*apcso,apcst*> by FINSEQ_1:44;
then  Sum (alternating-proper-f-vector p) = apcso + apcst by RVSUM_1:77
.= (num-polytopes (p,0)) - (num-polytopes (p,1)) by A2, A3 ;
hence  Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1)) ; ::_thesis: verum
end;

theorem Th86: :: POLYFORM:86
for p being polyhedron st dim p = 3 holds
Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))
proof
let p be polyhedron; ::_thesis: ( dim p = 3 implies Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) )
reconsider mo = - 1 as Integer ;
reconsider th = 3 as Nat ;
reconsider tw = 2 as Nat ;
reconsider o = 1 as Nat ;
assume A1: dim p = 3 ; ::_thesis: Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))
set apcs = alternating-proper-f-vector p;
 (- 1) |^ (tw + 1) = - 1 by Th6, Th9;
then A2: (alternating-proper-f-vector p) . tw = mo * (num-polytopes (p,(tw - 1))) by A1, Def27;
 (- 1) |^ (th + 1) = 1 by Th7, Th8;
then A3: (alternating-proper-f-vector p) . th = o * (num-polytopes (p,(th - 1))) by A1, Def27;
reconsider apcsth = (alternating-proper-f-vector p) . th as Integer ;
reconsider apcstw = (alternating-proper-f-vector p) . tw as Integer ;
reconsider apcson = (alternating-proper-f-vector p) . o as Integer ;
 (- 1) |^ (o + 1) = 1 by Th5, Th8;
then A4: (alternating-proper-f-vector p) . o = o * (num-polytopes (p,(o - 1))) by A1, Def27;
 len (alternating-proper-f-vector p) = 3 by A1, Def27;
then  alternating-proper-f-vector p = <*apcson,apcstw,apcsth*> by FINSEQ_1:45;
then  Sum (alternating-proper-f-vector p) = (apcson + apcstw) + apcsth by RVSUM_1:78
.= ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) by A4, A2, A3 ;
hence  Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) ; ::_thesis: verum
end;

theorem Th87: :: POLYFORM:87
for p being polyhedron st dim p = 0 holds
p is eulerian
proof
let p be polyhedron; ::_thesis: ( dim p = 0 implies p is eulerian )
set d = dim p;
set apcs = alternating-proper-f-vector p;
assume A1: dim p = 0 ; ::_thesis: p is eulerian
then  (- 1) |^ ((dim p) + 1) = - 1 by NEWTON:5;
then A2: 1 + ((- 1) |^ ((dim p) + 1)) = 0 ;
 len (alternating-proper-f-vector p) = 0 by A1, Def27;
then  alternating-proper-f-vector p = <*> INT ;
hence  p is eulerian by A2, Def29, GR_CY_1:3; ::_thesis: verum
end;

theorem Th88: :: POLYFORM:88
for p being polyhedron st p is simply-connected holds
p is eulerian
proof
let p be polyhedron; ::_thesis: ( p is simply-connected implies p is eulerian )
assume A1: p is simply-connected ; ::_thesis: p is eulerian
set apcs = alternating-proper-f-vector p;
percases ( dim p = 0 or dim p > 0 ) ;
suppose dim p = 0 ; ::_thesis: p is eulerian
hence  p is eulerian by Th87; ::_thesis: verum
end;
supposeA2: dim p > 0 ; ::_thesis: p is eulerian
deffunc H1( Nat) ->  Element of INT = ((- 1) |^ ($1 + 1)) * (dim (($1 - 1) -circuit-space p));
deffunc H2( Nat) ->  Element of INT = ((- 1) |^ ($1 + 1)) * (dim (($1 - 2) -bounding-chain-space p));
consider a being FinSequence such that
A3: len a = len (alternating-proper-f-vector p) and
A4: for n being Nat st n in dom a holds
a . n = H2(n) from FINSEQ_1:sch_2();
A5: rng a c= INT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng a or y in INT )
assume  y in rng a ; ::_thesis: y in INT
then consider x being set  such that
A6: x in dom a and
A7: y = a . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A6;
 a . x = ((- 1) |^ (x + 1)) * (dim ((x - 2) -bounding-chain-space p)) by A4, A6;
hence  y in INT by A7; ::_thesis: verum
end;
consider b being FinSequence such that
A8: len b = len (alternating-proper-f-vector p) and
A9: for n being Nat st n in dom b holds
b . n = H1(n) from FINSEQ_1:sch_2();
 rng b c= INT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng b or y in INT )
assume  y in rng b ; ::_thesis: y in INT
then consider x being set  such that
A10: x in dom b and
A11: y = b . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A10;
 b . x = ((- 1) |^ (x + 1)) * (dim ((x - 1) -circuit-space p)) by A9, A10;
hence  y in INT by A11; ::_thesis: verum
end;
then reconsider a = a, b = b as FinSequence of INT by A5, FINSEQ_1:def_4;
A12: len (alternating-proper-f-vector p) > 0 by A2, Def27;
A13: a . 1 = 1
proof
reconsider egy = 1 as Element of NAT ;
 1 <= 0 + 1 ;
then  egy <= len (alternating-proper-f-vector p) by A12, NAT_1:13;
then  egy in dom a by A3, FINSEQ_3:25;
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 Th62 ;
hence  a . 1 = 1 ; ::_thesis: verum
end;
A14: for n being Nat st 1 <= n & n < len (alternating-proper-f-vector p) holds
b . n = - (a . (n + 1))
proof
let n be Nat; ::_thesis: ( 1 <= n & n < len (alternating-proper-f-vector p) implies b . n = - (a . (n + 1)) )
assume that
A15: 1 <= n and
A16: n < len (alternating-proper-f-vector p) ; ::_thesis: b . n = - (a . (n + 1))
A17: n in dom b by A8, A15, A16, FINSEQ_3:25;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A18: b . n = ((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p)) by A9, A17;
A19: 1 <= n + 1 by NAT_1:11;
 n + 1 <= len (alternating-proper-f-vector p) by A16, INT_1:7;
then  n + 1 in dom a by A3, A19, FINSEQ_3:25;
then a . (n + 1) = H2(n + 1) by A4
.= (((- 1) |^ (n + 1)) * ((- 1) |^ 1)) * (dim ((n - 1) -bounding-chain-space p)) by NEWTON:8
.= (((- 1) |^ (n + 1)) * (- 1)) * (dim ((n - 1) -bounding-chain-space p)) by NEWTON:5
.= - (((- 1) |^ (n + 1)) * (dim ((n - 1) -bounding-chain-space p)))
.= - (b . n) by A1, A18, Th50 ;
hence  b . n = - (a . (n + 1)) ; ::_thesis: verum
end;
A20: b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1)
proof
reconsider n = len (alternating-proper-f-vector p) as Element of NAT ;
A21: n = dim p by Def27;
 0 + 1 = 1 ;
then  1 <= len (alternating-proper-f-vector p) by A12, NAT_1:13;
then  n in dom b by A8, FINSEQ_3:25;
then b . n = H1(n) by A9
.= ((- 1) |^ (n + 1)) * 1 by A1, A21, Th79
.= (- 1) |^ (n + 1) ;
hence  b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1) by Def27; ::_thesis: verum
end;
 for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds
(alternating-proper-f-vector p) . n = (a . n) + (b . n)
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len (alternating-proper-f-vector p) implies (alternating-proper-f-vector p) . n = (a . n) + (b . n) )
assume A22: ( 1 <= n & n <= len (alternating-proper-f-vector p) ) ; ::_thesis: (alternating-proper-f-vector p) . n = (a . n) + (b . n)
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
 n9 in dom a by A3, A22, FINSEQ_3:25;
then A23: a . n9 = ((- 1) |^ (n9 + 1)) * (dim ((n9 - 2) -bounding-chain-space p)) by A4;
 ( (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))) & n9 in dom b ) by A8, A22, Th51, FINSEQ_3:25;
hence  (alternating-proper-f-vector p) . n = (a . n) + (b . n) by A9, A23; ::_thesis: verum
end;
then  Sum (alternating-proper-f-vector p) = (a . 1) + (b . (len (alternating-proper-f-vector p))) by A12, A3, A8, A14, Th15;
hence  p is eulerian by A13, A20, Def29; ::_thesis: verum
end;
end;
end;

theorem :: POLYFORM:89
for p being polyhedron st p is simply-connected & dim p = 1 holds
num-vertices p = 2
proof
let p be polyhedron; ::_thesis: ( p is simply-connected & dim p = 1 implies num-vertices p = 2 )
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
assume  p is simply-connected ; ::_thesis: ( not dim p = 1 or num-vertices p = 2 )
then A1: p is eulerian by Th88;
assume A2: dim p = 1 ; ::_thesis: num-vertices p = 2
0 = Sum (alternating-f-vector p) by A1, Def31
.= (Sum (alternating-proper-f-vector p)) - 2 by A2, Th4, Th82
.= (num-polytopes (p,0)) - 2 by A2, Th84 ;
hence  num-vertices p = 2 ; ::_thesis: verum
end;

theorem :: POLYFORM:90
for p being polyhedron st p is simply-connected & dim p = 2 holds
num-vertices p = num-edges p
proof
let p be polyhedron; ::_thesis: ( p is simply-connected & dim p = 2 implies num-vertices p = num-edges p )
set s = (num-polytopes (p,0)) - (num-polytopes (p,1));
set c = alternating-f-vector p;
assume  p is simply-connected ; ::_thesis: ( not dim p = 2 or num-vertices p = num-edges p )
then A1: p is eulerian by Th88;
assume A2: dim p = 2 ; ::_thesis: num-vertices p = num-edges p
then A3: (num-polytopes (p,0)) - (num-polytopes (p,1)) = Sum (alternating-proper-f-vector p) by Th85;
0 = Sum (alternating-f-vector p) by A1, Def31
.= (num-polytopes (p,0)) - (num-polytopes (p,1)) by A2, A3, Th5, Th83 ;
hence  num-vertices p = num-edges p ; ::_thesis: verum
end;

theorem :: POLYFORM:91
for p being polyhedron st p is simply-connected & dim p = 3 holds
((num-vertices p) - (num-edges p)) + (num-faces p) = 2
proof
let p be polyhedron; ::_thesis: ( p is simply-connected & dim p = 3 implies ((num-vertices p) - (num-edges p)) + (num-faces p) = 2 )
set s = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2));
set c = alternating-f-vector p;
assume  p is simply-connected ; ::_thesis: ( not dim p = 3 or ((num-vertices p) - (num-edges p)) + (num-faces p) = 2 )
then A1: p is eulerian by Th88;
assume A2: dim p = 3 ; ::_thesis: ((num-vertices p) - (num-edges p)) + (num-faces p) = 2
then A3: ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) = Sum (alternating-proper-f-vector p) by Th86;
0 = Sum (alternating-f-vector p) by A1, Def31
.= (((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))) - 2 by A2, A3, Th6, Th82 ;
hence  ((num-vertices p) - (num-edges p)) + (num-faces p) = 2 ; ::_thesis: verum
end;