theorem :: GROUP_1A:196

for G being addGroup holds index ((Omega). G) = 1