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 Th5, Th8;
then alternating-proper-f-vector p = <*(num-polytopes p,0 )*> by A1, FINSEQ_1:57;
hence Sum (alternating-proper-f-vector p) = num-polytopes p,0 by RVSUM_1:103; :: thesis: verum