24/03/01 22:16:02.49 RwyqkuNg.net
>>499
任意の類 ∀[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を与える。証明おわり。
注 この仮定は選択公理を仮定するなら成立する。