A D554: Binary operation $f : X \times X \to Y$ is an unsigned basic binary operation on $X$ if and only if \begin{equation} Y \subseteq [0, \infty] \end{equation}