The number of injections from a $k$-element set into an $n$-element set is $n^{\underset{‾}{k}}$

Base case $k=0$. Then $B=\mathrm{\varnothing }$, and the only function $\mathrm{\varnothing }\to A$ is the empty function, which is injective because injectivity is a condition on pairs of points of the domain and there are none. So $\mathrm{Inj}(B,A)=\{\mathrm{\varnothing }\}$ has cardinality $1=n^{\underset{‾}{0}}$.

Inductive hypothesis: fix $k$ and assume that for all finite $A$, $B^{\mathrm{\prime }}$ with $\mid A\mid =n$ and $\mid B^{\mathrm{\prime }}\mid =k$ the set $\mathrm{Inj}(B^{\mathrm{\prime }},A)$ is finite with cardinality $n^{\underset{‾}{k}}$.

Setting up the inductive step. Let $\mid B\mid =\sigma (k)$, so $B\mathrm{\ne }\mathrm{\varnothing }$; fix $b\in B$ and put $B^{\mathrm{\prime }}:=B\setminus \{b\}$, which is finite with $\mid B^{\mathrm{\prime }}\mid =k$ by [L4], [L5] and cancellation, exactly as in the count of $A^B$. Put $T:=\{(g,a):g\in \mathrm{Inj}(B^{\mathrm{\prime }},A),a\in A\setminus g[B^{\mathrm{\prime }}]\}$ and define $\mathrm{\Phi }:\mathrm{Inj}(B,A)\to T$ by $\mathrm{\Phi }(f)=(f\upharpoonright B^{\mathrm{\prime }},f(b))$; this lands in $T$ because $f\upharpoonright B^{\mathrm{\prime }}$ is injective and $f(b)\mathrm{\ne }f(x)$ for $x\in B^{\mathrm{\prime }}$, so $f(b)\mathrm{\notin }f[B^{\mathrm{\prime }}]$. The map $(g,a)\mapsto g\cup \{(b,a)\}$ is a two-sided inverse: the extension is injective precisely because $a\mathrm{\notin }g[B^{\mathrm{\prime }}]$. So $\mathrm{\Phi }$ is a bijection. Finally $\mathrm{Inj}(B^{\mathrm{\prime }},A)\subseteq A^{B^{\mathrm{\prime }}}$ is finite by [L4].

The case $k>n$. Then $n^{\underset{‾}{k}}=0$ by [L3], so the hypothesis of step 1.2 gives $\mid \mathrm{Inj}(B^{\mathrm{\prime }},A)\mid =0$, that is $\mathrm{Inj}(B^{\mathrm{\prime }},A)=\mathrm{\varnothing }$; hence $T=\mathrm{\varnothing }$ and $\mathrm{Inj}(B,A)=\mathrm{\varnothing }$ by step 1.3, so its cardinality is $0$. And $\sigma (k)>n$ as well, so $n^{\underset{‾}{\sigma (k)}}=0$ by [L3]. Both sides are $0$.

The case $k\le n$. For each $g\in \mathrm{Inj}(B^{\mathrm{\prime }},A)$ the image $g[B^{\mathrm{\prime }}]$ is a subset of $A$ with $\mid g[B^{\mathrm{\prime }}]\mid =\mid B^{\mathrm{\prime }}\mid =k$, since $g$ is a bijection onto its image; and $A$ is the disjoint union of $g[B^{\mathrm{\prime }}]$ and $A\setminus g[B^{\mathrm{\prime }}]$, so $n=k+\mid A\setminus g[B^{\mathrm{\prime }}]\mid$ by [L5] and therefore $\mid A\setminus g[B^{\mathrm{\prime }}]\mid =n-k$ by [L7]. Now $T$ is the union of the pairwise disjoint sets $\{g\}\times (A\setminus g[B^{\mathrm{\prime }}])$ indexed by $g\in \mathrm{Inj}(B^{\mathrm{\prime }},A)$, each of cardinality $n-k$ because $a\mapsto (g,a)$ is a bijection; so [L5] gives $\mid T\mid ={\sum }_g(n-k)=\mid \mathrm{Inj}(B^{\mathrm{\prime }},A)\mid \cdot (n-k)=n^{\underset{‾}{k}}\cdot (n-k)=n^{\underset{‾}{\sigma (k)}}$, using the hypothesis of step 1.2 and [L3]. With step 1.3 this is $\mid \mathrm{Inj}(B,A)\mid$.

The two cases are exhaustive by trichotomy, so the statement holds at $\sigma (k)$ whenever it holds at $k$; with step 1.1 it holds for every $k$, and the two boundary readings are step 1.1 and step 2.1.