theorem :: GROUP_11:46

for G being Group
for A being non empty Subset of G
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) )