[proofplan] We use the standard construction of $R[x]$ as finitely supported coefficient sequences indexed by non-negative integers. Addition is coefficientwise, so finite support and the additive group axioms follow directly from the corresponding facts in $R$. Multiplication is finite convolution; finite support is preserved because degrees add, and the ring axioms follow by comparing coefficients and using associativity, commutativity, distributivity, and the identity element in $R$. [/proofplan] [step:Represent polynomials as finitely supported coefficient sequences] Let $0_R$ denote the additive identity of $R$. Define $\mathbb{N}_0 := \mathbb{N} \cup \{0\}$. In the standard construction, an element $p \in R[x]$ is a function \begin{align*} a: \mathbb{N}_0 \to R \end{align*} with finite support, where the support is the finite set \begin{align*} \operatorname{supp}(a) := \{i \in \mathbb{N}_0 : a(i) \ne 0_R\}. \end{align*} Since $a$ has finite support, choose $m \in \mathbb{N}_0$ such that $a_i=0_R$ for all $i>m$, where $a_i := a(i)$. We write this polynomial as \begin{align*} p=\sum_{i=0}^{m} a_i x^i. \end{align*} Similarly, if $q \in R[x]$ has coefficient function $b:\mathbb{N}_0 \to R$, choose $n \in \mathbb{N}_0$ such that $b_j=0_R$ for all $j>n$, and write \begin{align*} q=\sum_{j=0}^{n} b_j x^j. \end{align*} [/step] [step:Show coefficientwise addition preserves finite support] Define the sum $p+q$ by the coefficient function \begin{align*} c: \mathbb{N}_0 \to R,\qquad c_k:=a_k+b_k. \end{align*} If $k>\max\{m,n\}$, then $a_k=0_R$ and $b_k=0_R$, hence \begin{align*} c_k=0_R+0_R=0_R. \end{align*} Therefore $\operatorname{supp}(c)\subseteq \{0,\dots,\max\{m,n\}\}$, so $c$ has finite support and $p+q\in R[x]$. [/step] [step:Show convolution multiplication preserves finite support] Define the product $pq$ by the coefficient function \begin{align*} d: \mathbb{N}_0 \to R,\qquad d_k:=\sum_{i+j=k} a_i b_j. \end{align*} For each fixed $k\in\mathbb{N}_0$, the sum is finite because there are only $k+1$ pairs $(i,j)\in\mathbb{N}_0^2$ with $i+j=k$. If $k>m+n$ and $i+j=k$, then either $i>m$ or $j>n$; otherwise $i\le m$ and $j\le n$ would imply $k=i+j\le m+n$. Hence every summand $a_i b_j$ is $0_R$, so \begin{align*} d_k=0_R. \end{align*} Thus $\operatorname{supp}(d)\subseteq \{0,\dots,m+n\}$, so $d$ has finite support and $pq\in R[x]$. [/step] [step:Verify the additive group axioms coefficientwise] Let $r\in R[x]$ be the polynomial with coefficient function $e:\mathbb{N}_0\to R$, written $e_k$ at index $k$. For every $k\in\mathbb{N}_0$, associativity and commutativity of addition in $R$ give \begin{align*} (a_k+b_k)+e_k=a_k+(b_k+e_k) \end{align*} and \begin{align*} a_k+b_k=b_k+a_k. \end{align*} Therefore polynomial addition is associative and commutative. The zero polynomial is the finitely supported function $0:\mathbb{N}_0\to R$ defined by $0_k=0_R$ for every $k$, and it satisfies \begin{align*} a_k+0_k=a_k. \end{align*} The additive inverse of $p$ has coefficient function $k\mapsto -a_k$. It is finitely supported because if $a_k=0_R$, then $-a_k=0_R$, so its support is contained in $\operatorname{supp}(a)$. For every $k\in\mathbb{N}_0$, \begin{align*} a_k+(-a_k)=0_R. \end{align*} Hence $(R[x],+)$ is an abelian group. [/step] [step:Verify associativity and distributivity of multiplication by comparing coefficients] Two polynomials in the finite-support construction are equal exactly when their coefficient functions agree at every index $k\in\mathbb{N}_0$. Let $r\in R[x]$ have coefficient function $e:\mathbb{N}_0\to R$. For each $k\in\mathbb{N}_0$, the coefficient of $(pq)r$ at $x^k$ is \begin{align*} \sum_{u+v=k}\left(\sum_{i+j=u}a_i b_j\right)e_v. \end{align*} By distributivity and associativity in $R$, and because all sums are finite, this equals the finite sum over all triples $(i,j,v)\in\mathbb{N}_0^3$ satisfying $i+j+v=k$: \begin{align*} \sum_{i+j+v=k} a_i b_j e_v. \end{align*} The coefficient of $p(qr)$ at $x^k$ is \begin{align*} \sum_{i+w=k}a_i\left(\sum_{j+v=w}b_j e_v\right), \end{align*} which is the same finite sum \begin{align*} \sum_{i+j+v=k} a_i b_j e_v. \end{align*} Thus $(pq)r=p(qr)$. For distributivity, the coefficient of $p(q+r)$ at $x^k$ is \begin{align*} \sum_{i+j=k}a_i(b_j+e_j). \end{align*} Using distributivity in $R$, this equals \begin{align*} \sum_{i+j=k}a_i b_j+\sum_{i+j=k}a_i e_j, \end{align*} which is the coefficient of $pq+pr$ at $x^k$. Hence $p(q+r)=pq+pr$. The proof of $(p+q)r=pr+qr$ is identical, using right distributivity in $R$. [guided] We prove the multiplicative laws by reducing them to statements about each coefficient. This is valid because two polynomials in the finite-support construction are equal exactly when their coefficient functions agree at every index $k\in\mathbb{N}_0$. Let $r\in R[x]$ have coefficient function $e:\mathbb{N}_0\to R$. Fix $k\in\mathbb{N}_0$. The coefficient of $(pq)r$ at $x^k$ is obtained by first multiplying $p$ and $q$, then multiplying the result by $r$: \begin{align*} \sum_{u+v=k}\left(\sum_{i+j=u}a_i b_j\right)e_v. \end{align*} Every sum here is finite, since each equation such as $u+v=k$ has only finitely many solutions in $\mathbb{N}_0^2$. Therefore we may expand the finite sums using distributivity in $R$. The condition $u+v=k$ together with $i+j=u$ is equivalent to the single condition $i+j+v=k$, so the coefficient becomes \begin{align*} \sum_{i+j+v=k} a_i b_j e_v. \end{align*} Now compute the coefficient of $p(qr)$ at $x^k$. First multiplying $q$ and $r$ gives the inner convolution, and then multiplying by $p$ gives \begin{align*} \sum_{i+w=k}a_i\left(\sum_{j+v=w}b_j e_v\right). \end{align*} Again, by distributivity and associativity in $R$, this expands to the finite sum over triples satisfying $i+j+v=k$: \begin{align*} \sum_{i+j+v=k} a_i b_j e_v. \end{align*} The coefficient at every index $k$ is the same for $(pq)r$ and $p(qr)$, so $(pq)r=p(qr)$. For distributivity, fix $k\in\mathbb{N}_0$ again. The coefficient of $p(q+r)$ at $x^k$ is \begin{align*} \sum_{i+j=k}a_i(b_j+e_j). \end{align*} Applying distributivity in $R$ to each summand gives \begin{align*} \sum_{i+j=k}(a_i b_j+a_i e_j). \end{align*} Splitting this finite sum gives \begin{align*} \sum_{i+j=k}a_i b_j+\sum_{i+j=k}a_i e_j. \end{align*} This is exactly the coefficient of $pq+pr$ at $x^k$. Since this holds for every $k\in\mathbb{N}_0$, we have $p(q+r)=pq+pr$. The identity $(p+q)r=pr+qr$ follows by the same coefficient computation, using the distributive law $(a_i+b_i)e_j=a_i e_j+b_i e_j$ in $R$. [/guided] [/step] [step:Identify the multiplicative identity and prove commutativity] Define the constant polynomial $1_{R[x]}$ by the coefficient function $\varepsilon:\mathbb{N}_0\to R$ with $\varepsilon_0=1_R$ and $\varepsilon_k=0_R$ for all $k\ge 1$. For every $k\in\mathbb{N}_0$, the coefficient of $1_{R[x]}p$ at $x^k$ is \begin{align*} \sum_{i+j=k}\varepsilon_i a_j. \end{align*} All summands vanish except the term with $i=0$ and $j=k$, so this coefficient is \begin{align*} 1_R a_k=a_k. \end{align*} Thus $1_{R[x]}p=p$. The same computation using $a_k1_R=a_k$ gives $p1_{R[x]}=p$. Finally, for every $k\in\mathbb{N}_0$, the coefficient of $pq$ at $x^k$ is \begin{align*} \sum_{i+j=k}a_i b_j. \end{align*} Since $R$ is commutative, $a_i b_j=b_j a_i$ for every pair $(i,j)$, and exchanging the names of the indices gives \begin{align*} \sum_{i+j=k}a_i b_j=\sum_{j+i=k}b_j a_i. \end{align*} The right-hand side is the coefficient of $qp$ at $x^k$. Hence $pq=qp$. The closure of addition and multiplication, the additive abelian group structure, associativity and distributivity of multiplication, the multiplicative identity, and commutativity of multiplication together show that $R[x]$ is a commutative ring with identity. [/step]