theorem Th8: :: GROUPP_1:8

for G being Group
for N being normal Subgroup of G
for a being Element of G
for S being Element of (G ./. N) st S = a * N holds
for n being Nat holds S |^ n = (a |^ n) * N