Solution (source code)

= Solution

For each $y\in Y$, <surjectivity> makes the <fiber of a function> $f^{-1}(\{y\})$ nonempty. Choose one element $x_y$ of each such <fiber of a function> and define $g(y)=x_y$. Then $f(g(y))=y$ for every $y$, proving \b[$f\circ g=I_Y$]. For arbitrary <sets>, the simultaneous selection invokes the usual <axiom of choice>; this is the <right-inverse characterization of the axiom of choice>. For finite $Y$ only finitely many choices are needed. If $Y$ is empty, the unique empty <function> gives the same conclusion.