theorem :: GROUP_1A:198

for G being addGroup holds Index ((0). G) = card G