for G being Group
for N being normal Subgroup of G st Left_Cosets N is finite holds
card (G ./. N) = index N