for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff b * (a ") in H )