Normal Subgroup of Product of Groups

In [6] it was formalized that the direct product of a family of groups gives a new group. In this article, we formalize that for all j ∈ I, the group G = Π_i∈IG_i has a normal subgroup isomorphic to G_j. Moreover, we show some relations between a family of groups and its direct product.