let G be Group; :: thesis: for H being Subgroup of G st Left_Cosets H is finite holds
( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) )
let H be Subgroup of G; :: thesis: ( Left_Cosets H is finite implies ( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) ) )
assume A1: Left_Cosets H is finite ; :: thesis: ( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) )
then reconsider B = Left_Cosets H as finite set ;

hereby :: thesis: ex C being finite set st
( C = Right_Cosets H & index H = card C )

take B = B; :: thesis: ( B = Left_Cosets H & index H = card B )
thus ( B = Left_Cosets H & index H = card B ) by Def18; :: thesis: verum

end;

A2: ( B = Left_Cosets H & index H = card B ) by Def18;
reconsider C = Right_Cosets H as finite set by A1, Th166, CARD_1:68;
take C ; :: thesis: ( C = Right_Cosets H & index H = card C )
B,C are_equipotent by Th166;
hence ( C = Right_Cosets H & index H = card C ) by A2, CARD_1:21; :: thesis: verum