let G be addGroup; :: 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 ;
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;
then reconsider C = Right_Cosets H as finite set by Th136, CARD_1:38;
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