theorem :: GROUP_6:22

for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( N * a is Element of (G ./. N) & a * N is Element of (G ./. N) & carr N is Element of (G ./. N) ) by Th14, GROUP_2:135;