theorem :: FIELD_16:31

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