The universal property of the direct product of groups is a particular case of the universal property of the product in a category

Question

I have posted here quite a bit on different ways of stating the universal property of the direct product and of the direct sum of (abelian) groups. Once again, I have a question which most likely comes from the fact that I am only a beginner when it comes to category theory.
Is it correct to say that the universal property of the direct product of groups is a particular case of the universal property of the product in a category? In this post A question on the universal property of the direct sum of abelian groups I learnt that stating the universal property of the direct sum of abelian groups is a particular case of the universal property of the coproduct. That's why I assume that the same conclusion is valid if we change the coproduct to the product. But I would like to understand why this is correct. Isn't the universal property of the product in a category just a definition? I think that the universal property of the direct product of groups needs to be proved, so it may be regarded as a theorem. How can a theorem be a particular case of a definition? I am sorry if this is all obvious/trivial, but I really want to understand this.
EDIT: I thought about this now, let me know if I am correct. We may also define the direct product of groups through its universal property. In this way, this is no longer a theorem. And I guess that from here we may deduce that the direct product of groups can be presented the way we are used with it.

Answer 1

The universal property of the direct product of groups is precisely the universal property in the category of groups $\mathbf{Grp}$.

But as you should remember, an universal property does tell us the existence of an object! On the other hand, once we have found an object that satisfies the universal property, then it is the unique object up to unique isomorphism that satisfies the universal property - which is why we may speak of the product if it exists.

So in our particular case, we explicitly construct the direct product of groups $G \times H$ and then prove that it satisfies the universal property of products in $\mathbf{Grp}$. Only then can we feel confident to call $G \times H$ product and sleep at ease at night.