let G be Group; :: thesis: index ((Omega). G) = 1
Left_Cosets ((Omega). G) = {the carrier of G} by Th172;
hence index ((Omega). G) = card {the carrier of G} by Def18
.= 1 by CARD_1:50 ;
:: thesis: verum