theorem :: GROUP_3:7

for G being Group
for a being Element of G
for H being Subgroup of G holds a * H = {a} * H ;