>>680
>yたちを具体的な式に展開して命題に書かないとだめ

選択公理を仮定すれば
任意の類 ∀[s]∈R^N/〜 に対して代表列 r=f([s])∈[s] を与える選択関数 f:R^N/〜 → R^N の存在が保証される。
関数 g:R^N → R^N/〜 を g(s)=[s] で定義すれば、合成関数 f・g:R^N → R^N は、任意の実数列 ∀s∈R^N に対しその代表列 r=f・g(s) を与える。
ある実数列sの第D+1項から先すべてが分かっているなら、D+1より前の項を0で埋めた実数列s'はs〜s'を満たすから、f・g(s')=f・g(s)=r はsの代表rを与える。

y_iを次で定義する：∀n≧y_i ⇒ x_i[n]=f・g(x_i')[n]
ここでx_i'はx_iのある項より前を0で置換した実数列

以上で、x_i→x_i'→f・g(x_i')→y_i　の対応関係が定義されるので、関数d:R^N→N が定義できて、y_i=d(x_i)=d(x_i')　と書ける。

∀x_1,…,x_100∈R^N.∃d(x_1)=d(x_1'),…,d(x_100)=d(x_100')∈N.P(回答者が選んだ列xと対応するd(x)に対してx[d(x)]=r(x)[d(x)])=99/100

はい、yたちを具体的な式に展開して命題に書きました。