Morphisms in a category with products I'm having a hard time proving that
$$(\psi\phi)\times(\psi\phi)=(\psi\times\psi)(\phi\times\phi),$$
where $\phi:G\to H$ and $\psi:H\to K$ in some category with products. I have seen a diagram of this (see below) and it seems straightforward. But I can't manage this computation it seems. How is it done?

 A: The result holds much more generally.
I think that this ProofWiki proof (which I coincidentally provided to PW myself) will provide what you need (you can follow some links to see the definitions).
Normally, I would include the argument, but there is no support for drawing the diagrams here, which makes everything much less insightful.

As per request, an attempt to clarify commutation of the top "triangle" in OPs diagram.
By definition, the morphism $(\psi\phi)\times(\psi\phi)$ is the unique (by virtue of the definition of the categorical product) morphism $f: G \times G \to K \times K$ such that:
$$\pi^1_K f = (\psi\phi)\pi^1_G\qquad\text{and}\qquad\pi^2_K f = (\psi\phi)\pi^2_G$$
where $\pi^i_K: K \times K \to K$ and $\pi^i_G: G \times G \to G$, $i=1,2$ are the first and second projection morphisms from the product (which are signified by $m_G$ and $m_K$ in your diagram, dropping the $1$ and $2$ since they're "identical").
The commutation of the two middle squares implies that the perimeter of the resulting rectangle commutes as well, i.e. $m_K\left((\psi\times\psi)(\phi\times\phi)\right) = (\psi\phi)m_G$. 
That is, $(\psi\times\psi)(\phi\times\phi)$ is a morphism fitting the definition of $(\psi\phi)\times(\psi\phi)$. Since there was only one such morphism, they must be equal, and the top "triangle" commutes.
Note that this is in essence the same proof as given on the ProofWiki page. 
A: Sometimes it is far more easy just to compute things instead of drawing large diagrams(*). Recall that $\phi \times \psi$ is defined by $p_1 \circ (\phi \times \psi) = \phi \circ p_1$ and $p_2 \circ (\phi \times \psi)=\psi \circ p_2$.
Let $\phi_i : G_i \to H_i$ and $\psi : H_i \to K_i$ homomorphisms of groups for $i=1,2$. We claim that $(\psi_1  \times \psi_2)  \circ (\phi_1 \times \phi_2) = (\psi_1 \circ \phi_1) \times (\psi_2 \circ \phi_2)$ as morphisms $G_1 \times G_2 \to K_1 \times K_2$.
Proof: It suffices to check this after composing with the two projections.
$p_1 \circ (\psi_1  \times \psi_2)  \circ (\phi_1 \times \phi_2)
=\psi_1 \circ p_1 \circ (\phi_1 \times \phi_2)
=\psi_1 \circ \phi_1 \circ p_1
= p_1 \circ ((\psi_1 \circ \phi_1) \times (\psi_2 \circ \phi_2))$
Similarily for $p_2$, QED.
More generally, limits are functorial in the following sense: If $\{G_i\},\{H_i\},\{K_i\}$ are diagrams in a category, whose limits exist, and $\phi : \{G_i\} \to \{H_i\}$, $\psi : \{H_i\} \to \{K_i\}$ are morphisms of diagrams, then $\lim_i (\psi_i \circ \phi_i) = \lim_i \psi_i \circ \lim_i \phi_i$ as morphisms $\lim_i G_i \to \lim_i K_i$. The same proof as above works.
(*) I have already come across several papers on category theory such as the early ones by Anders Kock containing long (and nontrivial, not something as above) computations with 10 lines, which would fill two pages of diagrams instead.
