let G be Group; :: thesis: for h being Element of G st h " = 1_ G holds
h = 1_ G
let h be Element of G; :: thesis: ( h " = 1_ G implies h = 1_ G )
(1_ G) " = 1_ G by Th8;
hence ( h " = 1_ G implies h = 1_ G ) ; :: thesis: verum