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=\operatorname{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.