theorem Th8: :: E_TRANS2:8

for i, n being Nat holds len (~ ((tau i) |^ n)) = n + 1