:: deftheorem Def7 defines mult GROUP_1A:def 6 :
for G being non empty addMagma
for b₂ being Function of [:NAT, the carrier of G:], the carrier of G holds
( b₂ = mult G iff for h being Element of G holds
( b₂ . (0,h) = 0_ G & ( for n being Nat holds b₂ . ((n + 1),h) = (b₂ . (n,h)) + h ) ) );