The problem is: Using the Axiom of Choice, prove that if $(X,\leq)$ is an infinite finitely splitting tree, then $(X,\leq)$ has an infinite path. Be explicit where you use the Axiom of Choice.
I have a solution I'm not entirely sure about:
Call the minimal element of the tree $x_0$ (it exists by definition of tree). Then, the set of immediate successors of $x_0$ is finite and nonempty by definition of finitely splitting tree. Call it $A_0$.
Then define the function $g$ that selects one (any) of the elements of $A_0$, and call it $x_1$, i.e. $g(A_0)=x_1\in A_0$.
Repeat the process, consider $A_n$ the set of immediate successors of $x_n$ (finite and nonempty), and assign $g(A_n)=x_{n+1}\in A_n$ (with $x_{n+1}$ any element of $A_n$).
Therefore, we have a system of sets $S=\bigcup_{i=0}^{\infty} A_i$ (note it is infinite), and a choice function (which exists by the Axiom of Choice) since $g(A_i)\in A_i\ \forall i$, and $A_i\neq \varnothing \ \forall i$, since we are considering a finitely splitting tree.
Hence, we get a sequence $(x_n)$ for $n<\omega$ which is infinite because $S$ is, and $g(S)=(x_n)$, and $x_{n+1}$ is an immediate successor of $x_n$ for all $n<\omega$, thus $(x_n)$ is an infinite path.
Are there any problems in this proof? My doubts reside in that I am defining the choice function $g$ (which I know that exists by AC) on the system $S$, which I think also has to be defined using the AC, but for that you need $g$ again... Maybe is there a way of defining $S$ without mentioning $g$, and then construct $g$ on $S$?
The very common misconception is that you are defining the choice function. You cannot, should not, and do not. You are trying to define an infinite path (also known as a branch).
What you need to do is first fix a choice function which chooses a successor of a node in the tree, then use recursion to define this branch by iterating this choice function (and prove, of course, that it is an infinite branch).
Do note, sometimes "finitely splitting" includes the situation that not every node splits, in which case you need to argue that you can make your choice in a way that is still generating an infinite path, and not getting stuck at some point.