theorem Th129: :: GROUP_2:129

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