let s, t be FinSequence of INT ; :: 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))) ) & len t = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
t . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) implies s = t )
assume that
A4: len s = (dim p) + 2 and
A5: for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) and
A6: len t = (dim p) + 2 and
A7: for k being Nat st 1 <= k & k <= (dim p) + 2 holds
t . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ; :: thesis: s = t
for k being Nat st 1 <= k & k <= len s holds
s . k = t . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len s implies s . k = t . k )
assume A8: ( 1 <= k & k <= len s ) ; :: thesis: s . k = t . k
reconsider k = k as Nat ;
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) by A4, A5, A8;
hence s . k = t . k by A4, A7, A8; :: thesis: verum

end;

hence s = t by A4, A6, FINSEQ_1:14; :: thesis: verum