 Product-sum comparison lemma

In ZF, let $K,L$ be nonempty. If $K\times L$ injects into $K\bigsqcup L$, then there is either an injection or a surjection from $K$ to $L$.

Indeed, extend the inverse of the given injection to a surjection $p:K\bigsqcup L\to K\times L$ by sending points outside its range to one fixed pair $(k_{\ast },l_{\ast })$. If the second coordinate of $p$ restricted to the $K$-summand covers $L$, it is the required surjection. Otherwise choose $l_0$ that it misses. Every $(k,l_0)$ then has its preimage in the $L$-summand. Except possibly for the default pair, that preimage is unique, so these preimages inject $K$ into $L$. In the exceptional case they inject $K\setminus \{k_{\ast }\}$ into $L$; either their image is all of $L$, yielding a surjection from $K$, or an omitted point extends the map to an injection from $K$.