let G be addGroup; :: 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})) ;
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 A1;
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, A1;
hence card C = index (Normalizer {a}) by A1, Def18; :: thesis: verum