DEF-FINV. Inverse Function.
Let $f$ be a function. If $f$ is injective, then the converse relation $f^{-1}$ is also a function and is called the inverse / inverse function of $f$. $f$ is also called invertible.
PROP-FINV-ID.
Let $f$ be an injection. Then
$f\circ f^{-1}=\operatorname{id}_{\operatorname{ran}f}$;
$f^{-1}\circ f=\operatorname{id}_{\operatorname{dom}f}$.