In many topology and analysis textbooks a discussion of the Axiom of Choice is offered. In this context, is often stated that the following property holds for finite collections of sets:

Let $n\in\mathbb{N}$ be a positive integer and $S_1,S_2,...,S_n$ be nonempty sets, then $S_1\times...\times S_n$ is nonempty, i.e. we can select a collection $(s_1,...,s_n)$ such that $s_i\in S_i\ \forall i$.

The lemma should follow directly from ZF axiomatization. This is not proved and the given justification goes like: 'we can pick an element of each set by some logical proposition and repeat the operation finitely many times'. The same is stated not to hold for infinite collections of sets, and hence infinite 'chain' of propositions. This is why we must axiomatize the existence of a choice function.

I think I grasp the idea but overall the given motivation seem to me quite fuzzy.
How formally can we 'pick an object'? Why the same technique does not hold in the infinite case?

The question may be obvious, but I do not have a strong knowledge of set theory and logic and I would like to know more. Any help would be great