theorem :: GROUP_3:13

for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 * a) * H2 = H1 * (a * H2) by Th9;