let G be Group; :: thesis: for h being Element of G holds
( h |^ 2 = 1_ G iff h " = h )
let h be Element of G; :: thesis: ( h |^ 2 = 1_ G iff h " = h )
thus ( h |^ 2 = 1_ G implies h = h " ) :: thesis: ( h " = h implies h |^ 2 = 1_ G )

proof

assume h |^ 2 = 1_ G ; :: thesis: h = h "
then h * h = 1_ G by Th26;
hence h = h " by Th11; :: thesis: verum

end;

assume h = h " ; :: thesis: h |^ 2 = 1_ G
hence h |^ 2 = h * (h ") by Th26
.= 1_ G by Def5 ;
:: thesis: verum