Studying the differences between the direct product and the direct sum of modules, my book candidly says that we don't need the axiom of choice to know that the direct product of modules is a non-empty set.
I have thought about it for a while, but it seems to be much more subtle than I have conceived. How to see this fact?
Modules have a 0 element. It is a distinct element that is uniformly definable, so that means that you can always choose that one.