let G be Group; :: thesis: for h being Element of G holds h |^ 1 = h
let h be Element of G; :: thesis: h |^ 1 = h
thus h |^ 1 = h |^ (0 + 1)
.= (h |^ 0) * h by Lm2
.= (1_ G) * h by Def7
.= h by Def4 ; :: thesis: verum