Without choice, it's impossible to guarantee that an arbitrary product of non-empty sets is non-empty. The Cartesian product would just be a set containing the empty function, which is a singleton set and therefore non-empty. This definition doesn't rely on the Axiom of Choice, so we can prove in ZF¬C that the empty Cartesian product of non-empty sets is non-empty. So, the question of proving that an empty Cartesian product of non-empty sets is non-empty in ZF¬C does not seem to be problematic. This is the same across all standard set theories (ZF, ZF¬C, ZFC), because it's not about selecting an element from each of the sets in the family (which would require AC), it's just about the definition of the Cartesian product when there are no sets in the family.