Group Actions

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(G,\cdot)$ be a group, let $e$ be its identity element, unique by Uniqueness of the Identity Element and of Inverses in a Group (i), and let $X$ be a set.

(i) Group action. An action of $G$ on $X$ is a function from $G\times X$ to $X$, whose value at $(g,x)$ is written $g\cdot x$, such that for all $g,h\in G$ and $x\in X$

$$e\cdot x=x\qquad\text{and}\qquad g\cdot(h\cdot x)=(g\cdot h)\cdot x.$$