for D being non empty set
for o being BinOp of D st o is uniquely-decomposable holds
o .:^2 is uniquely-decomposable