let i, n be Nat; :: thesis: len (~ ((tau i) |^ n)) = n + 1
~ ((tau i) |^ n) = <%(In ((- i),INT.Ring)),(1. INT.Ring)%> `^ n by BINOM:def 2;
hence len (~ ((tau i) |^ n)) = n + 1 by UPROOTS:39; :: thesis: verum