AC supplies countable selections and prescribed serial paths

For an omega-indexed family $(A_n)$ of nonempty sets, its image $\mathcal{S}=\{A_n:n\in \mathbb{N}\}$ is a set of nonempty sets. By [F1] choose $c$ with $c(A)\in A$ for every $A\in \mathcal{S}$. Then $b(n)=c(A_n)$ is a function and $b(n)\in A_n$, which is [F2]. Repeated sets use the same selected value and cause no ambiguity. For an empty index family the empty function already suffices; singleton fibers force their unique value.

For the stated serial R, every fiber $R[x]=\{y\in X:xRy\}$ is nonempty. AC applied to the set of all these fibers gives c with $c(R[x])\in R[x]$. Define the self-map $s(x)=c(R[x])$ on X. No recursively changing choice is being assumed: s is now one fixed function chosen from a fixed set of nonempty fibers. It satisfies $xRs(x)$ for every x.

Apply [F4] to X, the prescribed a and s to obtain $x_0=a$ and $x_{n+1}=s(x_n)$ for every natural n. The defining property of s gives $x_{n}R{x}_{n+1}$, precisely [F3]. If X has one element and R is serial, this is its constant sequence. Empty X is excluded by the prescribed a. The uses of AC are exactly the two fixed-family selections in steps 1.1 and 1.2; recursion itself requires no further choice. This proves the two implications from AC, not either converse.