theorem Th25: :: GROUP_6:25

for G being Group
for a being Element of G
for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N