Description: An onto function implies dominance of domain over range. Lemma 10.20 of
Kunen p. 30. This theorem uses the axiom of choice ac7g . The axiom
of choice is not needed for finite sets, see fodomfi . See also
fodomnum . (Contributed by NM, 23-Jul-2004)(Proof shortened by BJ, 20-May-2024)