let G be Group; :: thesis: (1_ G) " = 1_ G
((1_ G) ") * (1_ G) = 1_ G by Def5;
hence (1_ G) " = 1_ G by Def4; :: thesis: verum