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?
 A: In arbitrary categories, there is a notion of "generalized element": A generalized element of an object $A$ is any morphism into $A$ (from any object of the category). A morphism $A\to B$ can be applied to a generalized element $Z\to A$ just by composing them to get a generalized element $Z\to B$. In these terms, the result you want can be proved: A generalized element of $\prod_iX_i$ is determined by its images under all the projections $\pi_i$. But "proved" here is too grandiose a term; this fact is just part of the categorical definition of product.
A: 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.
