theorem :: GROUP_1A:199

for G being finite addGroup holds index ((0). G) = card G