$S{\otimes }_{R}R[x]\cong S[x]$ as $S$-algebras

The displayed coefficient formula is additive in both variables and satisfies $F(sf(r)\otimes p)=F(s\otimes rp)$, so it is $R$-balanced. It therefore induces an additive map $F:S{\otimes }_{R}R[x]\to S[x]$ by [L3].

Define $G:S[x]\to S{\otimes }_{R}R[x]$ by $G({\sum }_i{s}_i{x}^i)={\sum }_i{s}_i\otimes x^i$. The sum is finite by [L2]. Coefficientwise addition and convolution multiplication show that $G$ is an $S$-algebra homomorphism, using $(s\otimes x^i)(t\otimes x^j)=st\otimes x^{i+j}$ from [L4].

The map $F$ is $S$-linear, sends $1\otimes 1$ to $1$, and, using [L2] and [L4], satisfies $F((s\otimes p)(t\otimes q))=F(st\otimes pq)=F(s\otimes p)F(t\otimes q)$. Hence it is an $S$-algebra homomorphism.

For every polynomial ${\sum }_i{s}_i{x}^i$, one has $F(G({\sum }_i{s}_i{x}^i))={\sum }_i{s}_i{x}^i$. For an elementary tensor, balance gives $G(F(s\otimes {\sum }_i{r}_i{x}^i))={\sum }_{i}sf(r_i)\otimes x^i={\sum }_{i}s\otimes r_i{x}^i=s\otimes {\sum }_i{r}_i{x}^i$.

The two maps $GF$ and the identity induce the same balanced pairing by step 2.2, so uniqueness in [L3] makes them equal; step 2.2 already gives $FG=1$ coefficientwise. Thus $F$ and $G$ are inverse $S$-algebra homomorphisms.