for G being Group
for a being Element of G
for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H |^ a)