theorem Th7: :: GROUPP_1:7

for G being Group
for N being Subgroup of G
for a, b being Element of G st N is normal & b in N holds
for n being Nat ex g being Element of G st
( g in N & (a * b) |^ n = (a |^ n) * g )