:: deftheorem Def20 defines uniquely-decomposable MONOID_0:def 20 :
for IT being non empty multMagma holds
( IT is uniquely-decomposable iff the multF of IT is uniquely-decomposable );