let p be polyhedron; :: thesis: for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for m, n being Nat st k = 0 & v = {x} & x = n -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) & 1 <= n & n <= num-polytopes (p,k) & m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
let k be Integer; :: thesis: for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for m, n being Nat st k = 0 & v = {x} & x = n -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) & 1 <= n & n <= num-polytopes (p,k) & m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
let x be Element of k -polytopes p; :: thesis: for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for m, n being Nat st k = 0 & v = {x} & x = n -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) & 1 <= n & n <= num-polytopes (p,k) & m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
let e be Element of (k - 1) -polytopes p; :: thesis: for v being Element of (k -chain-space p)
for m, n being Nat st k = 0 & v = {x} & x = n -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) & 1 <= n & n <= num-polytopes (p,k) & m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
let v be Element of (k -chain-space p); :: thesis: for m, n being Nat st k = 0 & v = {x} & x = n -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) & 1 <= n & n <= num-polytopes (p,k) & m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
let m, n be Nat; :: thesis: ( k = 0 & v = {x} & x = n -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) & 1 <= n & n <= num-polytopes (p,k) & m <> n implies (incidence-sequence (e,v)) . m = 0. Z_2 )
assume that
A1: k = 0 and
A2: v = {x} and
A3: x = n -th-polytope (p,k) and
A4: ( 1 <= m & m <= num-polytopes (p,k) ) and
A5: ( 1 <= n & n <= num-polytopes (p,k) & m <> n ) ; :: thesis: (incidence-sequence (e,v)) . m = 0. Z_2
A6: m -th-polytope (p,k) <> x by A3, A4, A5, Th35;

now

assume v @ (m -th-polytope (p,k)) = 1. Z_2 ; :: thesis: contradiction
then m -th-polytope (p,k) in {x} by A2, BSPACE:9;
hence contradiction by A6, TARSKI:def 1; :: thesis: verum

end;

then A7: v @ (m -th-polytope (p,k)) = 0. Z_2 by BSPACE:11;
set iseq = incidence-sequence (e,v);
not (k - 1) -polytopes p is empty by A1, Def5;
then (incidence-sequence (e,v)) . m = (0. Z_2) * (incidence-value (e,(m -th-polytope (p,k)))) by A4, A7, Def16
.= 0. Z_2 by VECTSP_1:7 ;
hence (incidence-sequence (e,v)) . m = 0. Z_2 ; :: thesis: verum