theorem Th8: :: GROUP_11:8

for G being Group
for N1, N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2