for G being Group
for N being normal Subgroup of G holds card (G ./. N) = Index N ;