theorem Th60: :: GROUP_3:60
for G being Group
for a, b being Element of G
for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)