There are two finite choice theorems, the internal one and the external one, both are true in ZF.
As Charles Staats pointed out, the external version is a tautology (modulo some finite combinatorics): if $a_1,\dots,a_n$ are all nonempty, then there are $z_1 \in a_1$,...,$z_n \in a_n$ and then $\{(a_1,z_1),\ldots,(a_n,z_n)\}$$\lbrace (a_1,z_1),\ldots,(a_n,z_n)\rbrace$ is the desired choice function for the family $X = \{a_1,\dots,a_n\}$$X = \lbrace a_1,\dots,a_n \rbrace$ of nonempty sets.
The internal version "every finite family of nonempty sets has a choice function" is stronger since a model of ZF may have nonstandard finite cardinals. The proof in this case is by induction on the cardinality of the family.
The empty family has a trivial choice function — the empty function. Suppose we know the theorem to be true for families of size $n$. Let $X$ be a family of nonempty sets with size $n+1$. Let $g:n+1\to X$ be a bijection. Let $X' = g[n]$ and $a = g(n)$. Then $X'$ is a family of nonempty sets of size $n$, which therefore has a choice function $f':X' \to \bigcup X'$. Since $a$ is nonempty, we can find $z \in a$ and hence $f = f' \cup \{(a,z)\}$$f = f' \cup \lbrace (a,z) \rbrace$ is a choice function for the original family $X$.