:: deftheorem defines emb POLYNOM8:def 1 :
for L being non empty well-unital doubleLoopStr
for m being Element of NAT holds emb (m,L) = m * (1. L);