Positive Powers Of A Regular Sequence Remain Regular

First let $x,y_1,\dots ,y_s$ be regular on a module $N$. Injectivity of $x$ implies injectivity of every $x^a$. For $a\ge 2$, multiplication by $x^{a-1}$ gives the exact sequence $0\to N\mathrm{/}xN\to N\mathrm{/}{x}^{a}N\to N\mathrm{/}{x}^{a-1}N\to 0$. Indeed, if $x^{a-1}m\in x^{a}N$, cancellation by injectivity of $x^{a-1}$ gives $m\in xN$; the last map is the natural quotient.

If a sequence $y_1,\dots ,y_s$ is regular on both ends of a short exact sequence $0\to A\to B\to C\to 0$, it is regular on $B$: injectivity of $y_1$ follows by mapping a killed element to $C$ and then to $A$; because $y_1$ is injective on $C$, quotienting by $y_1$ preserves exactness, and the same argument repeats for $y_2,\dots ,y_s$. Apply this observation inductively to the exact sequences of step 1.1. The sequence $y_1,\dots ,y_s$ is regular on $N\mathrm{/}{x}^{a}N$ for every $a\ge 1$, and $x^a,y_1,\dots ,y_s$ is regular on $N$. Its terminal quotient surjects onto the original nonzero terminal quotient, so remains nonzero.

Under the assumed AC, Regular Sequences Permutable Local lets us move any selected $x_i$ to the front of the current regular sequence. Step 2.1 replaces it by $x_i^{a_i}$, and the same permutation result returns that powered entry to its original position. Repeat this finite operation for $i=1,\dots ,n$. Each intermediate sequence is regular, and the final sequence is $x_1^{a_1},\dots ,x_n^{a_n}$. These permutation applications are the exact uses of Choice.