Let $f: X\to S$ be a smooth morphism of schemes. Let $p$ be a section. Let $\hat{\mathscr{O}}_{X, p(S)}$ be the completion $X$ along $p(S)$. Then I think for every point $s\in S$, there exists an open neighborhood $ U=Spec R$ of $s$, such that $\hat{\mathscr{O}}_{X, p(S)} (U)$ is a formal power series over $R$. How it should be proved? Or where can I find the reference? Thanks.