:: 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 b₅ being FinSequence of Z_2 holds
( b₅ = incidence-sequence (x,v) iff ( ( (k - 1) -polytopes p is empty implies b₅ = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b₅ = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b₅ . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) );