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, Th33;
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, Th60; :: 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, Th59;
hence Sum (incidence-sequence (e,v)) = 1. Z_2 by A10, A7, MATRIX_3:12; :: thesis: verum