let G be finite Group; :: thesis: index ((1). G) = card G
thus card G = (card ((1). G)) * (index ((1). G)) by Th177
.= 1 * (index ((1). G)) by Th81
.= index ((1). G) ; :: thesis: verum