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 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 ;

take C ; :: thesis: ( C = Right_Cosets H & index H = card C )

( index H = card B & B,C are_equipotent ) by Def18, Th136;

hence ( C = Right_Cosets H & index H = card C ) by CARD_1:5; :: thesis: verum

( 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 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 )

then reconsider C = Right_Cosets H as finite set by Th136, CARD_1:38;( 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;thus ( B = Left_Cosets H & index H = card B ) by Def18; :: thesis: verum

take C ; :: thesis: ( C = Right_Cosets H & index H = card C )

( index H = card B & B,C are_equipotent ) by Def18, Th136;

hence ( C = Right_Cosets H & index H = card C ) by CARD_1:5; :: thesis: verum