set aspcs = alternating-semi-proper-f-vector p;
set apcs = alternating-proper-f-vector p;
alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*> by Th50;
then A1: Sum (alternating-semi-proper-f-vector p) = (Sum (alternating-proper-f-vector p)) + ((- 1) |^ (dim p)) by RVSUM_1:74;
A2: ( Sum (alternating-semi-proper-f-vector p) = 1 implies p is eulerian )
proof
assume Sum (alternating-semi-proper-f-vector p) = 1 ; :: thesis: p is eulerian
then Sum (alternating-proper-f-vector p) = 1 + ((- 1) * ((- 1) |^ (dim p))) by A1
.= 1 + ((- 1) |^ ((dim p) + 1)) by NEWTON:6 ;
hence p is eulerian ; :: thesis: verum
end;
( p is eulerian implies Sum (alternating-semi-proper-f-vector p) = 1 )
proof
assume p is eulerian ; :: thesis: Sum (alternating-semi-proper-f-vector p) = 1
then Sum (alternating-semi-proper-f-vector p) = (1 + ((- 1) |^ ((dim p) + 1))) + ((- 1) |^ (dim p)) by A1
.= (1 + ((- 1) * ((- 1) |^ (dim p)))) + ((- 1) |^ (dim p)) by NEWTON:6
.= 1 ;
hence Sum (alternating-semi-proper-f-vector p) = 1 ; :: thesis: verum
end;
hence ( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 ) by A2; :: thesis: verum