[proofplan] We use the defining representation of a formal [power series](/page/Power%20Series) by its coefficient sequence. Write $A(X)$ and $B(X)$ with coefficients $a_n,b_n\in R$. Equality in $R[[X]]$ is equality of the underlying coefficient sequences, while $[X^n]$ extracts the $n$th coefficient, so the two implications are exactly the two directions of this extensionality principle. [/proofplan] [step:Write both series in terms of their coefficient sequences] Since $A(X),B(X)\in R[[X]]$, there exist uniquely determined sequences $(a_n)_{n\geq 0}$ and $(b_n)_{n\geq 0}$ in $R$ such that \begin{align*} A(X)=\sum_{n=0}^{\infty}a_nX^n \end{align*} and \begin{align*} B(X)=\sum_{n=0}^{\infty}b_nX^n. \end{align*} By the definition of coefficient extraction for formal power series, for every integer $n\geq 0$, \begin{align*} [X^n]A(X)=a_n \end{align*} and \begin{align*} [X^n]B(X)=b_n. \end{align*} [/step] [step:Extract coefficients from an equality of formal power series] Assume $A(X)=B(X)$ in $R[[X]]$. Equality of formal power series means equality of their coefficient sequences. Hence, for every integer $n\geq 0$, we have $a_n=b_n$. Using the coefficient identities from the previous step gives \begin{align*} [X^n]A(X)=[X^n]B(X). \end{align*} [/step] [step:Recover equality of formal power series from equality of all coefficients] Conversely, assume that for every integer $n\geq 0$, \begin{align*} [X^n]A(X)=[X^n]B(X). \end{align*} Using $[X^n]A(X)=a_n$ and $[X^n]B(X)=b_n$, this gives $a_n=b_n$ for every integer $n\geq 0$. Therefore the coefficient sequences $(a_n)_{n\geq 0}$ and $(b_n)_{n\geq 0}$ are equal, so by the definition of equality in $R[[X]]$, \begin{align*} A(X)=B(X). \end{align*} [guided] We now prove the converse carefully, because this is the direction where the formal nature of $R[[X]]$ matters. The hypothesis says that every coefficient extracted from $A(X)$ agrees with the corresponding coefficient extracted from $B(X)$: \begin{align*} [X^n]A(X)=[X^n]B(X) \end{align*} for every integer $n\geq 0$. From the coefficient representations already fixed, the symbol $[X^n]A(X)$ denotes the $n$th coefficient of $A(X)$, namely $a_n$, and $[X^n]B(X)$ denotes the $n$th coefficient of $B(X)$, namely $b_n$. Substituting these definitions into the displayed equality gives \begin{align*} a_n=b_n \end{align*} for every integer $n\geq 0$. A formal power series is determined by its entire coefficient sequence: two elements of $R[[X]]$ are equal exactly when their coefficients agree at every nonnegative degree. Since the coefficient sequence of $A(X)$ is $(a_n)_{n\geq 0}$ and the coefficient sequence of $B(X)$ is $(b_n)_{n\geq 0}$, the equality $a_n=b_n$ for all $n\geq 0$ implies equality of the two formal power series: \begin{align*} A(X)=B(X). \end{align*} [/guided] [/step]