theorem Th116: :: GROUP_2:116

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