let p be polyhedron; :: thesis: alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
set r = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>;
set n = dim p;
A1: len <*((- 1) |^ (dim p))*> = 1 by FINSEQ_1:39;
A2: len (alternating-proper-f-vector p) = dim p by Def27;
A3: len (alternating-f-vector p) = (dim p) + 2 by Def26;
A4: for k being Nat st 1 <= k & k <= len (alternating-f-vector p) holds
(alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (alternating-f-vector p) implies (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k )
assume A5: ( 1 <= k & k <= len (alternating-f-vector p) ) ; :: thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k

per cases ( k = 1 or k = (dim p) + 2 or ( 1 < k & k < (dim p) + 2 ) ) by A3, A5, XXREAL_0:1;

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

reconsider o = 1 as Nat ;
( 1 <= (dim p) + 2 & o - 2 = - 1 ) by Th10;
then A7: (alternating-f-vector p) . o = ((- 1) |^ o) * (num-polytopes (p,(- 1))) by Def26;
( (- 1) |^ 1 = - 1 & num-polytopes (p,(- 1)) = 1 ) by Th28;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A6, A7, Th15; :: thesis: verum

end;

suppose A8: k = (dim p) + 2 ; :: thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k

len <*(- 1)*> = 1 by FINSEQ_1:39;
then k = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + 1 by A2, A8;
then A9: ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (- 1) |^ (dim p) by Th16
.= (- 1) |^ k by A8, Th12 ;
1 <= k by A8, Th10;
then A10: (alternating-f-vector p) . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) by A8, Def26;
num-polytopes (p,(k - 2)) = 1 by A8, Th29;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A10, A9; :: thesis: verum

end;

suppose A11: ( 1 < k & k < (dim p) + 2 ) ; :: thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k

set m = k - 1;
A12: ( (k + 1) - 1 = k & ((dim p) + 2) - 1 = (dim p) + 1 ) ;
A13: k + 1 <= (dim p) + 2 by A11, INT_1:7;
len (<*(- 1)*> ^ (alternating-proper-f-vector p)) = (len <*(- 1)*>) + (len (alternating-proper-f-vector p)) by FINSEQ_1:22
.= (dim p) + 1 by A2, FINSEQ_1:39 ;
then ( len <*(- 1)*> = 1 & k <= len (<*(- 1)*> ^ (alternating-proper-f-vector p)) ) by A13, A12, FINSEQ_1:39, XREAL_1:9;
then ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (alternating-proper-f-vector p) . (k - 1) by A11, Th17;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A11, Th78; :: thesis: verum

end;

end;

end;

( len ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + (len <*((- 1) |^ (dim p))*>) & len <*(- 1)*> = 1 ) by Th14, FINSEQ_1:39;
hence alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by A3, A2, A1, A4; :: thesis: verum