AC supplies the countable and dependent choices used in Banach integration

Let $(A_n{)}_{n\in \mathbb{N}}$ be a countable family of nonempty sets. Its image $\mathcal{A}=\{A_n:n\in \mathbb{N}\}$ is a set of nonempty sets, so [F1] gives a choice function $c$ on $\mathcal{A}$. Define $b(n)=c(A_n)$. Then $b(n)\in A_n$ for every $n$, proving [F2]. Repeated members of the family cause no ambiguity because $c$ assigns them the same selected value. The empty subfamily has the empty choice function, and singleton members force their unique values.

Let $X$, $R$, and $a$ satisfy the second assertion. For $x\in X$ put $S_x=\{y\in X:xRy\}$. Seriality makes every $S_x$ nonempty. Apply [F1] to the set $\mathcal{S}=\{S_x:x\in X\}$, choose $c(S)\in S$ for every $S\in \mathcal{S}$, and define $s(x)=c(S_x)$. This is a well-defined self-map even if two successor sets coincide, and $xRs(x)$ for every $x$.

Apply [F4] to $s$ and $a$. The resulting sequence satisfies $x_0=a$ and $x_{n+1}=s(x_n)$, hence $x_{n}R{x}_{n+1}$ by step 1.2. This is exactly [F3]. If $X$ is a singleton, seriality forces the constant sequence; the empty-set case is excluded by the supplied $a$. AC is used only for the fixed-family selections in steps 1.1 and 1.2, while recursion makes no further choice.