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),\dots$ first repeats; bijectivity of $\sigma$ makes the first repeated value $x$. If the least positive return time is $d$, then $O=\{x,\sigma (x),\dots ,{\sigma }^{d-1}(x)\}$ and $\sigma$ restricts to the cycle $(x\sigma (x)\dots {\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 $⟨\sigma ⟩$-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.