let G be Group; :: thesis: for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizator H) is finite ) holds
ex C being finite set st
( C = con_class H & card C = index (Normalizator H) )
let H be strict Subgroup of G; :: thesis: ( ( con_class H is finite or Left_Cosets (Normalizator H) is finite ) implies ex C being finite set st
( C = con_class H & card C = index (Normalizator H) ) )
assume A1: ( con_class H is finite or Left_Cosets (Normalizator H) is finite ) ; :: thesis: ex C being finite set st
( C = con_class H & card C = index (Normalizator H) )
A2: card (con_class H) = Index (Normalizator H) by Th161
.= card (Left_Cosets (Normalizator H)) ;
then A3: con_class H, Left_Cosets (Normalizator H) are_equipotent by CARD_1:21;
then ( con_class H is finite & Left_Cosets (Normalizator H) is finite ) by A1, CARD_1:68;
then consider B being finite set such that
A4: ( B = Left_Cosets (Normalizator H) & index (Normalizator H) = card B ) by GROUP_2:def 18;
reconsider C = con_class H as finite set by A1, A3, CARD_1:68;
take C ; :: thesis: ( C = con_class H & card C = index (Normalizator H) )
thus C = con_class H ; :: thesis: card C = index (Normalizator H)
thus card C = index (Normalizator H) by A2, A4; :: thesis: verum