> [!NOTE] Theorem (Bijective iff invertible)
> Suppose $X$ and $Y$ are non-empty. Then $f:X\to Y$ is [[Bijection|bijective]] iff it has an [[Function Inverse|inverse]]. In this case the inverse is unique. ^db677e
*Proof*. ($\implies$) Suppose $f:X\to Y$ is bijective. Then $f$ has both a left inverse $g$ and a right inverse $g'.$ Suppose $y$ is any element of $Y.$ We compute as follows: $
\begin{aligned}
g(y) & =g\left(\operatorname{Id}_Y(y)\right) & & \text { definition of } \operatorname{Id}_Y \\
& =g\left(\left(f \circ g^{\prime}\right)(y)\right) & & g^{\prime} \text { is a right inverse for } f \\
& =\left(g \circ\left(f \circ g^{\prime}\right)\right)(y) & & \text { definition of composition } \\
& =\left((g \circ f) \circ g^{\prime}\right)(y) & & \text { associativity of composition } \\
& =(g \circ f)\left(g^{\prime}(y)\right) & & \text { definition of composition } \\
& =\operatorname{Id}_X\left(g^{\prime}(y)\right) & & g \text { is a left inverse for } f \\
& =g^{\prime}(y) & & \text { definition of } \operatorname{Id}_x
\end{aligned}
$Thus $g=g'$ is the desired inverse for $f.$
If $g''$ is another inverse for $f$ then the above computation with $g''$ instead of $g'$ shows that $g=g''.$ Thus $f$ has a unique inverse.
($\impliedby$) Suppose that $f$ has an inverse $g.$ So $g$ is both a right and left inverse for $f$ and so $f$ is bijective, as required.