:: deftheorem Def4 defines Nat-mult-right BINOM:def 4 :
for R being non empty addLoopStr
for b₂ being Function of [: the carrier of R,NAT:], the carrier of R holds
( b₂ = Nat-mult-right R iff for a being Element of R holds
( b₂ . (a,0) = 0. R & ( for n being Element of NAT holds b₂ . (a,(n + 1)) = (b₂ . (a,n)) + a ) ) );