for G being addGroup
for H being Subgroup of G holds
( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) ) by Th136, CARD_1:5;