Description: Every infinite class is equinumerous to its Cartesian square. This
theorem, which is equivalent to the axiom of choice over ZF, provides the
basis for infinite cardinal arithmetic. Proposition 10.40 of
TakeutiZaring p. 95. This is a corollary of infxpen (used via
infxpidm2 ). (Contributed by NM, 17-Sep-2004)(Revised by Mario
Carneiro, 9-Mar-2013)