let p be polyhedron; 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; 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); ( c = {p} implies incidence-sequence (x,c) = <*(1. Z_2)*> )
assume A1:
c = {p}
; 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;
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; verum