theorem Th7: :: GROUP_11:7

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