for p being polyhedron
for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds
(alternating-proper-f-vector p) . n = (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p)))