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)