theorem Th130: :: GROUP_2:130

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