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