Every permutation of a finite set is a product of pairwise disjoint cycles, uniquely up to reordering and cyclic rotation

The evaluation rule is an action by the Given, and [L3] identifies its orbit at $x$ as $\{\sigma^r(x):r\in\mathbb Z\}$; by [L2] these orbits partition $X$.

Fix an orbit $O$. Since $O$ is finite, the sequence $x,\sigma(x),\sigma^2(x),\ldots$ first repeats; bijectivity of $\sigma$ makes the first repeated value $x$. If the least positive return time is $d$, then $O=\{x,\sigma(x),\ldots,\sigma^{d-1}(x)\}$ and $\sigma$ restricts to the cycle $(x\,\sigma(x)\,\ldots\,\sigma^{d-1}(x))$; when $d=1$, $x$ is fixed.

The cycles obtained from the non-singleton orbits have pairwise disjoint supports, and their product agrees with $\sigma$ on each orbit and fixes every singleton orbit. Their product is therefore $\sigma$; if every orbit is a singleton, this is the empty product.

In any disjoint-cycle decomposition of $\sigma$, [L4] allows powers to be taken factor by factor, while every factor except the unique one supporting a given point fixes that point. Thus successive powers of $\sigma$ move the point exactly around that factor's support, so the support is the point's intrinsic $\langle\sigma\rangle$-orbit. Hence the factor supports are forced, and the cycle on each support is forced up to its starting point, which is cyclic rotation; only the order of the disjoint factors remains free.