$\mathbb{R}((t^{-1}))$ is a field: every nonzero formal Laurent series is invertible

Define $u : \mathbb{Z} \to \mathbb{R}$ by $u(j) := -c^{-1} f(p + j)$ for $j \ge 1$ and $u(j) := 0$ for $j \le 0$. Then $u$ vanishes at every index $< 1$, so its support is bounded below and $u \in K$.

By [L5] with $A = K$, $a = 1_K$ and $F(h) = hu$ there is a family $(u^{n})_{n \in \mathbb{N}}$ in $K$ with $u^{0} = 1_K$ and $u^{\sigma(n)} = u^{n} u$.

For every $k \in \mathbb{Z}$, $\bigl(\iota(c)\,t^{-p}\,(1_K - u)\bigr)(k) = c\,(1_K - u)(k - p)$ by [L2]; this is $0$ when $k < p$ because $1_K - u$ vanishes at every negative index, it is $c$ when $k = p$, and it is $c \cdot \bigl(-u(k-p)\bigr) = c c^{-1} f(k) = f(k)$ when $k > p$. Comparing with $f(k) = 0$ for $k < p$ and $f(p) = c$, we get $f = \iota(c)\, t^{-p}\,(1_K - u)$.

For every $n \in \mathbb{N}$, $u^{n}$ vanishes at every index $< n$: at $n = 0$ this says $1_K$ vanishes at every negative index, which holds by [L1]; and if $u^{n}$ vanishes at every index $< n$ then, since $u$ vanishes at every index $< 1$ by [step 1.1], the product $u^{\sigma(n)} = u^{n}u$ vanishes at every index $< n + 1$ by [L2].

Define $g : \mathbb{Z} \to \mathbb{R}$ by $g(k) := \sum_{n=0}^{k} (u^{n})(k)$ for $k \ge 0$ and $g(k) := 0$ for $k < 0$; each value is a finite sum of reals, and $g$ vanishes at every index $< 0$, so $g \in K$.

Fix $k \ge 1$. In $(ug)(k) = \sum_{i+j=k} u(i)g(j)$ a term can be nonzero only when $i \ge 1$ and $j \ge 0$, hence only for $1 \le i \le k$ and $j = k - i$; so $(ug)(k) = \sum_{i=1}^{k} u(i)\, g(k-i) = \sum_{i=1}^{k} u(i) \sum_{n=0}^{k-i} (u^{n})(k-i)$.

For $k \le 0$ one has $(ug)(k) = 0$, since $u$ vanishes at every index $< 1$ and $g$ at every index $< 0$, so every pair $(i,j)$ with $i + j = k$ has $u(i)g(j) = 0$.

In the inner sum of [step 4.1] the terms with $k - i < n \le k-1$ vanish by [step 2.2], so the inner sum may be extended to $n = 0, \dots, k-1$ without changing its value; interchanging the two finite sums gives $(ug)(k) = \sum_{n=0}^{k-1} \sum_{i=1}^{k} u(i)\,(u^{n})(k-i)$.

For each $n$, $\sum_{i=1}^{k} u(i)(u^{n})(k-i) = \sum_{i+j=k} u(i)(u^{n})(j) = (u\,u^{n})(k) = (u^{\sigma(n)})(k)$, because a term of the full convolution can be nonzero only for $i \ge 1$ and $j \ge 0$; hence $(ug)(k) = \sum_{n=0}^{k-1} (u^{\sigma(n)})(k) = \sum_{n=1}^{k} (u^{n})(k)$ for every $k \ge 1$.

For $k \ge 1$, $\bigl((1_K - u)g\bigr)(k) = g(k) - (ug)(k) = \sum_{n=0}^{k}(u^{n})(k) - \sum_{n=1}^{k}(u^{n})(k) = (u^{0})(k) = 1_K(k)$; for $k = 0$, $g(0) = (u^{0})(0) = 1$ and $(ug)(0) = 0$, so the value is $1 = 1_K(0)$; and for $k < 0$ both $g(k)$ and $(ug)(k)$ are $0$, as is $1_K(k)$. Hence $(1_K - u)g = 1_K$.

Using [step 2.1], [L2] and $cc^{-1} = 1$, one computes $f \cdot \bigl(\iota(c^{-1})\,t^{p}\,g\bigr) = \iota(c)\iota(c^{-1})\, t^{-p}t^{-(-p)}\,(1_K - u)g = 1_K \cdot 1_K \cdot 1_K = 1_K$, so $\iota(c^{-1}) t^{p} g \in K$ is a multiplicative inverse of $f$.

$K$ is a commutative ring with $1_K \ne 0_K$ by [L2], its nonzero elements are closed under multiplication by [L3], and by [step 8.1] every nonzero element has an inverse; so $K$ satisfies the field axioms of [L7] and the construction is complete.