Units of a Monoid

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(M,\cdot)$ be a monoid with identity $e$, with products written $uv$ as in Semigroups (i).

(i) Units. An element $u\in M$ is a unit if there is $v\in M$ with

$$uv=vu=e;$$

each such $v$ is an inverse of $u$.

(ii) The set of units. The set of units of $M$ is

$$M^{\times}=\{u\in M: u\text{ is a unit}\}$$

(a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)).