theorem :: GROUP_2:155

for G being Group
for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds
( G is finite & H = (1). G )