let p be polyhedron; :: thesis: alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p)
set acs = alternating-f-vector p;
set aspcs = alternating-semi-proper-f-vector p;
set d = dim p;
set r = <*(- 1)*> ^ (alternating-semi-proper-f-vector p);
A1: len (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) = (len <*(- 1)*>) + (len (alternating-semi-proper-f-vector p)) by FINSEQ_1:22
.= (len <*(- 1)*>) + ((dim p) + 1) by Def28
.= 1 + ((dim p) + 1) by FINSEQ_1:40
.= (dim p) + 2 ;
A2: for n being Nat st 1 <= n & n <= len (alternating-f-vector p) holds
(alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len (alternating-f-vector p) implies (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n )
assume that
A3: 1 <= n and
A4: n <= len (alternating-f-vector p) ; :: thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
A5: n <= (dim p) + 2 by A4, Def26;

per cases ( n = 1 or n > 1 ) by A3, XXREAL_0:1;

suppose A6: n = 1 ; :: thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n

then (alternating-f-vector p) . n = ((- 1) |^ 1) * (num-polytopes (p,(1 - 2))) by A5, Def26
.= (- 1) * (num-polytopes (p,(- 1)))
.= (- 1) * 1 by Th28
.= - 1 ;
hence (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n by A6, FINSEQ_1:41; :: thesis: verum

end;

suppose A7: n > 1 ; :: thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n

then A8: 1 - 1 < n - 1 by XREAL_1:9;
then reconsider m = n - 1 as Element of NAT by INT_1:3;
n - 1 <= ((dim p) + 2) - 1 by A5, XREAL_1:9;
then A9: m <= (dim p) + 1 ;
len <*(- 1)*> = 1 by FINSEQ_1:39;
then A10: (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n = (alternating-semi-proper-f-vector p) . (n - 1) by A1, A5, A7, FINSEQ_1:24;
0 < 0 + m by A8;
then 1 <= m by NAT_1:19;
then (alternating-semi-proper-f-vector p) . m = ((- 1) |^ (m + 1)) * (num-polytopes (p,(m - 1))) by A9, Def28
.= ((- 1) |^ n) * (num-polytopes (p,(n - 2))) ;
hence (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n by A3, A5, A10, Def26; :: thesis: verum

end;

end;

end;

len (alternating-f-vector p) = len (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) by A1, Def26;
hence alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p) by A2; :: thesis: verum