Formalizing composition of sequences The following first equality is intuitively evident:
$$
\lim_{n\to \infty} \left(1+\frac{x+y+\frac{xy}{n}}{n}\right)^n 
= \lim_{n\to \infty} \left(1+\frac{x+y}{n}\right)^n
=e^{x+y}
$$
how can I give a formal argument?
Informally it is something like
$$
\lim_{n\to \infty} \left(1+\frac{x+y+\frac{xy}{n}}{n}\right)^n 
=\lim_{n\to \infty} \left(1+\frac{\lim_{n\to \infty}\left(x+y+\frac{xy}{n}\right)}{n}\right)^n 
=\lim_{n\to \infty} \left(1+\frac{x+y}{n}\right)^n 
$$
Is there a "classical" property of sequences that backs this argument? Something like limit of composition, but here we speak of sequence only:
$$
(b_n),\quad b_n \to b\quad\text{ for }n\to\infty \implies 
\lim_{n\to \infty} \left(1+\frac{b_n}{n}\right)^n
=\lim_{n\to \infty} \left(1+\frac{b}{n}\right)^n
$$
EDIT As Qiaochu Yuan is important to define what I have already defined.
This computation is at the beginning of "Real Analysis", lets say in the chapter of sequences. Later, in the notes of complex analysis, I develop formal series with derivation and everything is the standard way (I think).
By this question I tried another approach, very early (1) define
$$
e^x = \lim_{n\to\infty}\left(1+\frac{x}{n}\right)^n
$$
(2) derive the product as depicted in this question
(3) derive the derivation of the $e^x$.
Thus I have (a) no logarithm, (b) no derivation of $e^x$ yet.
 A: You can use the basic fact that for any sequence $c_n \stackrel{n\to\infty}{\longrightarrow}0$ $(c_n \neq 0)$ you have
$$\left(1+c_n\right)^{\frac 1{c_n}}\stackrel{n\to\infty}{\longrightarrow}e$$
So with $c_n =\frac{b_n}n$ and $b_n \stackrel{n\to\infty}{\longrightarrow}b$, you get
\begin{eqnarray*} \left(1+c_n\right)^n
& = & \left(\left(1+c_n\right)^\frac 1{c_n}\right)^{c_n\cdot n}\\
& = & \left(\left(1+c_n\right)^\frac 1{c_n}\right)^{b_n} \\
& \stackrel{n\to\infty}{\longrightarrow} & e^b
\end{eqnarray*}
Here the continuity of $f(x,y) = x^y$ in both variables $x$ and $y$ is used which can easily be established considering,for example, first the logarithm of this function.
Hence, you have
$$\lim_{n\to\infty} \left(1+\frac{b_n}n\right)^n=e^b = \lim_{n\to\infty} \left(1+\frac{b}n\right)^n$$
A: The desired statement is true. It follows from taking logarithms and writing
$$\begin{eqnarray*} \log \left( 1 + \frac{b_n}{n} \right)^n &=& n \log \left( 1 + \frac{b_n}{n} \right) \\
 &=& n \left( \frac{b_n}{n} + O \left( \frac{b_n^2}{n^2} \right) \right) \\
 &=& b_n + O \left( \frac{b_n^2}{n} \right). \end{eqnarray*}$$
Taking the limit as $n \to \infty$ gives that the limit of the logarithms is $\lim_{n \to \infty} \left( b_n + O \left( \frac{b_n^2}{n} \right) \right) = b$ (using that $b_n$ is convergent and hence bounded, so the $O \left( \frac{b_n^2}{n} \right)$ term vanishes in the limit).
Depending on how you've defined exponentials and logarithms and proven their properties this argument may be circular, since it depends on the first two terms of the Taylor series of the logarithm, and one of several ways to compute the Taylor series of the logarithm is to use $\log xy = \log x + \log y$ which is more or less equivalent to $e^{x+y} = e^x e^y$.
There are alternatives for proving that $e^{x + y} = e^x e^y$ which avoid having to prove this; for example, taking for granted that $\frac{d}{dx} e^x = e^x$ and $e^0 = 1$ (which together uniquely determine $e^x$ by the existence and uniqueness theorems for ODEs), we have first
$$\frac{d}{dx} (e^x e^{-x}) = e^x e^{-x} - e^x e^{-x} = 0$$
so $e^x e^{-x}$ is a constant, and plugging in $x = 0$ gives $e^x e^{-x} = 1$. Next,
$$\frac{d}{dx} \left( e^{x+y} e^{-x} e^{-y} \right) = e^{x+y} e^{-x} e^{-y} - e^{x+y} e^{-x} e^{-y} = 0$$
so $e^{x+y} e^{-x} e^{-y}$ is a constant in $x$, and plugging in $x = 0$ gives $e^y e^{-y} = 1$ and hence $e^{x+y} = e^x e^y$.
A: Another approach: Note that
$$\left(1+\frac{x+y+\frac{xy}{n}}{n}\right)^n 
= \left(1+\frac x n\right)^n\left(1+\frac y n\right)^n.$$
Addendum
We have that
\begin{align*}
\left(\frac{1+\frac{x+y+\frac{xy}{n}}{n}}{1+\frac{x+y}{n}}\right)^n
&= \left(
\frac{\left(1+\frac x n\right)\left(1+\frac y n\right)}{1+\frac{x+y}{n}}\right)^n 
\longrightarrow \frac{e^x e^y}{e^{x+y}} \quad(n\to\infty).
\end{align*}
It remains to show that this limit is unity.
See this answer, for example.
