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 and
A5: 1 <= n and
A6: n <= num-polytopes p,k ; :: thesis: (incidence-sequence e,v) . n = 1. Z_2
set iseq = incidence-sequence e,v;
A7: not (k - 1) -polytopes p is empty by A1, Def5;
A8: x in v by A2, TARSKI:def 1;
(incidence-sequence e,v) . n = (v @ x) * (incidence-value e,x) by A4, A5, A6, A7, Def16
.= (1. Z_2 ) * (incidence-value e,x) by A8, BSPACE:def 3
.= (1. Z_2 ) * (1. Z_2 ) by A1, A3, Th58
.= 1. Z_2 by VECTSP_1:def 16 ;
hence (incidence-sequence e,v) . n = 1. Z_2 ; :: thesis: verum