:: deftheorem defines uniquely-decomposable MONOID_0:def 9 :
for D being non empty set
for IT being BinOp of D holds
( IT is uniquely-decomposable iff ( IT is having_a_unity & ( for a, b being Element of D st IT . (a,b) = the_unity_wrt IT holds
( a = b & b = the_unity_wrt IT ) ) ) );