for L being domRing
for p being Polynomial of L st len p <> 0 holds
for n being Nat holds len (p `^ n) = ((n * (len p)) - n) + 1