let p be polyhedron; :: thesis: ( dim p = 1 implies Sum (alternating-proper-f-vector p) = num-polytopes (p,0) )
reconsider egy = 1 as Nat ;
set apcs = alternating-proper-f-vector p;
assume dim p = 1 ; :: thesis: Sum (alternating-proper-f-vector p) = num-polytopes (p,0)
then A1: ( len (alternating-proper-f-vector p) = 1 & (alternating-proper-f-vector p) . egy = ((- 1) |^ (egy + 1)) * (num-polytopes (p,(egy - 1))) ) by Def27;
(- 1) |^ (egy + 1) = 1 by Th4, Th7;
then alternating-proper-f-vector p = <*(num-polytopes (p,0))*> by A1, FINSEQ_1:40;
hence Sum (alternating-proper-f-vector p) = num-polytopes (p,0) by RVSUM_1:73; :: thesis: verum