theorem :: GROUP_2:96

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