:: deftheorem defines 1_ POLYNOM1:def 9 :
for n being set
for L being non empty right_unital multLoopStr_0 holds 1_ (n,L) = (0_ (n,L)) +* ((EmptyBag n),(1. L));