let p be polyhedron; :: thesis: ( dim p is odd implies Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2 )
reconsider minusone = - 1 as Integer ;
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
reconsider lastterm = (- 1) |^ (dim p) as Integer ;
assume dim p is odd ; :: thesis: Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2
then A1: (- 1) |^ (dim p) = - 1 by Th8;
alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by Th79;
then Sum (alternating-f-vector p) = ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (Sum <*lastterm*>) by Th19
.= ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (- 1) by A1, RVSUM_1:73
.= ((- 1) + (Sum (alternating-proper-f-vector p))) + (- 1) by RVSUM_1:73
.= (Sum (alternating-proper-f-vector p)) - 2 ;
hence Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2 ; :: thesis: verum