$\mathbb{R}((t^{-1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below

Let $S\subseteq \mathbb{Z}$ be nonempty with $s\ge b$ for all $s\in S$. Every element of $T:=\{s-b:s\in S\}$ is a nonnegative integer, so by [L4] $T=\{\epsilon (a):a\in A\}$ for a nonempty $A\subseteq \mathbb{N}$; by [L3] $A$ has a least element $a_0$, and since $\epsilon$ preserves order and $x\mapsto x+b$ preserves order, $\epsilon (a_0)+b$ is an element of $S$ that is $\le$ every element of $S$.

Fix $k\in \mathbb{Z}$ and let $(i,j)\in S_k$. Then $f(i)\mathrm{\ne }0$ and $g(j)\mathrm{\ne }0$, so $i\ge m$ and $j\ge n$; from $i+j=k$ and $j\ge n$ we get $i=k-j\le k-n$. Hence $m\le i\le k-n$, and $j=k-i$ is determined by $i$.

The integers $i$ with $m\le i\le k-n$ are in order-preserving bijection with the naturals $a$ satisfying $\epsilon (a)\le k-n-m$ by [L4], and there are finitely many of these, none at all when $k-n-m<0$; so $S_k$ is a finite set by [step 1.2], it is empty whenever $k<m+n$, and therefore $(fg)(k)$ is a finite sum of reals which is $0$ whenever $k<m+n$.

$(f+g)(k)=f(k)+g(k)=0$ for every $k<\min (m,n)$ and $(-f)(k)=-f(k)=0$ for every $k<m$, so $f+g$ and $-f$ have support bounded below; and $(fg)(k)=0$ for every $k<m+n$ by [step 2.1], so $fg$ does too. All three therefore lie in $K$.

$(fg)(k)={\sum }_{i+j=k}f(i)g(j)={\sum }_{j+i=k}g(j)f(i)=(gf)(k)$, since the two sums have the same finite index set and their terms agree by commutativity of multiplication in $\mathbb{R}$; so multiplication on $K$ is commutative.

For $f,g,h\in K$ and $k\in \mathbb{Z}$, expanding both $((fg)h)(k)$ and $(f(gh))(k)$ by [L1] and [L5] gives the sum of $f(i)g(j)h(l)$ over the triples $(i,j,l)$ with $i+j+l=k$ and $f(i)g(j)h(l)\mathrm{\ne }0$; that set is finite because the argument of [step 1.2] bounds $i$, $j$ and $l$ from below and hence, as in [step 2.1], from above as well. So multiplication on $K$ is associative.

$(f(g+h))(k)={\sum }_{i+j=k}f(i)(g(j)+h(j))={\sum }_{i+j=k}f(i)g(j)+{\sum }_{i+j=k}f(i)h(j)=(fg)(k)+(fh)(k)$, all three sums being finite; so multiplication distributes over addition.

For $h\in K$, $(t^{-a}h)(k)={\sum }_{i+j=k}{t}^{-a}(i)h(j)$ has at most one nonzero term, the one with $i=a$ and $j=k-a$, so $(t^{-a}h)(k)=h(k-a)$; taking $h=t^{-b}$ gives $(t^{-a}{t}^{-b})(k)=t^{-b}(k-a)$, which is $1$ when $k=a+b$ and $0$ otherwise, that is, $t^{-a}{t}^{-b}=t^{-(a+b)}$.

$(\iota (c)f)(k)={\sum }_{i+j=k}\iota (c)(i)f(j)$ has at most one nonzero term, the one with $i=0$ and $j=k$, so $(\iota (c)f)(k)=cf(k)$.

$(f\cdot 1_K)(k)={\sum }_{i+j=k}f(i)1_K(j)$ has at most one nonzero term, the one with $j=0$ and $i=k$, so $(f\cdot 1_K)(k)=f(k)$ and $f\cdot 1_K=f$; moreover $1_K(0)=1\mathrm{\ne }0=0_K(0)$, so $1_K\mathrm{\ne }{0}_K$.

Addition on $K$ is defined index by index, and $K$ is closed under it and under negation by [step 3.1]; so associativity, commutativity, the law $f+0_K=f$ and the law $f+(-f)=0_K$ each hold at every index by the corresponding law in $\mathbb{R}$, and $(K,+,0_K)$ is an abelian group.

By [step 4.1] addition makes $K$ an abelian group, by [step 3.2], [step 3.3] and [step 3.7] multiplication is commutative and associative with identity $1_K\mathrm{\ne }{0}_K$, and by [step 3.4] it distributes over addition; hence $K$ is a commutative ring with identity.

Clause 1 is [step 2.1], clause 2 is [step 3.1] with [step 2.1], clause 3 is [step 5.1], clause 4 is [step 3.5] and [step 3.6], and clause 5 is [step 1.1] applied to $S=\mathrm{supp}f$, which is nonempty when $f\mathrm{\ne }{0}_K$ and bounded below because $f\in K$.