Tangent bundle of a product diffeom. to the product of tangent bundle. I have to prove that $T(M \times N) \cong T(M) \times T(N)$. 
I think I found a map but I cannot prove that is a diffeomorphism. 
That is the map :
$F : T(M \times N) \to T(M) \times T(N)$ defined by $F((m,n),X) = ((m,(\pi_{1})_{\star,(m,n)}(X)),(n,(\pi_{2})_{\star,(m,n)}(X)))$
where $\pi_1 : M \times N \to M$ and $ \pi_2 : M \times N \to N$ are the projections and the "little star" represent the push-forward.
I might be wrong but, since projections are submersions, the map is surjective and it's also injective from a direct check. So it's enought to check that is a local diffeomorphism or that is $C^\infty$ with a $C^\infty$ inverse. There is a way to show this without using local charts? I've tried with local charts on $T(M\times N)$ induced by charts on M and N but nothing came out. 
 A: Now the idea using local charts I think is the following :
Let $(U,\phi)$ be a local chart for $M$ , $(V,\psi)$ be a local chart for $N$, and so $(U\times V,\Phi:= \phi\times \psi)$ is a local chart for $M\times N$ by definition, and $(TU, \tilde \phi)$ $(TV,\tilde \psi)$ $(T(U\times V), \tilde\Phi)$ will be the induced local charts in $TM, TN $ and $T(M\times N)$. Now the same way you constructed $F$ it is easy to construct $F^{-1}$ using the inclusions instead of the projections and now the only problem is to check that this maps are in fact smooth. Now I will do this for $F$, and $F^{-1}$ is analogous.
So in these local charts we have that $(\tilde \phi\times \tilde \psi)\circ F\circ(\tilde \Phi)^{-1}(x_1,...x_m,y_1,...,y_n,\epsilon_1,...\epsilon_m,\eta_1,...,\eta_n)=\\= (\tilde \phi\times \tilde \psi)\circ F(\phi^{-1}(x_1,...x_m),\psi^{-1}(y_1,...,y_n),\epsilon_1,...,\epsilon_m,\eta_1,...,\eta_n)=\\=(\tilde\phi\times \tilde \psi)(\phi^{-1}(x_1,...x_m),\epsilon_1,...,\epsilon_m,\psi^{-1}(y_1,...,y_n),\eta_1,...,\eta_n)=\\
=(x_1,...,x_m,\epsilon_1,...\epsilon_m,y_1,...,y_n,\eta_1,...,\eta_n)$
Now to clarify what is happening when we apply $F$  at the tangent vector that this $v=\epsilon_1 \frac{\partial}{\partial x_1}+...+\epsilon_n \frac{\partial}{\partial x_n}+...+\eta_1 \frac{\partial}{\partial y_1}+...+\eta_n \frac{\partial}{\partial y_n}$, we need to look at the diferentials $d\pi_1$ and $d\pi_2$. I will only look at one of them since the other is analogous. So for example at $d\pi_1(\frac{\partial}{\partial x_i})=\sum_{j=1}^{m}\frac{(\phi\circ \pi_1 \circ (\phi\times \psi)^{-1} )^j}{\partial x_i}\frac{\partial }{\partial x_j}=\frac{\partial}{\partial x_i}$, and $d\pi_1(\frac{\partial}{\partial y_i})=\sum_{j=1}^{m}\frac{(\psi\circ \pi_1 \circ (\phi\times \psi)^{-1} )^j}{\partial y_i}\frac{\partial }{\partial x_j}=0$.
