>>21
つづき

３）
同値類内の
2つの形式的冪級数の差 Fp-Fp'を作ると、nから先が一致するから
Fp-Fp'＝(s1-s'1)x+(s2-s'2)x^2+(s3-s'3)x^3・・・+0X^n0+0X^(n0+1)+・・・
（シッポの「+0X^n0+0X^(n0+1)+・・・」の部分は、n0次以上の項から係数が0になる意味です。なお、それ以前の係数は0ではない）
つまり、p'=Fp-Fp' で、p'∈R[X] （多項式環）で、n0-1次多項式です
上記の式を変形して、Fpと同じ同値類の任意の元Fp'は
Fp'=Fp-p' と書ける
つまり、任意のFp'は、Fpから多項式 p'を引いたものになる
多項式 p'は、下記のwikipedia 多項式環の定義の通り
”多項式には項が有限個しかないこと -つまり十分大きな k（ここでは k > m）に関する係数 pk がすべて零である”です
（なお、R[X] は環だから、任意の和と積の２項演算で閉じているので、R[X]に含まれる多項式の次数nには、上限は無いことを注意しておこう）
そして、p'がR[X] の全てを渡ることで、Fpの同値類が尽くされることにも、注意しておこう

４）
いま、簡単のために、Fpの係数、即ち数列 s = (s1，s2，s3 ，・・・）の各数ｓｎたちはどれも0ではないとする。こうしても、一般性は失わなれない
つまり、Fp not∈R[X] かつ Fp ∈R[[X]] ということです
これで、上記の多項式p'が多項式環R[X] の全てを渡っても
必ず Fp'=Fp-p' ≠0 (つまり、Fp'の係数が全て0になることはないということ）
もっと言えば、シッポの先に、係数で0にならない部分が、必ず残るということ

つづく