let p be polyhedron; :: thesis: ( dim p is even implies Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) )
assume A1: dim p is even ; :: thesis: Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
A2: alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by Th82;
A3: (- 1) |^ (dim p) = 1 by A1, Th8;
reconsider minusone = - 1 as Integer ;
reconsider lastterm = (- 1) |^ (dim p) as Integer ;
Sum (alternating-f-vector p) = ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (Sum <*lastterm*>) by A2, Th22
.= ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + 1 by A3, RVSUM_1:103
.= ((- 1) + (Sum (alternating-proper-f-vector p))) + 1 by RVSUM_1:103
.= Sum (alternating-proper-f-vector p) ;
hence Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) ; :: thesis: verum