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∈IGi has a normal subgroup isomorphic to Gj. Moreover, we show some relations between a family of groups and its direct product.