The set $A^B$ of functions $B\to A$ between finite sets is finite, with $\mid A^B\mid =\mid A{\mid }^{\mid B\mid }$

Base case $\mid B\mid =0$. Then $B=\mathrm{\varnothing }$ by [L2], and a function $\mathrm{\varnothing }\to A$ is the empty function, of which there is exactly one whatever $A$ is; so $A^B=\{\mathrm{\varnothing }\}$, which is finite with cardinality $1$ because $0\mapsto \mathrm{\varnothing }$ is a bijection of $1=\{0\}$ onto it. And $\mid A{\mid }^0=1$ by [L5].

Inductive hypothesis: fix $n\in \mathbb{N}$ and assume that for every finite $A$ and every finite $B^{\mathrm{\prime }}$ with $\mid B^{\mathrm{\prime }}\mid =n$ the set $A^{B^{\mathrm{\prime }}}$ is finite with $\mid A^{B^{\mathrm{\prime }}}\mid =\mid A{\mid }^n$.

Inductive step. Let $\mid B\mid =\sigma (n)$. Then $B\mathrm{\ne }\mathrm{\varnothing }$ by [L2], so fix $b\in B$ and put $B^{\mathrm{\prime }}:=B\setminus \{b\}$, which is finite by [L7]. Since $B=B^{\mathrm{\prime }}\cup \{b\}$ with $B^{\mathrm{\prime }}\cap \{b\}=\mathrm{\varnothing }$ and $\mid \{b\}\mid =1$, [L3] gives $\sigma (n)=\mid B^{\mathrm{\prime }}\mid +1$, hence $\mid B^{\mathrm{\prime }}\mid =n$ by cancellation. Define $\mathrm{\Psi }:A^B\to A^{B^{\mathrm{\prime }}}\times A$ by $\mathrm{\Psi }(f)=(f\upharpoonright B^{\mathrm{\prime }},f(b))$; its inverse is $(g,a)\mapsto g\cup \{(b,a)\}$, which is a function on $B^{\mathrm{\prime }}\cup \{b\}=B$ because $b\mathrm{\notin }{B}^{\mathrm{\prime }}$, and the two composites are the identity, so $\mathrm{\Psi }$ is a bijection. By the hypothesis of step 1.2 and by [L4] the codomain is finite with cardinality $\mid A{\mid }^n\cdot \mid A\mid =\mid A{\mid }^{\sigma (n)}$, and transport carries this to $A^B$.

By induction on $\mid B\mid$ the statement holds for every pair of finite sets $A$, $B$.

The two degenerate readings are instances of it: $B=\mathrm{\varnothing }$ gives $1=\mid A{\mid }^0$ by step 1.1, valid for $A=\mathrm{\varnothing }$ as well; and $A=\mathrm{\varnothing }$ with $\mid B\mid \ge 1$ gives $\mid A^B\mid =0^{\mid B\mid }=0$, which is right because a function $B\to \mathrm{\varnothing }$ would have to supply a value in $\mathrm{\varnothing }$ for some element of $B$.