:: deftheorem defines unital_poly UNIROOTS:def 4 :
for n being non zero Nat
for L being non empty left_unital doubleLoopStr holds unital_poly (L,n) = ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L));