The Number of Elements of a Finite Set

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $A$ be a finite set, and let $[n]$ be as in Intervals of Natural Numbers §segment.

¶ The number of elements of $A$, written $\#A$, is the unique $n\in\mathbb{N}_{0}$ for which there is a bijection from $[n]$ onto $A$, given 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 §unique.