theorem Th122: :: GROUP_2:122

for G being Group
for a, b being Element of G
for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)