for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds a + H,H + b are_equipotent