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 Th72;
hence Sum (incidence-sequence (x,c)) = 1. Z_2 by FINSOP_1:11; :: thesis: verum