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;
num-polytopes p,(dim p) = 1 by Th32;
then A2: len (incidence-sequence x,c) = 1 by Def16;
(incidence-sequence x,c) . 1 = 1. Z_2

proof

reconsider egy = 1 as Nat ;
A3: egy <= num-polytopes p,(dim p) by Th32;
set z = egy -th-polytope p,(dim p);
A4: (incidence-sequence x,c) . egy = (c @ (egy -th-polytope p,(dim p))) * (incidence-value x,(egy -th-polytope p,(dim p))) by A3, Def16;
A5: c @ (egy -th-polytope p,(dim p)) = 1. Z_2 by A1, Th73;
incidence-value x,(egy -th-polytope p,(dim p)) = 1. Z_2 by Th72, Th74;
hence (incidence-sequence x,c) . 1 = 1. Z_2 by A4, A5, VECTSP_1:def 16; :: thesis: verum

end;

hence incidence-sequence x,c = <*(1. Z_2 )*> by A2, FINSEQ_1:57; :: thesis: verum