let p be polyhedron; :: thesis: ( dim p is even implies Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) )
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 even ; :: thesis: Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)
then A1: (- 1) |^ (dim p) = 1 by Th7;
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) ;
hence Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) ; :: thesis: verum