let p be polyhedron; :: thesis: 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)))
let n be Nat; :: thesis: ( 1 <= n & n <= len (alternating-proper-f-vector p) implies (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))) )
set apcs = alternating-proper-f-vector p;
assume A1: 1 <= n ; :: thesis: ( not n <= len (alternating-proper-f-vector p) or (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))) )
set a = (- 1) |^ (n + 1);
assume n <= len (alternating-proper-f-vector p) ; :: thesis: (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)))
then n <= dim p by Def27;
then (alternating-proper-f-vector p) . n = ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A1, Def27
.= ((- 1) |^ (n + 1)) * (dim ((n - 1) -chain-space p)) by Th34
.= ((- 1) |^ (n + 1)) * ((rank ((n - 1) -boundary p)) + (nullity ((n - 1) -boundary p))) by RANKNULL:44
.= (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p))) ;
hence (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))) ; :: thesis: verum