The Solovay inner model is closed under ambient omega-sequences

Formula, rank and finite ordinal codes together with $s\in S$ give a definable surjection $F:\mathrm{O}\mathrm{r}\mathrm{d}\times S\twoheadrightarrow M$: for a code, return the uniquely defined object, and return $\mathrm{\varnothing }$ for an invalid code.

By ambient AC choose for each $n$ a pair $({\alpha }_n,s_n)$ with $F({\alpha }_n,s_n)=f(n)$. A fixed pairing ${\omega }^2\cong \omega$ interleaves the $s_n$ into one $s\in S$, while the countable ordinal sequence $n\mapsto {\alpha }_n$ is also a member of $S$; interleave these two sequences once more. This is the sole new use of Choice.

The graph of $f$ is definable from that one $S$-parameter and the fixed definition of $F$, and every value has hereditary $OD(S)$ transitive closure. Hence the graph and $f$ belong to $M$. The empty-domain restriction and constant sequences use the same code and require no selection.