(From Awodey) Prove $(A\times B)^C\cong A^C\times B^C$ This is an exercise from Awodey's category theory, namely exercise 2 in Chapter 6.

Prove $(A\times B)^C\cong A^C\times B^C$

The following is the solution in the textbook:

(Please ignore the "$g$" stuffs )
Once I encountered this problem, the first idea of mine is to define $f:(A\times B)^C \to A^C\times B^C$ as $\alpha(\in (A\times B)^C)\mapsto (\pi_1\circ \alpha,\pi_2\circ \alpha)$ where the $\pi$'s are projections.
And I can take the inverse to be $(p\in A^C,q\in B^C)\mapsto (c\mapsto (p(c),q(c)))$ I wonder if my thoughts are doable.
The solution given in the textbook seems more complicated, trying to understand it, I chased the map defined here, I checked it for the $f$ part and the output consists with the map I defined.
But I just realized something that let me feel very worry: What I did is defining a map, not a general arrow. And when I chased the diagram, I took $A^C$ to be the collection of maps $C\to A$, but I think I cannot do like this because exponential is not defined as a collection of maps or even arrows, it is defined as an object which satisfies the UMP of exponential, we do not know how does its "elements" looks like.
So the following is what I am asking about:
Any comment to my thoughts above? I am self-studing. Any guidence would be very appreciate.
If possible, could someone gives a detailed procedure of chasing the definition of the arrow $f$ to show that it is an isomorphism?
Thanks!
 A: This doesn't directly answer your question, but it's another way to approach questions like this (if you know Yoneda's Lemma).
Look at $\mathrm{Hom}(X,A)$ or $\mathrm{Hom}(A,X)$ for an arbitrary object $X$, and use universal properties of $A$ and $B$ to show that this is naturally isomorphic to $\mathrm{Hom}(X,B)$ or $\mathrm{Hom}(B,X)$. Then it follows that $A\cong B$ by Yoneda's Lemma.
In this case, for any object $X$, we have the chain of natural isomorphisms:
\begin{align*}
\mathrm{Hom}(X,(A\times B)^C) &\cong \mathrm{Hom}(X\times C,A\times B)\\
&\cong \mathrm{Hom}(X\times C,A)\times \mathrm{Hom}(X\times C,B)\\
&\cong \mathrm{Hom}(X,A^C)\times \mathrm{Hom}(X,B^C)\\
&\cong \mathrm{Hom}(X,A^C\times B^C)
\end{align*}
So by Yoneda's Lemma, $(A\times B)^C \cong A^C\times B^C$. 
A: In order to prove that $ff^{-1} = 1_{A^C \times B^C}$ and $f^{-1}f = 1_{(A \times B)^C}$, we need the following lemma:

Lemma. For any $f \colon Y \times C \to Z$ and $g\colon X \to Y$,
  $$\lambda f g = \lambda(f (g \times 1_C)).$$

For a proof of the lemma see this answer by Hanno to a previous question.
Now we can prove that $f$ is an isomorphism. The first direction:
\begin{align}
f f^{-1} & = \langle \lambda (\pi_1 \overline{1_{(A \times B)^C}}), \lambda (\pi_2 \overline{1_{(A \times B)^C}}) \rangle \lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle \\
& = \langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle \lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle \\
& = \langle \lambda (\pi_1 \epsilon) \lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle, \lambda (\pi_2 \epsilon) \lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle \rangle \\
& = \langle \lambda (\pi_1 \epsilon (\lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle \times 1_C)), \lambda (\pi_2 \epsilon (\lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle \times 1_C)) \rangle \\
& = \langle \lambda (\pi_1 \overline{\lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle}), \lambda (\pi_2 \overline{\lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle}) \rangle \\
& = \langle \lambda (\pi_1 \langle \overline{\pi_1}, \overline{\pi_2} \rangle), \lambda (\pi_2 \langle \overline{\pi_1}, \overline{\pi_2} \rangle) \rangle \\
& = \langle \lambda \overline{\pi_1}, \lambda \overline{\pi_2} \rangle \\
& = \langle \pi_1, \pi_2 \rangle \\
& = 1_{A^C \times B^C}.
\end{align}
The other direction:
\begin{align}
f^{-1} f & = \lambda \langle \overline{\pi_1}, \overline{\pi_2} \rangle \langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle \\
& = \lambda (\langle \overline{\pi_1}, \overline{\pi_2} \rangle (\langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle \times 1_C)) \\
& = \lambda (\langle \overline{\pi_1} (\langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle \times 1_C), \overline{\pi_2} (\langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle \times 1_C) \rangle) \\
& = \lambda (\langle \epsilon (\pi_1 \times 1_C) (\langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle \times 1_C), \epsilon (\pi_2 \times 1_C) (\langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle \times 1_C) \rangle) \\
& = \lambda (\langle \epsilon ((\pi_1 \langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle) \times 1_C), \epsilon ((\pi_2 (\langle \lambda (\pi_1 \epsilon), \lambda (\pi_2 \epsilon) \rangle) \times 1_C) \rangle) \\
& = \lambda (\langle \epsilon (\lambda (\pi_1 \epsilon) \times 1_C), \epsilon (\lambda (\pi_2 \epsilon) \times 1_C) \rangle) \\
& = \lambda (\langle \overline{\lambda (\pi_1 \epsilon)}, \overline{\lambda (\pi_2 \epsilon)} \rangle) \\
& = \lambda (\langle \pi_1 \epsilon, \pi_2 \epsilon \rangle) \\
& = \lambda (\langle \pi_1, \pi_2 \rangle \epsilon) \\
& = \lambda \epsilon \\
& = 1_{(A \times B)^C}.
\end{align}
