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
A3: len s = dim p and
A4: for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) and
A5: len t = dim p and
A6: 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 A7: ( 1 <= k & k <= len s ) ; :: thesis: s . k = t . k
reconsider k = k as Nat ;
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) by A3, A4, A7;
hence s . k = t . k by A3, A6, A7; :: thesis: verum
end;
hence s = t by A3, A5; :: thesis: verum