let G be Group; :: thesis: for a being Element 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 Element 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 Th132
.= 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