let p be polyhedron; :: thesis: ( dim p = 2 implies Sum (alternating-proper-f-vector p) = (num-polytopes p,0 ) - (num-polytopes p,1) )
reconsider t = 2 as Nat ;
reconsider o = 1 as Nat ;
set apcs = alternating-proper-f-vector p;
reconsider apcso = (alternating-proper-f-vector p) . o as Integer ;
reconsider apcst = (alternating-proper-f-vector p) . t as Integer ;
assume A1: dim p = 2 ; :: thesis: Sum (alternating-proper-f-vector p) = (num-polytopes p,0 ) - (num-polytopes p,1)
then A2: ( (alternating-proper-f-vector p) . o = ((- 1) |^ (o + 1)) * (num-polytopes p,(o - 1)) & (alternating-proper-f-vector p) . t = ((- 1) |^ (t + 1)) * (num-polytopes p,(t - 1)) ) by Def27;
A3: ( (- 1) |^ (o + 1) = 1 & (- 1) |^ (t + 1) = - 1 ) by Th5, Th8, Th9;
len (alternating-proper-f-vector p) = 2 by A1, Def27;
then alternating-proper-f-vector p = <*apcso,apcst*> by FINSEQ_1:61;
then Sum (alternating-proper-f-vector p) = apcso + apcst by RVSUM_1:107
.= (num-polytopes p,0 ) - (num-polytopes p,1) by A2, A3 ;
hence Sum (alternating-proper-f-vector p) = (num-polytopes p,0 ) - (num-polytopes p,1) ; :: thesis: verum