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
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
incidence-sequence (x,c) = <*(1. Z_2)*>
let c be Element of ((dim p) -chain-space p); :: thesis: ( c = {p} implies incidence-sequence (x,c) = <*(1. Z_2)*> )
assume A1: c = {p} ; :: thesis: incidence-sequence (x,c) = <*(1. Z_2)*>
set iseq = incidence-sequence (x,c);
A2: (incidence-sequence (x,c)) . 1 = 1. Z_2

proof

reconsider egy = 1 as Nat ;
set z = egy -th-polytope (p,(dim p));
egy <= num-polytopes (p,(dim p)) by Th29;
then A3: (incidence-sequence (x,c)) . egy = (c @ (egy -th-polytope (p,(dim p)))) * (incidence-value (x,(egy -th-polytope (p,(dim p))))) by Def16;
( c @ (egy -th-polytope (p,(dim p))) = 1. Z_2 & incidence-value (x,(egy -th-polytope (p,(dim p)))) = 1. Z_2 ) by A1, Th69, Th70, Th71;
hence (incidence-sequence (x,c)) . 1 = 1. Z_2 by A3; :: thesis: verum

end;

num-polytopes (p,(dim p)) = 1 by Th29;
then len (incidence-sequence (x,c)) = 1 by Def16;
hence incidence-sequence (x,c) = <*(1. Z_2)*> by A2, FINSEQ_1:40; :: thesis: verum