let G be addGroup; :: 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 A1: Left_Cosets H is finite ; :: thesis: index H = index (H * a)
then A2: ex B being finite set st
( B = Left_Cosets H & index H = card B ) by Def18;
A3: Index H = Index (H * a) by Th71;
then Left_Cosets (H * a) is finite by A1;
hence index H = index (H * a) by A2, A3, Def18; :: thesis: verum