From dc2acaa4c6b29352e3b8a8a3de54602cf9fe018a Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 9 Jul 2025 00:24:58 +0200
Subject: Refine `bijection_circ`

---
 library/function.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/function.tex b/library/function.tex
index f74acbf..c7f709e 100644
--- a/library/function.tex
+++ b/library/function.tex
@@ -618,8 +618,8 @@
 \end{proposition}
 \begin{proof}
     $g\circ f\in\surj{A}{C}$ by \cref{bijections,surjections_circ}.
-
     $g\circ f$ is an injection.
+    Follows by \cref{circ_rightunique,bijections}.
 \end{proof}
 
 \subsection{Converse as a function}
-- 
cgit v1.2.3