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