theorem :: FIELD_15:46

for R being non degenerated unital doubleLoopStr
for n being non zero Nat
for a being Element of R holds deg (X^ (n,a)) = n by Lm12;