Formal Proof of Exponential rule I tried to prove this, but was unsuccessful for a long time.. 
Any ideas?
Prove that $(\exp(x))^y=\exp(xy)$ using the identities, 
$$\exp(x)=\sum_{n\geq0} \frac{x^n}{n!}, \quad (1+x)^\alpha=\sum_{n\geq0} {\alpha \choose n} x^n$$
 A: One can prove the sought power series equality via the uniqueness theorem for first-order ODE's. It's easy to show that both power series satisfy $\rm\ f'(x) = y\ f(x),\ \ f(0) = 1\:.\ $ Put $\rm\ f(x) = \sum_{n \ge 0} \frac{x^n y^n}{n!},\:$  
$\rm\quad\displaystyle\ \ g(x)\ =\ \sum_{n \ge 0}\ \ {y \choose n}\ (\exp(x) - 1)^n\:.\ \ $ Clearly $\rm\:f\:$ satisfies the ODE. $\ $ For $\rm\:g\:$ we have  
$\rm\quad\displaystyle\ g'(x)\ =\ \sum_{n \ge 1}\ n\: {y \choose n}\ exp(x)\ (\exp(x) - 1)^{n-1}$  
$\rm\displaystyle\quad\quad\quad\quad\quad =\ y\ \exp(x)\ \sum_{n \ge 1}\ {y-1\choose n-1}\ (\exp(x)-1)^{n-1}$  
$\rm\displaystyle\quad\quad\quad\quad\quad =\ y\ \exp(x)\ \sum_{n \ge 0}\ {y-1\choose n}\   (\exp(x)-1)^n $  
$\rm\displaystyle\quad\quad\quad\quad\quad =\ y\ \exp(x)\ {\exp(x)}^{y-1}$  
$\rm\displaystyle\quad\quad\quad\quad\quad =\ y\ g(x)$
NOTE $\ $ The above is simply $\rm\ (exp(x)^y)' =\ y\ exp(x)\ exp(x)^{y-1}\ $ expressed in power series form. Note that the coefficient identity at the core is the same binomial identity as a couple days ago, viz.
$\rm\displaystyle\quad\quad\quad\quad\quad\  {y \choose n}\ =\ \frac{y}{n}\ {y-1\choose n-1}$
A: I'll assume you want an equality of formal power series
$$\sum_{n \ge 0} \frac{x^n y^n}{n!} = \sum_{n \ge 0} {y \choose n} (\exp(x) - 1)^n.$$
The proof of this is easier to explain combinatorially than via series manipulation, if you allow me to first assume that $y$ is a non-negative integer.  In that case I claim that the coefficient of $\frac{x^n}{n!}$ on the RHS is the number of functions from $[n]$ to $[y]$ (where $[k] = { 1, 2, ... k }$), which is clearly $y^n$.
To see this, note that $\exp(x) - 1$ is the exponential generating function for non-empty sets, hence $(\exp(x) - 1)^k$ is the exponential generating function for partitions of a set into $k$ non-empty blocks, and ${y \choose k}$ is the number of ways to choose $k$ elements out of $y$ elements.  But a function from $[n]$ to $[y]$ is nothing more than a partition of $[n]$ into $k$ non-empty blocks (the preimages of each element of the range), together with a choice of $k$ elements of $[y]$ (the image of each of the blocks).  
To see how this implies the identity for arbitrary $y$, note that the coefficient of $\frac{x^n}{n!}$ on the RHS (regarded as a formal power series in $x$ and $y$) must be a polynomial of degree at most $n$, and this polynomial agrees with $y^n$ for all non-negative integers, so it must be identically equal to $y^n$.  (What I've proven essentially amounts to the inversion formulas relating the Stirling numbers of the first and second kinds.)
If you want a proof without this extra simplification then you need to do some messy inclusion-exclusion or some messy series manipulation and I don't really see the point either way.
