for G being Group holds Index ((1). G) = card G