theorem Th9: :: GROUP_3:9

for G being Group
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (A * a) * H = A * (a * H)