h = 1_ G by Def1;
hence g * h = g by GROUP_1:def 4; :: thesis: verum