Proof that equality on categorical products is componentwise equality I want to proof that in the categorical product as defined here it holds that
for $x,y \in \prod X_i$ then
$$
 x = y \textrm{ iff } \forall i \in I : \pi_i(x) = \pi_i(y).
$$
The direction from left to right is trivial, but the other, that iff the components equal than their product is equal I am not able to proof, I tried to substitute the identity morphisms in the universal property, but I always get the wrong "types" in the functions involved. Any hints?

As in a general category there is no meaning to membership in an object, one needs to carefully interpret what is meant. The usual way to go about it is to use generalized elements. A generalized element in a category is simply a morphism $fx:A\to B$ in it, just we think of it as being an element of $B$ of type $A$. In particular, when $A$ is a terminal object, such generalized elements are called global elements. In familiar categories such as $Set$ or $Top$ but not $Grp$ or $Ring$) global elements $*\to A$ correspond precisely to the actual elements in the underlying set of the object $A$. 
Note that if $x:A\to B$ is a generalized element and $f:B\to C$ is a morphism, then defining $f(x)$ to mean $f\circ x$ turns every morphism into a function on generalized elements that preserves types. In particular, every morphism $f:B\to C$ gives rise to a function from the global elements of $B$ to the global elements of $C$.
Now, if $B\prod C$ is a product in the category, then a global element $x$ of it of type $A$ is a morphism $x:A\to B\prod C$, and thus corresponds bijectively and naturally to a pair of morphisms $A\to B$ and $A\to C$. In other words, for each type $A$, there is a natural bijection between the generalized elements of $A$ of the product $B\prod C$ and pairs of generalized elements of type $A$ of each component.
