When we count a class of objects, we generate an enumeration of them, which we may represent by a bijection from a standard class having that many objects to the class being counted. Our standard class of
So, a class
f:(nA). Bij(n; A; f)
which may also be expressed as
(n ~ A)
Now, since counting means coming up with an enumeration, we may ask whether counting in different ways, i.e., coming up with different orders, will always result in the same number, as we assume. Of course, we know this is so, but there are different degrees of knowing. It is not necessary to simply accept this as an axiom; there is enough structure to the problem to make a non-trivial proof.
Thm* (A ~ m) (A ~ k) m = k
This theorem is closely related to what is sometimes called the "pigeon-hole principle", which states the mathematical content of the fact that if you put
Thm* m,k:, f:(mk). k<m (x,y:m. x y & f(x) = f(y))
If you examine the proofs of these theorems, you will notice that they both cite the key lemma
Thm* (f:(mk). Inj(m; k; f)) mk.