# Principle of Finite Choice

## Theorem

Let $I$ be a non-empty finite indexing set.

Let $\left\langle{S_i}\right\rangle_{i \mathop \in I}$ be an $I$-indexed family of non-empty sets.

Then there exists an $I$-indexed family $\left\langle{x_i}\right\rangle_{i \mathop \in I}$ such that:

$\forall i \in I: x_i \in S_i$

That is, there exists a mapping:

$\displaystyle f: I \to \bigcup_{i \mathop \in I} S_i$

such that:

$\forall i \in I: f \left({i}\right) \in S_i$

## Proof

We use the Principle of Mathematical Induction on the cardinality of $I$.

### Basis for the Induction

Let $\left\vert{I}\right\vert = 1$.

Let $j \in I$.

Then $I = \left\{{j}\right\}$.

By the definition of a non-empty set, there exists an $x \in S_j$.

Hence, there exists a mapping $f: I \to S_j$ such that $f \left({j}\right) = x$.

Since $\forall i \in I: i = j$, the result follows.

### Induction Hypothesis

Assume that the theorem holds for all $I$ with $\left\vert{I}\right\vert = n$.

This is the induction hypothesis.

### Induction Step

Now, suppose that $\left\vert{I}\right\vert = n + 1$.

Let $j \in I$.

Let $J = I \setminus \left\{{j}\right\}$.

By Cardinality Less One, $\left\vert{J}\right\vert = n$.

By the induction hypothesis, there exists a mapping:

$\displaystyle g: J \to \bigcup_{i \mathop \in J} S_i$

such that:

$\forall i \in J: g \left({i}\right) \in S_i$

By the definition of a non-empty set, there exists a $y \in S_j$.

Hence, there exists a mapping:

$\displaystyle f: I \to \bigcup_{i \mathop \in I} S_i$

such that:

$\displaystyle \forall i \in I: f \left({i}\right) = \begin{cases} g \left({i}\right) & : i \ne j \\ y & : i = j \end{cases}$

Then:

$\forall i \in I: f \left({i}\right) \in S_i$

as desired.

$\blacksquare$