(m+1); (k+1); f) 
Inj(m; k; Replace value k by f(m) in f)(m+1); (k+1); f)
Thm*
Thm* (
i:m. f(i) = k (Replace value k by f(m) in f)(i) = f(m) 
k)(m+1); (k+1); f)
Thm*
Thm* (
i:m. 
f(i) = k (Replace value k by f(m) in f)(i) = f(i) k)