let G be addGroup; :: 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)) ;
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