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