let s, t be FinSequence of INT ; :: 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)) ) & len t = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes p,(k - 1)) ) implies s = t )
assume that
A8: len s = dim p and
A9: for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes p,(k - 1)) and
A10: len t = dim p and
A11: for k being Nat st 1 <= k & k <= dim p holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes p,(k - 1)) ; :: 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 that
A12: 1 <= k and
A13: k <= len s ; :: thesis: s . k = t . k
reconsider k = k as Nat ;
s . k = ((- 1) |^ (k + 1)) * (num-polytopes p,(k - 1)) by A8, A9, A12, A13;
hence s . k = t . k by A8, A11, A12, A13; :: thesis: verum

end;

hence s = t by A8, A10, FINSEQ_1:18; :: thesis: verum