Group structure on every nonempty set (source code)

= Group structure on every nonempty set
{title2=$x\star y=j^{-1}(j(x)j(y))$}

Assuming choice, every nonempty <set> admits a <group operation>. A <finite set> receives a <cyclic group> structure. For an <infinite set>, a maximal partial <group> obtained by Zorn has infinite carrier $A$ with smaller complement; infinite-cardinal doubling implies the whole <set> is equipotent with $A$. Transport its operation along a <bijection> $j$. This final <group> need not extend a previously chosen partial <group> on its original <subset>; transport changes labels and only asserts existence.