for G being addGroup
for a being Element of G
for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H * a)