:: deftheorem defines Index GROUP_1A:def 27 :
for G being addGroup
for H being Subgroup of G holds Index H = card (Left_Cosets H);