let G be Group; :: thesis: for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizator {a}) is finite ) holds
ex C being finite set st
( C = con_class a & card C = index (Normalizator {a}) )
let a be Element of G; :: thesis: ( ( con_class a is finite or Left_Cosets (Normalizator {a}) is finite ) implies ex C being finite set st
( C = con_class a & card C = index (Normalizator {a}) ) )
assume A1: ( con_class a is finite or Left_Cosets (Normalizator {a}) is finite ) ; :: thesis: ex C being finite set st
( C = con_class a & card C = index (Normalizator {a}) )
A2: card (con_class a) = Index (Normalizator {a}) by Th157
.= card (Left_Cosets (Normalizator {a})) ;
then A3: con_class a, Left_Cosets (Normalizator {a}) are_equipotent by CARD_1:21;
then ( con_class a is finite & Left_Cosets (Normalizator {a}) is finite ) by A1, CARD_1:68;
then consider B being finite set such that
A4: ( B = Left_Cosets (Normalizator {a}) & index (Normalizator {a}) = card B ) by GROUP_2:def 18;
reconsider C = con_class a as finite set by A1, A3, CARD_1:68;
take C ; :: thesis: ( C = con_class a & card C = index (Normalizator {a}) )
thus C = con_class a ; :: thesis: card C = index (Normalizator {a})
thus card C = index (Normalizator {a}) by A2, A4; :: thesis: verum