theorem Th60: :: GROUP_1A:261

for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (H * a) * b = H * (a + b)