theorem :: GROUP_2:97

for G being Group
for A, B being Subset of G
for H being Subgroup of G holds (A * H) * B = A * (H * B) by Th10;