Well-defined formal power series

307 Views Asked by At

I am working on the following problem:

Assume we are working in a formal power series ring $R[[x]]$ over a ring $R$ containing $\mathbb{Q}$. Define $\exp(x)$ and $\log(1 + x)$ by their usual Taylor series. Given $F(x), G(x) \in R[[x]]$ such that $F(0) = 1$, show that there is a well-defined formal power series \begin{equation} F(x)^{G(x)} \overset{def}{=} \exp(G(x) \log F(x)). \end{equation} What I think is the following: Given that $H(x) = G(x)\log F(x)$ makes sense as a formal power series (multiplication of formal power series is always valid), so I just need to prove that the composition of $H(x)$ and $\exp(x)$, as formal power series, makes sense, i.e. $H(0) = 0$. Am I right or am I missing something else?