let G be addGroup; :: thesis: for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds
ex C being finite set st
( C = con_class H & card C = index (Normalizer H) )
let H be strict Subgroup of G; :: thesis: ( ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) implies ex C being finite set st
( C = con_class H & card C = index (Normalizer H) ) )
A1: card (con_class H) = Index (Normalizer H) by Th135
.= card (Left_Cosets (Normalizer H)) ;
assume A3: ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) ; :: thesis: ex C being finite set st
( C = con_class H & card C = index (Normalizer H) )
then reconsider C = con_class H as finite set by A1;
take C ; :: thesis: ( C = con_class H & card C = index (Normalizer H) )
thus C = con_class H ; :: thesis: card C = index (Normalizer H)
Left_Cosets (Normalizer H) is finite by A3, A1;
hence card C = index (Normalizer H) by A1, Def18; :: thesis: verum