deffunc H₁( Nat) -> Element of INT = ((- 1) |^ ($1 + 1)) * (num-polytopes p,($1 - 1));
consider s being FinSequence of INT such that
A1: len s = (dim p) + 1 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) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes p,(k - 1)) ) )
A3: dom s = Seg ((dim p) + 1) by A1, FINSEQ_1:def 3;
for j being Nat st 1 <= j & j <= (dim p) + 1 holds
s . j = ((- 1) |^ (j + 1)) * (num-polytopes p,(j - 1))

proof

let j be Nat; :: thesis: ( 1 <= j & j <= (dim p) + 1 implies s . j = ((- 1) |^ (j + 1)) * (num-polytopes p,(j - 1)) )
assume ( 1 <= j & j <= (dim p) + 1 ) ; :: thesis: s . j = ((- 1) |^ (j + 1)) * (num-polytopes p,(j - 1))
then j in Seg ((dim p) + 1) by FINSEQ_1:3;
hence s . j = ((- 1) |^ (j + 1)) * (num-polytopes p,(j - 1)) by A2, A3; :: thesis: verum

end;

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