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.\]
For any binary relation $R$,
\[(R^{-1})^{-1} = R.\]
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:
Let $A$ and $B$ be finite sets. For any surjection $f : A \to B$, if for every $b\in B$,
\[\big\lvert f^{-1}[\{ b \}] \big\rvert = k,\]then
\[\lvert A \rvert = k \lvert B \rvert.\]