theorem :: GROUP_11:62

for G being Group
for H1, H2 being Subgroup of G
for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)