theorem Th131: :: GROUP_2:131

for G being Group
for a being Element of G
for H being Subgroup of G holds
( carr H,a * H are_equipotent & carr H,H * a are_equipotent )