let i be Nat; :: thesis: for k being non zero Nat holds tau i divides (tau i) |^ k
let k be non zero Nat; :: thesis: tau i divides (tau i) |^ k
(k - 1) + 1 = k ;
then (tau i) |^ k = ((tau i) |^ 1) * ((tau i) |^ (k - 1)) by BINOM:10
.= (tau i) * ((tau i) |^ (k - 1)) by BINOM:8 ;
hence tau i divides (tau i) |^ k by GCD_1:def 1; :: thesis: verum