theorem :: RING_5:43

for n being Nat
for R being non degenerated unital doubleLoopStr holds deg (npoly (R,n)) = n by lem6;