Happiness is a warm proof

{\thm For a function $f$, a finite domain implies a finite range. The converse does not hold. }
\begin{proof}
Suppose $|\dom f| = 1$ such that $\dom f = \{x\}$. Then, trivially, $\ran f = \{f(x)\}$, whence the range is finite.

Assume inductively the theorem holds for all $|\dom f| = k$ where $k \leq n$. S/F/A/C there exists
a $f: A \to B$ for any two sets $A, B$ such that $|\dom f| = |\dom A| = n+1$ and an infinite range.
Then we can construct the surjection
$g: A \to \ran f$. Because $A$ is finite, there exists the bijection $h: A \to \omega_{n+1}$. Then
$s = g \circ h^{-1}: \omega_{n+1} \to \ran f$ is also onto, whence $p: \omega_{n+1} \backslash
\{m \in \omega_{n+1}: s(m) = s(n)\} \to \ran f \backslash \{s(n)\}$ such that $p(x) = s(x)$ is
also onto. Trivially, $|\dom p| \leq n$ because the set we're subtracting is nonempty due to the fact
that $s$ is onto. By our inductive assumption, $\ran f \backslash \{s(n)\}$ is finite. By a class lemma,
$\ran f \backslash \{s(n)\} \cup \{s(n)\} = \ran f$ is also finite, a contradiction.
Therefore, the range is finite.

By the principle of complete induction, we have proven the theorem.
\end{proof}