[proofplan]
We prove the result by induction on the finite ordinal $n \in \omega$. The base case $n = 0$ is exactly the [Empty Set axiom](/page/Empty%20Set%20Axiom). In the successor step, we assume that the finite image of any indexed family over $n$ exists, restrict an indexed family over the successor ordinal to the old domain $n$, and then adjoin the new value using the [Pairing axiom](/page/Pairing%20Axiom) and the [Union axiom](/page/Union%20Axiom).
[/proofplan]
[step:Verify the empty-indexed case using the Empty Set axiom]
Let $n = 0$, and let $a$ be an indexed family of sets over $0$, meaning a function whose domain is $0$ and whose values are sets. By the [Empty Set axiom](/page/Empty%20Set%20Axiom), there exists a set $F$ such that, for every set $x$, $x \notin F$. Since there is no $i \in 0$, we have
\begin{align*}
x \in F \iff \exists i \in 0 \; x = a(i)
\end{align*}
for every set $x$. Thus the desired set exists when $n = 0$.
[/step]
[step:Adjoin one new element to a finite set]
Assume that for a fixed $n \in \omega$, every indexed family of sets over $n$ has a finite image set. Let $b$ be an indexed family of sets over $n \cup \{n\}$, meaning a function whose domain is the successor ordinal $n \cup \{n\}$ and whose values are sets.
Since $n \subset n \cup \{n\}$, the restriction of $b$ to $n$ exists as the set of ordered pairs
\begin{align*}
a := b|_n = \{(i,y) \in b : i \in n\}.
\end{align*}
This restriction $a$ is a function with domain $n$, and for every $i \in n$ its value satisfies $a(i)=b(i)$.
By the induction hypothesis, there exists a set $F$ such that, for every set $x$,
\begin{align*}
x \in F \iff \exists i \in n \; x = b(i).
\end{align*}
By the [Pairing axiom](/page/Pairing%20Axiom) applied to $b(n)$ and $b(n)$, there exists the singleton set
\begin{align*}
S = \{b(n)\}.
\end{align*}
By the [Pairing axiom](/page/Pairing%20Axiom) applied to $F$ and $S$, there exists the set
\begin{align*}
P = \{F,S\}.
\end{align*}
By the [Union axiom](/page/Union%20Axiom), there exists the set
\begin{align*}
G = \bigcup P.
\end{align*}
For every set $x$,
\begin{align*}
x \in G
&\iff \exists Y \in P \; x \in Y \\
&\iff x \in F \ \text{or}\ x \in S \\
&\iff \left(\exists i \in n \; x = b(i)\right) \ \text{or}\ x = b(n) \\
&\iff \exists i \in n \cup \{n\} \; x = b(i).
\end{align*}
Thus the finite range set for $b$ exists.
[guided]
The induction hypothesis gives us a set containing exactly the first $n$ values of the function. We must show how to add the next value without assuming that finite sets already exist.
Let $b$ be an indexed family of sets over $n \cup \{n\}$, meaning a function whose domain is the successor ordinal $n \cup \{n\}$ and whose values are sets. We restrict $b$ to the old domain $n$ by forming the set of ordered pairs
\begin{align*}
a := b|_n = \{(i,y) \in b : i \in n\}.
\end{align*}
Because $n \subset n \cup \{n\}$, this restriction is a function with domain $n$, and for every $i \in n$ it satisfies $a(i)=b(i)$. The induction hypothesis applies to this restricted indexed family, so there is a set $F$ satisfying
\begin{align*}
x \in F \iff \exists i \in n \; x = b(i)
\end{align*}
for every set $x$.
Now we must add the one remaining value $b(n)$. The [Pairing axiom](/page/Pairing%20Axiom) applied to $b(n)$ with itself gives the singleton
\begin{align*}
S = \{b(n)\}.
\end{align*}
The [Pairing axiom](/page/Pairing%20Axiom) applied to the two sets $F$ and $S$ gives
\begin{align*}
P = \{F,S\}.
\end{align*}
The [Union axiom](/page/Union%20Axiom) then gives
\begin{align*}
G = \bigcup P.
\end{align*}
This set contains exactly the elements belonging to either $F$ or $S$. Therefore, for every set $x$,
\begin{align*}
x \in G
&\iff \exists Y \in P \; x \in Y \\
&\iff x \in F \ \text{or}\ x \in S \\
&\iff \left(\exists i \in n \; x = b(i)\right) \ \text{or}\ x = b(n).
\end{align*}
Since the successor ordinal $n \cup \{n\}$ has precisely the elements of $n$ together with the new element $n$, the last condition is equivalent to
\begin{align*}
\exists i \in n \cup \{n\} \; x = b(i).
\end{align*}
Thus $G$ is exactly the finite set of values of $b$.
[/guided]
[/step]
[step:Conclude by induction on $\omega$]
The base case holds for $0$, and the successor step shows that the assertion for $n$ implies the assertion for $n \cup \{n\}$. By [induction on $\omega$](/page/Induction%20on%20Omega), for every $n \in \omega$ and every indexed family of sets $a$ over $n$, there exists a set $F$ such that
\begin{align*}
x \in F \iff \exists i \in n \; x = a(i)
\end{align*}
for every set $x$. Given sets $a_0,\dots,a_{n-1}$, they determine the indexed family $a$ over $n$ by $a(i)=a_i$ for each $i \in n$. Applying the preceding sentence to this family gives a set $F$ whose elements are exactly $a_0,\dots,a_{n-1}$, which is the asserted set $\{a_0,\dots,a_{n-1}\}$.
[/step]
