theorem Th128: :: GROUP_2:128

for G being Group
for a, b being Element of G
for H being Subgroup of G holds a * H,b * H are_equipotent