:: deftheorem defines * BINOM:def 6 :
for R being non empty addLoopStr
for a being Element of R
for n being Nat holds a * n = (Nat-mult-right R) . (a,n);