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 (alternating-f-vector p) = (dim p) + 2 by Def26;
A2: len (alternating-proper-f-vector p) = dim p by Def27;
A3: len ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + (len <*((- 1) |^ (dim p))*>) by Th16;
A4: len <*(- 1)*> = 1 by FINSEQ_1:56;
A5: len <*((- 1) |^ (dim p))*> = 1 by FINSEQ_1:56;
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 that
A6: 1 <= k and
A7: 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 A1, A6, A7, XXREAL_0:1;

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

A9: 1 <= (dim p) + 2 by Th12;
reconsider o = 1 as Nat ;
o - 2 = - 1 ;
then A10: (alternating-f-vector p) . o = ((- 1) |^ o) * (num-polytopes p,(- 1)) by A9, Def26;
A11: (- 1) |^ 1 = - 1 by Th4, Th9;
num-polytopes p,(- 1) = 1 by Th31;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A8, A10, A11, Th17; :: thesis: verum

end;

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

then 1 <= k by Th12;
then A13: (alternating-f-vector p) . k = ((- 1) |^ k) * (num-polytopes p,(k - 2)) by A12, Def26;
A14: ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (- 1) |^ k

proof

k = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + 1

proof

len <*(- 1)*> = 1 by FINSEQ_1:56;
hence k = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + 1 by A2, A12; :: thesis: verum

end;

then ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (- 1) |^ (dim p) by Th18
.= (- 1) |^ k by A12, Th14 ;
hence ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (- 1) |^ k ; :: thesis: verum

end;

num-polytopes p,(k - 2) = 1 by A12, Th32;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A13, A14; :: thesis: verum

end;

suppose A15: ( 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;
A16: len <*(- 1)*> = 1 by FINSEQ_1:56;
k <= len (<*(- 1)*> ^ (alternating-proper-f-vector p))

proof

A17: len (<*(- 1)*> ^ (alternating-proper-f-vector p)) = (len <*(- 1)*>) + (len (alternating-proper-f-vector p)) by FINSEQ_1:35
.= (dim p) + 1 by A2, FINSEQ_1:56 ;
A18: k + 1 <= (dim p) + 2 by A15, INT_1:20;
A19: (k + 1) - 1 = k ;
((dim p) + 2) - 1 = (dim p) + 1 ;
hence k <= len (<*(- 1)*> ^ (alternating-proper-f-vector p)) by A17, A18, A19, XREAL_1:11; :: thesis: verum

end;

then ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (alternating-proper-f-vector p) . (k - 1) by A15, A16, Th19;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A15, Th81; :: thesis: verum

end;

end;

end;

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