let G be Group; :: thesis: for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds
ex C being finite set st
( C = con_class A & card C = index (Normalizer A) )
let A be Subset of G; :: thesis: ( ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) implies ex C being finite set st
( C = con_class A & card C = index (Normalizer A) ) )
A1: card (con_class A) = Index (Normalizer A) by Th130
.= card (Left_Cosets (Normalizer A)) ;
then A2: con_class A, Left_Cosets (Normalizer A) are_equipotent by CARD_1:5;
assume A3: ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) ; :: thesis: ex C being finite set st
( C = con_class A & card C = index (Normalizer A) )
then reconsider C = con_class A as finite set by A2, CARD_1:38;
take C ; :: thesis: ( C = con_class A & card C = index (Normalizer A) )
thus C = con_class A ; :: thesis: card C = index (Normalizer A)
Left_Cosets (Normalizer A) is finite by A3, A2, CARD_1:38;
hence card C = index (Normalizer A) by A1, GROUP_2:def 18; :: thesis: verum