Is induction neccessary for proving that every injective mapping of a finite set into itself is a mapping onto itself? Upon reviewing the basic theorem that the number of elements in a fixed finite set is unique, I tried to determine what part of this proposition is in need of proof.  It seems axiomatic.  Nonetheless, BBFSK have a very long-winded, and seemingly convoluted discussion of this, and related ideas.
When I attempted to produce my own argument in support of the above proposition, the part which I am not able to state purely in the terminology of mappings (bijection, injection, etc) is that an injection of a finite set into itself is a mapping onto itself.  The proof BBFSK give uses induction.  After thinking about it for a while, that was the only approach I could come up with.
Is there a rigorous proof of the proposition that every injective mapping of a finite set into itself is a mapping of the set onto itself which does not involve induction?
 A: Dedekind proposed to use this property as the definition of "finite set", so that's at least one alternative -- closely in line with your intuition of declaring it to be axiomatic. Unfortunately there are technical problems with that approach. In particular you then need the axiom of choice to prove that induction works for all "finite" cardinalities, which is untidy at the least.
(A set $X$ such that every injection $X\to X$ is a bijection is now called "Dedekind-finite").
In a standard development of set theory, on the other hand, you're out of luck. Here "finite" is defined as "has the same cardinality as an element of $\omega$", and $\omega$ is (essentially) defined to be the largest set that mathematical induction works for. So in order to prove anything about "finite" you need to have an induction somewhere, because that's the only way to connect to the definition. This induction can be hidden in the proof of another property that you depend on, but that is basically just kicking the buck around. Eventually it has to stop.

This comment by Daniel Schepler is also relevant (but see further discussion in the comment thread):

There's also the notion of Kuratowski finiteness, which is essentially equivalent to the condition that the power set of $$ is well-founded under the relation of "strict extension by one element". But then, of course, the natural way to prove nearly anything about Kuratowski finite sets is to use induction on the well-foundedness property... 

