theorem Th1: :: GROUP_11:1

for G being Group
for N being normal Subgroup of G
for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N