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 and
A2: for j being Nat st j in dom s holds
s . j = H₁(j) from FINSEQ_2:sch 1();
A3: dom s = Seg (dim p) by A1, FINSEQ_1:def 3;
A4: for j being Nat st 1 <= j & j <= dim p holds
s . j = ((- 1) |^ (j + 1)) * (num-polytopes p,(j - 1))

proof

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

end;

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