:: deftheorem Def34 defines *+^ MONOID_0:def 34 :
for D being non empty set
for b₂ being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma holds
( b₂ = D *+^ iff ( the carrier of b₂ = D * & ( for p, q being Element of b₂ holds p [*] q = p ^ q ) ) );