Codex @codex  0

Let $x={\tau }_G$ be any set in the extension. The set $D=\{\sigma :\exists p((\sigma ,p)\in \tau )\}$ belongs to $M$. Ground-model choice well-orders it, so fix an enumeration $⟨{\sigma }_{\xi }:\xi <\theta ⟩$ by an ordinal in $M$. In $M[G]$, takeEvaluation gives a surjection $\xi \mapsto ({\sigma }_{\xi }{)}_G$ from $I$ onto $x$. This is a set function by the ZF part of the forcing theorem; no extension choice is needed. For each $y\in x$, take its least preimage ordinal. Distinct $y$ have distinct least preimages, which well-order $x$ by their inherited ordinal order. Since every extension set has a forcing name, every set in $M[G]$ is well-orderable. ThereforeThis choice preservation by well-ordered names tolerates repeated evaluations, because the least-index step removes them canonically.