In this entry, we show that the statement:

(*) the non-empty generalized cartesian product of non-empty sets is non-empty

Proof. Suppose $C=\lbrace A_j\mid j\in J\rbrace$ is a set of non-empty sets, with $J\ne \varnothing$ We want to show that $$B:=\prod_{j\in J} A_j$$ is non-empty. Let $A = \bigcup C$ Then, by AC, there is a function $f:C\to A$ such that $f(X)\in X$ for every $X\in C$ Define $g:J \to A$ by $g(j):=f(A_j)$ Then $g\in B$ as a result, $B$ is non-empty.

Remark. The statement that if $J\ne \varnothing$ then $B\ne \varnothing$ implies $A_j\ne \varnothing$ does not require AC: if $B$ is non-empty, then there is a function $g:J\to A$ and, as $J\ne \varnothing$ $g\ne \varnothing$ which means $A\ne \varnothing$ or that $A_j\ne \varnothing$ for some $j\in J$

Proof. Suppose $C$ is a set of non-empty sets. If $C$ itself is empty, then the choice function is the empty set. So suppose that $C$ is non-empty. We want to find a (choice) function $f: C\to \bigcup C$ such that $f(x)\in x$ for every $x\in C$ Index elements of $C$ by $C$ itself: $A_x:=x$ for each $x\in C$ So $A_x\ne \varnothing$ by assumption. Hence, by (*), the (non-empty) cartesian product $B$ of the $A_x$ is non-empty. But an element of $B$ is just a function $f$ whose domain is $C$ and whose codomain is the union of the $A_x$ or $\bigcup C$ such that $f(A_x)\in A_x$ which is precisely $f(x)\in x$