$K$を体とし，$P$をその上の素因子とします．
$P$の$K$における付値環及び素イデアルを$\mathfrak{o}, \mathfrak{p}$とします．
$K$を$P$で完備化したものを$K_P$と書きます．
$P$は$K_P$に拡張することができます．
$K_P$における$\mathfrak{o}$や$\mathfrak{p}$の閉包はそれぞれ拡張した$P$の$K_P$における付値環及び素イデアルと一致します．
記号の乱用ですが，拡張した$P$の$K_P$における付値環及び素イデアルも$\mathfrak{o},\mathfrak{p}$と書くことにします．
これらについて次の定理が成り立ちます．
$t$を$\nu_P(t)=1$なる$K_P$の任意の元とする．このとき，$\nu_P(a)=i_0$なる任意の元$a$は
$$a=\sum_{i=i_0}^\infty u_i t^i, \quad u_i\in\mathfrak{o}/\mathfrak{p},\quad u_{i_0}\neq 0$$
という形に一意的に展開できる．
$\nu_P(a)=i_0$なる$a$に対し,$a^\prime=at^{-i_0}$とおけば，$\nu_P(a^\prime)=0$より，$a^\prime\in\mathfrak{o}$，$a^\prime\notin\mathfrak{p}$である．よって$a^\prime\equiv u_0$（mod$\mathfrak{p}$）なる$u_0\neq 0を\mathfrak{o}/\mathfrak{p}$から取ってくることができる．
今，$u_0,u_1,\cdots,u_{n-1}$を$\mathfrak{o}/\mathfrak{p}$から適当に選んで$$a^\prime\equiv u_0+u_1 t + \cdots + u_{n-1}t^{n-1},\quad \text{mod}\,\mathfrak{p}^n$$
とすることができたならば，
$$b=\frac{a^\prime-(u_0+u_1 t + \cdots + u_{n-1}t^{n-1})}{t^n}$$
において，$a^\prime-(u_0+u_1 t + \cdots + u_{n-1}t^{n-1})\in\mathfrak{p}^n$より，$\nu_P(b)\ge0$が成り立つ．よって$b\in\mathfrak{o}$．$b\equiv u_n$（mod$\mathfrak{p}$）なる元$u_n\in\mathfrak{o}/\mathfrak{p}$を取ると，$\mathfrak{p}=(t)$だったので
$t^nb\equiv t^nu_n$（mod$\mathfrak{p}^{n+1}$）が成り立つ．よって，
$$a^\prime\equiv u_0+u_1 t + \cdots + u_{n-1}t^{n-1}+u_n t^n\quad \text{mod}\,\mfp^{n+1}$$
が成り立つ．
こうして$u_0$から始めて$u_0,u_1,\cdots$を次々定めていけば
$$a^\prime = \sum_{i=0}^\infty u_i t^i$$
となり，
$$a=\sum_{i=0}^\infty u_i t^{i+i_0}$$
が得られる．書き直せば定理の主張の形にできる．
次に一意性を示す．定理の形になったと同時に，
$$a=\sum_{i=j_0}^\infty u_i^\prime t^i,\quad u_i^\prime\in\mfo/\mfp,\quad u_{j_0}^\prime\neq 0$$
ともなったとする．$\nu_P(u_{i_0})=\nu_P(u_{j_0}^\prime)=0$より$j_0 = \nu_P(a)=i_0$はすぐにわかる．よって$a^\prime = at^{-i_0}$の二つの展開
$$a^\prime = \sum_{i=0}^\infty u_{i+i_0}t^i = \sum_{i=0}^\infty u_{i+i_0}^\prime t^i$$
を比較して，
$$a^\prime \equiv u_{i_0}\equiv u_{i_0}^\prime\quad\text{mod}\,\mfp=(t)$$
今，$u_i,u_i^\prime$は$\mfo/\mfp$から選んでいたので，$u_{i_0}=u_{i_0}^\prime$が分かる．
よって
$$\frac{a^\prime-u_{i_0}}{t}=\sum_{i=1}^\infty u_{i+i_0}t^{i-1} = \sum_{i=1}^\infty u_{i+i_0}^\prime t^{i-1}$$
より
$$\frac{a^\prime -u_{i_0}}{t}\equiv u_{i_0+1}\equiv u_{i_0+1}^\prime\quad \text{mod}\,\mfp$$
が分かり，同様に$u_{i_0+1}= u_{i_0+1}^\prime$となり，以下同様にして次々に同じであるとわかる．
間違ってたらごめんなさい．．．