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 Th32;
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, Th72, Th73, Th74;
hence (incidence-sequence x,c) . 1 = 1. Z_2 by A3, VECTSP_1:def 16; :: thesis: verum

end;

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