let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H |^ a)
let a be Element of G; :: thesis: for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H |^ a)
let H be Subgroup of G; :: thesis: ( Left_Cosets H is finite implies index H = index (H |^ a) )
assume Left_Cosets H is finite ; :: thesis: index H = index (H |^ a)
then consider B being finite set such that
A1: ( B = Left_Cosets H & index H = card B ) by GROUP_2:def 18;
A2: ( Index H = card (Left_Cosets H) & Index (H |^ a) = card (Left_Cosets (H |^ a)) & Index H = Index (H |^ a) ) by Th84;
then Left_Cosets H, Left_Cosets (H |^ a) are_equipotent by CARD_1:21;
then Left_Cosets (H |^ a) is finite by A1, CARD_1:68;
then consider C being finite set such that
A3: ( C = Left_Cosets (H |^ a) & index (H |^ a) = card C ) by GROUP_2:def 18;
thus index H = index (H |^ a) by A1, A2, A3; :: thesis: verum