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.

For every $n<\omega$ there is a set code $c=(\alpha ,s)$ with $F(c)=f(n)$. Collection applied to this formula over the set $\omega$ gives one set $C$ of codes meeting every fibre. Thus $C_n=\{c\in C:F(c)=f(n)\}$ is a nonempty set for each $n$. Ambient AC now chooses $c_n=({\alpha }_n,s_n)\in C_n$ simultaneously. 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 selection from the set-family $(C_n{)}_{n<\omega }$ 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.