theorem Th10: :: GROUP_11:10

for G being Group
for N, N1, N2 being normal Subgroup of G
for a, b being Element of G st the carrier of N = N1 * N2 holds
(a * N1) * (b * N2) = (a * b) * N