theorem :: GROUP_1A:196
for G being addGroup holds index ((Omega). G) = 1