[proofplan] Take an arbitrary indexed family $(A_i)_{i\in I}$ of inhabited sets. The Blass coding lemma assigns to it a [vector space](/page/Vector%20Space) $V(A)$ whose Hamel bases decode into choice functions for the family. The basis principle supplies a Hamel basis $E$ of $V(A)$. Applying the decoding operation to $E$ gives the required function $c$ with $c(i)\in A_i$ for every $i$. [/proofplan] [step:Start with an arbitrary inhabited family] Let $(A_i)_{i\in I}$ be an indexed family of inhabited sets. To prove the choice principle, it is enough to construct a function $c:I\to\bigcup_{i\in I}A_i$ such that $c(i)\in A_i$ for each $i\in I$. [guided] The family $(A_i)_{i\in I}$ is arbitrary, and each $A_i$ is inhabited. The choice principle asks us to produce one function $c:I\to\bigcup_{i\in I}A_i$ with the membership property $c(i)\in A_i$ for every index $i\in I$. Proving this for the arbitrary family proves the universal statement. [/guided] [/step] [step:Apply the coding lemma and the basis principle] By the Blass coding lemma, the family $(A_i)_{i\in I}$ determines a $k$-vector space $V(A)$ and a decoding operation $\operatorname{Dec}_A$ with the stated property. By the basis principle, the vector space $V(A)$ has a Hamel basis; choose one and call it $E$. [guided] The coding lemma turns the family $(A_i)_{i\in I}$ into the vector space $V(A)$ and provides the operation $\operatorname{Dec}_A$. The basis principle applies to this particular $k$-vector space, so there exists a Hamel basis $E$ of $V(A)$. [/guided] [/step] [step:Decode the basis into a choice function] Define \begin{align*} c=\operatorname{Dec}_A(E). \end{align*} Since $E$ is a Hamel basis of $V(A)$, the defining property of $\operatorname{Dec}_A$ says that $c$ is a function \begin{align*} c:I\to\bigcup_{i\in I}A_i \end{align*} and that $c(i)\in A_i$ for every $i\in I$. [guided] Set $c=\operatorname{Dec}_A(E)$. The hypothesis on $\operatorname{Dec}_A$ applies to every Hamel basis $E$ of $V(A)$, and the previous step produced such a basis. Therefore $c:I\to\bigcup_{i\in I}A_i$ and $c(i)\in A_i$ for all $i\in I$. [/guided] [/step] [step:Conclude the choice principle] The construction above assigns a choice function to the arbitrary inhabited family $(A_i)_{i\in I}$. Hence every indexed family of inhabited sets admits a choice function. [/step]