theorem Th4: :: GROUP_11:4

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