The Number of Elements of a Disjoint Finite Union

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $I$ be a finite set and $(C_{i})_{i\in I}$ a family of finite sets with $C_{i}\cap C_{i'}=\emptyset$ for all distinct $i,i'\in I$, let $\#$ be as in The Number of Elements of a Finite Set §cardinality, and let sums in $\mathbb{N}_{0}$ over finite sets be as in Sums and Products over a Finite Set and over an Interval §sums, which apply to the addition of $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws. The union $\bigcup_{i\in I}C_{i}$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §family-union.

¶ $\#\bigcup_{i\in I}C_{i}=\sum_{i\in I}\#C_{i}$.

¶ If $r\in\mathbb{N}_{0}$ and $\#C_{i}=r$ for every $i\in I$, then $\#\bigcup_{i\in I}C_{i}=\#I\cdot r$.