Currying law for cardinal exponentiation (source code)

= Currying law for cardinal exponentiation

There is a natural <bijection> between functions $M\to K^L$ and functions $M\times L\to K$, obtained by sending $f$ to $(m,l)\mapsto f(m)(l)$. Therefore
$$
(\kappa^\lambda)^\mu=\kappa^{\lambda\mu}.
$$