deffunc H₁( Nat) -> Element of INT = In ((((- 1) |^ $1) * (num-polytopes (p,($1 - 2)))),INT);
consider s being FinSequence of INT such that
A1: len s = (dim p) + 2 and
A2: for j being Nat st j in dom s holds
s . j = H₁(j) from FINSEQ_2:sch 1();
take s ; :: thesis: ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )
for j being Nat st 1 <= j & j <= (dim p) + 2 holds
s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2)))

proof

let j be Nat; :: thesis: ( 1 <= j & j <= (dim p) + 2 implies s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2))) )
assume ( 1 <= j & j <= (dim p) + 2 ) ; :: thesis: s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2)))
then j in dom s by A1, FINSEQ_3:25;
then s . j = H₁(j) by A2;
hence s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2))) ; :: thesis: verum

end;

hence ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) ) by A1; :: thesis: verum