theorem :: GROUP_1A:325

for G being addGroup
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = (carr N1) + (carr N2)