Choice for a Family Indexed by a Finite Set

Let $S$ be a set, let $F$ be a finite set, and let $(A_i)_{i\in F}$ be a family of subsets of $S$ indexed by $F$ such that $A_i\ne\emptyset$ for every $i\in F$.

Then there exists a function $a:F\to S$ such that $a(i)\in A_i$ for every $i\in F$.