let G be Group; :: thesis: (1_ G) " = 1_ G
( ((1_ G) " ) * (1_ G) = 1_ G & (1_ G) * (1_ G) = 1_ G ) by Def5, Def6;
hence (1_ G) " = 1_ G by Th14; :: thesis: verum