A regular sequence lowers dimension exactly in a Cohen-Macaulay local ring

[base] The empty sequence gives the original ring, so the assertion holds for $i=0$.

Suppose $x\in \mathfrak{m}$ is regular on a nonzero Cohen–Macaulay Noetherian local ring $C$ of dimension $c$. The quotient $C\mathrm{/}xC$ is nonzero by regularity. Every chain of primes of $C\mathrm{/}xC$ lifts to a chain ${\mathfrak{q}}_0⊊\cdots ⊊{\mathfrak{q}}_e$ of primes of $C$ containing $x$. Choose a minimal prime $\mathfrak{a}\subseteq {\mathfrak{q}}_0$. Since $x$ is a nonzerodivisor, [F1] gives $x\mathrm{\notin }\mathfrak{a}$, so $\mathfrak{a}⊊{\mathfrak{q}}_0$. The lifted chain therefore extends to one of length $e+1$ in $C$, yielding $\dim (C\mathrm{/}xC)\le c-1$.

By [F2], $\mathrm{depth}(C\mathrm{/}xC)=\mathrm{depth}C-1=c-1$. Depth is at most dimension, so step 1.2 forces $\dim (C\mathrm{/}xC)=c-1$. Hence the quotient is Cohen–Macaulay. This is the one-element dimension-drop claim.

[IH] Assume the conclusion for length $i-1$. Then $C=A\mathrm{/}(f_1,\dots ,f_{i-1})$ is nonzero Cohen–Macaulay of dimension $h-i+1$. The regular-sequence convention makes $f_i$ regular on $C$, so step 2.1 applied to $C$ makes $C\mathrm{/}{f}_{i}C$ Cohen–Macaulay of dimension $h-i$. In particular $i\le h$.

[discharge-induction: step 3.1] The base and induction steps prove all lengths. AC is inherited at the associated-prime and depth boundaries; each individual iteration is finite.