Uniqueness of morphism (reasoning in categorial language). This question is related to a previous question of mine.
I figured out that maybe the right thing to ask for is for someone to solve one of the problems in Aluffi's book, that way I’ll know what the reasoning should look like.
The following question appears in section 2.3 of Aluffi's book:

Let $\varphi: G \to H$ be a morphism in a category with products.
Explain why there is a unique morphism
$$(\varphi \times \varphi): G \times G \to H \times H.$$
compatible in the evident way with the natural projections.
Next let $\psi: H \to K$ be a morphism in the same category and
consider morphisms between the products $G \times G, H \times H, K \times K$.
Prove: $$(\psi \varphi) \times (\psi \varphi) = (\psi \times \psi)(\varphi \times \varphi).$$

How should a thorough rigorous answer to this question look like? Answers with diagrams are preferred (since this is a major part i still don't get).
Please don't leave any holes in reasoning unless they are totally obvious and if you use diagrams please explain how you reason with them.
I'd like to emphasis that I'm not at all asking this question out of laziness. I'm finding myself a bit lost in this new language and in need of guidance.
Big pluses to anyone who would make me understand the big picture and make it all feel like a bad dream.
 A: Let's call $\pi_1 \colon G \times G \to G$ and $\pi_2 \colon G \times G \to G$ the two projections of the product $G\times G$.
Let $p_1 \colon H \times H \to H$ and $p_2 \colon H \times H \to H$ be the projections of the product $H \times H$.
Finally let $q_1 \colon K \times K \to K$ and $q_2 \colon K \times K \to K$ be the projections for the product $K\times K$.
The evident way in which the morphism $\varphi \times \varphi$ should be compatible with the projections of the two products is expressed by the following equations
$$p_1 \circ \varphi \times \varphi = \varphi \circ \pi_1$$
$$p_2 \circ \varphi \times \varphi = \varphi \circ \pi_2$$
The existence of such morphisms $\varphi \times \varphi$ comes from the universal property of the product $H\times H$ which tells that for the pair $\varphi \circ \pi_1,\varphi \circ \pi_2 \colon G\times G \to H$
there's a unique $\varphi \times \varphi \colon G \times G \to H \times H$ which satisfies those equations.
To solve the second problem we can observe that we just proved that for every homomorphism $\varphi \colon G \to H$ the morphism $\varphi \times \varphi \colon G \times G \to H \times H$ is given by the universal property above.
To verify that for $\varphi \colon G \to H$ and $\psi \colon H \to K$ we have that 
$$\psi \circ \varphi \times \psi \circ \varphi = (\psi \times \psi) \circ (\varphi \times \varphi)$$ 
we just need to prove that $(\psi \times \psi) \circ (\varphi\times \varphi)$ verifies the corresponding equation expressing the universal property.
Namely we have to verify that 
$$q_1 \circ (\psi \times \psi) \circ (\varphi\times \varphi) = \psi \circ \varphi \circ \pi_1$$
and 
$$q_2 \circ (\psi \times \psi) \circ (\varphi\times \varphi) = \psi \circ \varphi \circ \pi_2$$
By what said above $q_1 \circ (\psi \times \psi)=\psi \circ p_1$
and $q_2 \circ (\psi \times \psi)=\psi \circ p_2$ 
so 
$$q_1 \circ (\psi \times \psi) \circ (\varphi\times \varphi) = \psi \circ p_1 \circ (\varphi \times \varphi)$$
which is equals to $\psi \circ \varphi \circ \pi_1$ (because $p_1 \circ(\varphi \times \varphi)=\varphi \circ \pi_1$).
In similar way you can prove the other equality.
Hope this helps.
A: To give map to the product $H\times H$ is exactly the same as giving a pair of maps to each of the factors, i.e. a pair of maps $f_1,f_2: G\times G \to H.$
(This is the definition of the categorical product: a map to the product is determined by its composite with each of the projections.)
We are requiring that the map $G\times G \to H \times H$ be compatible with
the projections, and so we have no choice but to define $f_i$ to be the composite 
of the $i$th projection $G\times G \to G$, and the given morphism $G \to H$.
Putting this all together, we've proved existence and uniqueness.

I'm not sure that diagrams are particularly helpful here.  The main point is
to understand how to give a map to the categorical product (i.e. by definition, you have to give a map to each factor), and then to understand
(in this particular case, or any particular case you might be dealing with) what the 
maps to the factor should be.
A: The question isn't right.  There isn't a unique morphism $G\times G\to H\times H$, there's a unique morphism... with such and such properties.
I recommend beginning your thinking in the category of sets.  If I have a map of sets $G\to H$, is there a "natural" map $G\times G \to H\times H$ that springs to mind?  Is there some special property that distinguishes this map from any other?
