The serial-relation Dependent Choice principle over ZF

Work in ZF. Write $\omega =\{0,1,2,\dots \}$ as in The natural numbers $\mathbb{N}$ (von Neumann). A relation $R\subseteq A\times A$ is serial on $A$ when $(\mathrm{\forall }a\in A)(\mathrm{\exists }b\in A)aRb$, where $aRb$ means $(a,b)\in R$ (Relation, $\mathrm{dom}R$, $\mathrm{ran}R$, $\mathrm{fld}R$, and the specialisations "relation from $A$ to $B$" and "relation on $A$").

Dependent Choice (DC) is the following global principle: for every nonempty set $A$ and every serial relation $R$ on $A$, there is a function $f:\omega \to A$ such that $f(n)Rf(n+1)$ for every $n\in \omega$. Here function has its ordinary set-theoretic meaning A function is a relation $f$ with $(a,b)\in f$ and $(a,c)\in f$ implying $b=c$; $f:A\to B$, the value $f(a)$, domain and codomain.

The prescribed-start form asks, for each such $A,R$ and each $a_0\in A$, for such an $f$ with $f(0)=a_0$. The equivalence of these global principles requires a proof; it is not part of the definition.

Neither form requires distinct values, an irreflexive relation, or transitivity. On a singleton $A=\{a\}$, seriality forces $aRa$ and the constant map satisfies the requirement. The empty carrier is excluded: it has a vacuously serial relation but admits no map from $\omega$.

The nonempty qualification is explicit in Karagila, Definition 4, printed p.4. Miller, Definition 5.1, printed p.10, supplies the starting-point-free formula but omits that necessary qualification in its displayed wording.