:: deftheorem defines 1_. POLYNOM3:def 8 :
for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L));