Sets of Maps between Finite Sets, Finite Unions of Finite Sets, and Finite Choice

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let finite sets be as in Finite Sets §finite, and let $A$ and $B$ be sets.

¶ If $A$ and $B$ are finite, then the set $B^{A}$ of maps from $A$ to $B$ is finite; if moreover $B\neq\emptyset$, then $B^{A}\neq\emptyset$.

Let now $I$ be a finite set and $(C_{i})_{i\in I}$ a family of sets, with union $\bigcup_{i\in I}C_{i}$ as in Indexed Families of Sets and Their Union, Intersection and Product §union, a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets §union.

¶ If $C_{i}$ is finite for every $i\in I$, then $\bigcup_{i\in I}C_{i}$ is finite.

¶ If $C_{i}\neq\emptyset$ for every $i\in I$, then there is a map $f:I\to\bigcup_{i\in I}C_{i}$ with $f(i)\in C_{i}$ for every $i\in I$.