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