for p being polyhedron
for k being Integer
for x being Element of k -polytopes p holds (0. (k -chain-space p)) @ x = 0. Z_2 by BSPACE:14;