let G be Group; :: thesis: for a being Element of G holds a |^ a = a
let a be Element of G; :: thesis: a |^ a = a
thus a |^ a = (1_ G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4 ; :: thesis: verum