:: deftheorem defines npoly RING_5:def 3 :
for R being non empty unital doubleLoopStr
for n being Nat holds npoly (R,n) = (0_. R) +* ((0,n) --> ((1. R),(1. R)));