f:X→Y:写像
f:単射⇒∃g:Y→X　s.t. g。f=1_x

証明
f:単射と仮定する。
g:Y→Xを
g(y)=g(f(x))=x　(if y∈f(X))　　g(y)=w　otherwise
と定義する。
g:well-defined
なぜならy∈Yに対してf(x)=yとなるx∈Xが存在するなら、x∈Xは一意である。
(∵f:単射)
f(x)=yとなるx∈Xが存在しないなら、g(y)=wとおく。
結局gは∀y∈Yに対してXの元を一つずつ対応させる写像である。

このとき
g。f(x)=g(f(x))
　　　 =x (∵gの定義)

よってg。f=1_x



どうですか？？？わかりにくいでしょうか？
また、あたっているでしょうか？どこかおかしなことがあったらよろしく
お願いします。