theorem Th1: :: GROUP_20:1

for G being Group
for H being normal Subgroup of G
for x, y being Element of G st y in H holds
( (x * y) * (x ") in H & x * (y * (x ")) in H )