これで正解だ！！！！！！！！！！！！！

f:X→Y
fは全単射⇔∃g:Y→X　s.t. g。f=1_x f。g=1_y

（⇒）
fが全単射と仮定する。
g:Y→X　g(f(x))=x　と定義する。

gはwell-def
∵
fが全射であることから、∀y∈Yに対して∃x∈X　s.t. f(x)=y
またfが単射であることから∀y∈Yに対してそれに対応するx∈Xは一つである。
ゆえに、gはy=f(x)∈Y にx∈Xを対応させる写像である。

g。f(x)=g(f(x))=x　(∵gの定義)

f。g(y)=f。g(f(x))
　　　 =f(x) (∵　gの定義)
=y

QED