:: deftheorem Def18 defines index GROUP_1A:def 28 :
for G being addGroup
for H being Subgroup of G st Left_Cosets H is finite holds
for b₃ being Element of NAT holds
( b₃ = index H iff ex B being finite set st
( B = Left_Cosets H & b₃ = card B ) );