The one-parameter formal-series ring is complete, separated, and has residue field $k$

Define $c_0(f)$ to be the coefficient of $h^0$. By [F1], $c_0(fg)=c_0(f)c_0(g)$, while coefficientwise addition preserves sums; the constant-series map $k\to R$ is a right inverse, so $c_0$ is a surjective ring homomorphism. If $c_0(f)=0$, define $g_n=f_{n+1}$; then $f=hg$, so $\ker c_0\subseteq hR$. Conversely every multiple of $h$ has zero constant coefficient by the product formula. Hence $\ker c_0=hR$, and the induced map $R\mathrm{/}hR\to k$ is a bijective ring homomorphism.

If $f,g\in R$ are nonzero, let $r$ and $s$ be their least indices with nonzero coefficients. In the convolution for the coefficient of $h^{r+s}$ in $fg$, every summand except the pair $(r,s)$ vanishes: a nonzero summand would require $i\ge r$, $j\ge s$, and $i+j=r+s$. The remaining coefficient is $f_r{g}_s\mathrm{\ne }0$ by [F3]. Also $1_R\mathrm{\ne }{0}_R$ because their constant coefficients are $1_k$ and $0_k$. Thus [F2] and [F4] show that $R$ is an integral domain.

A series lies in $h^{n}R$ exactly when its coefficients of degrees $0,\dots ,n-1$ vanish: one direction follows from multiplication by $h^n$, and the converse follows by shifting coefficients down by $n$. Therefore an $h$-adically Cauchy sequence $(f_j)$ has, for each $r\ge 0$, an eventually constant coefficient of $h^r$; define $f_r$ to be that unique eventual value and let $f={\sum }_{r\ge 0}{f}_r{h}^r$. For any $n$, the Cauchy condition makes the first $n$ coefficients of $f_j$ agree with those of $f$ for all sufficiently large $j$, so $f_j-f\in h^{n}R$ eventually. This proves completeness. If $f\in {\bigcap }_{n\ge 0}{h}^{n}R$, every coefficient of $f$ vanishes, so $f=0$; this proves separatedness. Applying the same construction to each of the finitely many standard coordinates of [F6] proves the assertion for every finite free $R$-module.

By step 1.2, $R$ is an integral domain, so [F5] applies: $K=\mathrm{Frac}(R)$ is a field and the canonical map $R\to K$ is injective.