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