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