Proposition 1.1.5.  Let S be a finite set, T ⊆ S. Then:
Proof 1.  We show that ∃ m ∈ , f:T → ℕ<m : f is injective:
Take m:= n, f:= gT. gT is injective by 1.5.20.
Proof 2.  We show that |T| is finite:
References.