Relator root versus proper power

The symmetrised set is exactly $\{a^7,a^{-7}\}$. Its two words start in different letters, so have no nonempty common prefix; equal positive rotations all give the first word and equal inverse rotations the second. Thus there are no pieces and $C^{\mathrm{\prime }}(1\mathrm{/}6)$ holds vacuously by [F1]. The one-letter word $a$ cannot be a proper power of a nonempty shorter word, so it is a root by [F2].

Every one-generator word freely reduces to $a^j$ for an integer $j$, since any change of sign in the string creates an adjacent inverse pair. The relation $a^7=1$ reduces the exponent modulo seven, so every element is one of $1,a,\dots ,a^6$. The exponent sum modulo seven is unchanged by free cancellation and by inserting or deleting any conjugate of $a^{\pm 7}$: the conjugating exponents cancel and the relator contributes a multiple of seven. It therefore defines a homomorphism from the quotient to the additive residues modulo seven, taking $a^j$ to the residue of $j$.

The seven displayed elements have distinct images, so they are distinct; step 1.2 also proves that they exhaust the quotient. In particular $a^7=1$ and $a^j\mathrm{\ne }1$ for $1\le j\le 6$. This proves exact order seven, while keeping the literal word root $a$ distinct from its quotient image.