This will be proved using induction on m, varying k.
The base case, 0k, is trivial, so we move on to the induction step, assuming 0<m, and assuming the induction hypothesis:
k':. (f':((m-1)k'). Inj((m-1); k'; f')) m-1k'.
The problem is then to show that mk, given some fmk such that Inj(m; k; f).
Obviously, mk will follow from m-1k-1, so by applying the induction hyp to k-1, our problem reduces to finding an f'(m-1)(k-1) such that Inj((m-1); (k-1); f').
Such a construction is
Def Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f
Def (Replace values x s.t. P(x) by y in f)(i) == if P(f(i))y else f(i) fi
Thm* Inj((m+1); (k+1); f) Inj(m; k; Replace value k by f(m) in f)
This last theorem is sufficient for concluding our argument.
QED
Note:
Considering f(k+1)(j+1) as a sequence of k+1 values selected from the first j+1 natural numbers,
(Replace value j by f(k) in f) kj removes the entry for the largest value, namely j, and replaces it with the last value of the sequence, namely f(k), if necessary.
This is the key lemma to the proofs of the uniqueness of counting, and the pigeon-hole principle, i.e.,
f:(
m
m
kk':
k by f(m) in f
y else f(i) fi
y & f(x) = f(y))
