Definition 1. Let $R$ be a binary relation. The converse of $R$ is the relation
\[R^{-1} = \{(y, x) : (x, y) \in R\}.\]This is a set by Separation Schema:
\[R^{-1} \subseteq \im R \times \dom R.\]Proposition 1 (Involutivity). For any binary relation $R$,
\[(R^{-1})^{-1} = R.\]Proposition 2. Let $A$ and $B$ be finite sets. For any surjection $f : A \to B$,
\[\lvert A \rvert = \sum_{b \in B} \big\lvert f^{-1}[\{ b \}] \big\rvert.\]Proof.
\[A = \bigsqcup_{b \in B}f^{-1}[\{ b \}].\]
In particular:
Proposition 3. Let $A$ and $B$ be finite sets. For any surjection $f : A \to B$, if
\[\big\lvert f^{-1}[\{ b \}] \big\rvert = k\]for every $b\in B$, then
\[\lvert A \rvert = k \lvert B \rvert.\]