theorem :: FIELD_15:21

for R being domRing
for p being non zero Polynomial of R
for n being Nat holds deg (p `^ n) = n * (deg p) by t1;